A cut-off approach for bounded verification of parameterized systems (ICSE 2010) - A Short Review

A cut-off approach for bounded verification of parameterized systems. - Qiusong Yang, Mingshu Li

In this paper a new approach based on forward bounded reachability analysis is proposed for verification of parameterized systems. Experimental results show improvements in verification efficiency as a result of introduction of new cut offs on the maximum length of paths.

For the notations used in the paper, the properties of parameterized systems are expressed in property automata, whose accepting languages (paths leading to trap states) prescribe undesirable behaviour of verified system. The overall approach starts with construction of an extended reachability graph (ERG), which is the synchronous product of the property automaton and the parameterized system. It models the execution of control processes and regulated replications of a parameterized system and their execution’s impact on the property automaton. Instead of using a complete ERG a set of increasingly refined abstractions to it is sequentially generated.  In order to abstract the global state of the parameterized system a notion of configuration is introduced as follows

-          Configuration is a vector of the form c= where ‘s’ is a state vector and ‘a’ is a counter vector.

-          These configuration form the vertices of the ERG while the edges of the graph represent the transitions between these configurations

-          It can  be shown that is possible to calculate the configurations inductively from a finite bounded ERG

The authors state and prove a theorem in the paper which shows that only a finite bounded ERG is needed in order to prove the property.

The given algorithm is implemented in java and compared with other existing algorithms for verification of parameterized systems. The results of such a comparison show that FBRA out performs the known methods in many of the examples. But in a few cases it is indeed slower which the authors attribute to the enumeration of all states in ERGs.  As future work they propose to adopt some of the strategies used to optimize the FBRA algorithm.

Falcon: fault localization in concurrent programs (ICSE 2010) - A Short Review

Falcon: fault localization in concurrent programs - Sangmin Park, Richard W. Vuduc, Mary Jean Harrold

This paper presents a new dynamic fault localization technique that can pinpoint faulty data-access patterns in multithreaded concurrent programs. The authors explain the technique by means of running example which proceedings with the following steps

-          The authors start with defining concurrency violations of interest for this paper

o   Data Race – do not focus on it in this paper but the method can handle this

o   Order Violation – Conflicting interleaving patterns

o   Atomicity Violation –  Unserializable interleaving patterns

-          Online Pattern Identification, in this step they monitor an instrumented version of the program which is run multiples times. In each of these runs a fixed sliding window is used to identify patterns. Any interesting pattern is an interleaving of read write accesses to a shared memory location. These patterns are associated with passing and failing executions.

o   Within a particular siding window look for access for a particular shared memory location

o   Once the window becomes full, scan it for unserializable interleaving patterns

o   If there is no unserializable interleaving pattern check for conflicting interleaving patterns

o   Emit all patterns found

o   These patterns are then associated with passing and failing executions

-          In the second step the patterns are ranked using suspiciousness (based on Jaccard Index) which represents the likelihood of a pattern being related to a fault.

                                                                                                

A prototype implementation (FALCON) of this technique in Java and a detailed empirical study of the system is given next in the paper. They evaluate the effectiveness and efficiency of the system with respect to the ability to indentify suspicious patterns which relate to faults. The results from the study of window size show that for most cases a moderate window (10) size can still enable FALCON to detect many relevant suspicious patterns (75%). Finally a study indirectly compares FALCON to CCI (which is a related recent work done in fault localization) the authors conclude that FALCON ranks the patterns much better than the related ranking of accesses from CCI.

Even though the initial study is promising there are a number of limitations which can form future work, current system only take 1 test input and execute the program multiple times. There is no relation between the pattern and the actual bug that causes the suspicious pattern.  A single bug may give rise to many patterns or vice versa. There are other types of violations like deadlocks which are not currently indentified using FALCON.

Oracle-guided component-based program synthesis (ICSE 2010) - A Short Review

Oracle-guided component-based program synthesis - Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari

In this paper the authors propose a novel technique for synthesizing loop-free programs. Two potential usage of such a synthesis can be in generating efficient bit manipulating programs and for deobfuscating malware programs.  Formally the synthesis problem considered in the paper requires

-          A validation oracle V, that, given any candidate program can tell whether the program is the desired one or not. (For the examples in this paper the user herself is the validation oracle)

-          An I/O oracle I, that, given any program input, returns the output of the desired program on that input. (Again the user herself is the I/O oracle for the examples in this paper)

-          A set of specifications called a library of basic components f, such that each component includes,

o   A tuple of input variables and a output variable

o   An expression over the input and out variables such that it specifics the input-output relationship of the component

Now the goal of the synthesis problem is to synthesize a program P that can be validated by the oracle V, i.e. V (P) = true.  Further, the program P should be contrasted using only the base components in the library.

The authors propose an encoding of the program using a set of integer-valued location variables L, such that the value of the variable determine which components goes where (location) and from which location it takes its input. Next they define two constraints

-          I/O behavioural constraint which ensures that the generated program has the same input-output behaviour as that specified by the I/O oracle.

-          Distinguishing constraint which generates an input that differentiates this program from another candidate program

Now you can synthesis the candidate program by using SMT solvers to solve the behavioural constraint and then using SMT solvers again to solve the distinguishing constraint that will generate an input (new) which is added to the set of input-output pairs and this continues unless we get a semantically unique program (shown my failure of SMT solver to solve distinguishing constraint). Check that program with the validation oracle to see if it valid.

The evaluation sections shows the applicability of this approach to synthesize minimal bit manipulating programs and the authors also discuss optimizing this technique by using an application dependent bias in the sampling of input space. In the discussion the authors explore connections of this approach with fundamental results in computational learning theory.  They say that on the basis of the teaching dimension results by Goldman and Kerns it can be shown that only a few examples would be needed to synthesis these programs as they form a low teaching dimension.

Possible weakness of the approach is limitation to synthesis of simple (minimal) loop-free programs.

Has the bug really been fixed? (ICSE 2010) - A short review

This paper defines and formalizes the Bad Fix Problem, as per studies developers spend 50-80 % of their time fixing bugs. Many of these bug fixes themselves are a) sources of new bugs and b) do not fix the original bug for all inputs. The authors formalize these two notions as Coverage and Disruption.

Where,

Coverage of the fix measures the extent to which the fix correctly handles all the bug triggering inputs

And Disruption of a fix counts the deviations from the program’s intended behaviour introduced by a fix.

Hence for a given fix, the Bad Fix Problem is to determine the coverage and disruption of the fix.

The approach taken to calculate the Coverage for the fix is based on Distance Bounded Weakest Precondition (WP). In order to mitigate the path-explosion problem of WP the authors calculate the WP for a subset of paths near a distinguished path in the interprocedural control flow graph (ICFG).  The distance measure they use for nearness is the Levenshtein distance (which represents the minimum number of add/delete/substitutes required to change a string to another). The concrete path induced by the known bug triggering input is used as the distinguished path for calculating the Distance Bounded WP.

Once we have the distance bounded WP the coverage of a fix is determined by executing the Program symbolically using the WP and deriving a Post Condition (eliminating non-input variables from the clause).  For a buggy input the output of the program violates an assertion (say A) now if the post condition implies A then the fix is valid in terms of the coverage or else we report a counter example as a new bug triggering input.

The violations in disruption are defined by the test suite. So if the new Program runs on standard regression test cases as well as on a random subset of inputs we claim the fix valid and every test case failure is a disruption.

The authors implement this approach in a tool for the java language (FIXATION). The empirical evaluation shows that fixation is able to identify the known bad fixes in the code in reasonable time. The path explosion problem of WP is avoided by using a distance measure for calculating WP. The authors show that the analysis is able to scale for increasing values of distance “d”.

One of the limitations of this approach can be that it models the bugs as assertion failures and it relies on assertions being available or inferred. Also determining the value of distance “d” to obtain a better results is still a problem the papers suggests that the user start with a small value and increment it as more paths are explored. The possible future application of this approach can be in unit testing where the tool can directly work with the self contained assertions in a unit test case.

References

1. Gu, Zhongxian, et al. "Has the bug really been fixed?." Software Engineering, 2010 ACM/IEEE 32nd International Conference on. Vol. 1. IEEE, 2010.