Reports for Article 138 Reviewed Article Article ID 138 Author Kuncak, Viktor Title Delayed Choice Execution for Falsification Abstract
We present an approach for finding errors in programs and specifications. We formulate our approach as an execution mechanism for a non-deterministic guarded-command language. Guarded commands have already proved useful for verification-condition generation but are usually viewed as a non-executable representation. We show how to execute guarded commands using an explicit-state model checker. We illustrate the benefits of this approach in two related domains: bounded-exhaustive testing and falsification for Hoare triples.
The basis of our approach is the delayed-choice technique for improving the execution of guarded commands. Delayed choice postpones non-deterministic choice of values until they are used. Our approach also supports copy-propagation of symbolic values but avoids the cost of full-blown symbolic execution.
We describe an implementation of our approach in Java PathFinder, a popular model checker for Java programs. Our experimental results show that our techniques significantly improve performance compared to the current execution strategy in Java Pathfinder.
Type of Contribution (Category) Regular Paper Report 138-FR-608
Default_[Final_Report] Decision Outcome
Dear Author,
We are sorry that we have to inform you that your submission has not been accepted at TACAS'09.
The selection process was very competitive as we received 131 papers and were able to accept only 35. Please log in at the conference website to get access to the review reports.
We wish you all the best for your future research and hope that the reviewer feedback on your submission is helpful for you. Of course, we would be happy if you would still consider attending TACAS'09.
Sincerely,
Stefan Kowalewski and Anna Philippou
PC Co-Chairs, TACAS 2009 Report 138-R-257
Default Score
Either Way Confidence
High Detailed Comments for Author(s)
The paper claims two contributions: (a) the use of a non-deterministic guarded command language to write pre and post conditions, and to use symbolic execution to check correctness of the resulting Hoare triple {P}s{Q}, (b) the use of delayed choice as a lightweight symbolic execution.
I do not agree that (a) is novel. In fact, I think the claim in the abstract that “Guarded commands … are usually views as a non-executable specification” is not true: there are many previous instances of guarded commands used as programming languages (e.g., Flanagan and Saxe, generating compact verification conditions).
The second idea is that in an explicit model checker, do not choose values of every input right away, but symbolically track the inputs until they are used for the first time. This ensures that, e.g., inputs that are never used along interesting paths are not expanded in the model checker. This experimental evaluation of this idea (performed in Java Pathfinder) is of interest. Report 138-R-31
Default Score
Either Way Confidence
Medium Detailed Comments for Author(s)
This paper describes the use of delayed choice technique in the explicit state model checking setting, for the purpose of test generation or falsification of Hoare triples used in modular verification. The main idea is to delay the non-deterministic choices of values until the values are used for the first time. In a sense, this replaces forward (eager) choice splitting on multiple values, by a backward (lazy) splitting, which can be goal-directed toward a counterexample. An additional technique is to support copy-propagation of symbolic values, which delays the choice of values if the values are simply copied without modification. These techniques provide light-weight symbolic execution in the explicit state setting. The authors report results for an implementation in JPF, that shows significant performance improvement on many test generation benchmarks.
Although the idea of delayed choice is not new, it is interesting to see the evolution and migration of these ideas from Korat to JPF. On the other hand, there should be a better comparison against purely symbolic approaches.
The paper also discusses many other aspects of their approach, including a unified style of predicate-based and generator-based specifications for pre-conditions. I did not find much novelty in these discussions. Indeed, as in most such approaches, the examples show the practical difficulties in manually creating complex specifications, no matter which style.
The organization of the paper should be improved. The example (Section 2) runs on until page 9, and still the reader has only a vague notion of what delayed choice execution is. I would recommend keeping this section quite short, describing the technical details in Section 3, and then getting back to detailed explanation of the example. Also, many aspects of the overall testing method are thrown at the reader in Section 2 – these too can be better organized, perhaps in a separate background section.
A related reference is the following work, which also uses the idea of delayed choice in an explicit state model checker, although the application is for verification of assembly code:
Thomas Noll and Bastian Schlich. Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code. In Proceedings of the Haifa Verification Conference (HVC), 2007, LNCS 4899, Springer. Report 138-R-380
Default Score
Mild Reject Confidence
High Detailed Comments for Author(s)
This paper discusses a so-called “delayed-choice execution” technique for generating counterexamples violating a specific Hoare triple of the form {precondition}program{postcondition}.
Unfortunately, the originality and depth of this paper are really weak.
The first claimed contribution (see page 3) of supporting a combination of predicates to specify preconditions as well as test generators (nondeterministic test drivers) is not new: systems like Boogie [4] already support all this (for instance, x=getInt(a,b) can be written as havoc{x};assume{a=<x=<b}).
The second claimed contribution, namely the (simple) idea of “delayed choice execution” and “copy propagation” is not new either: both of these techniques are already used in many tools, like DART [19]. Specifically, the “algorithm” (3 last lines) of page 10 is included in the combination of Figures 1 and 3 in [19] (in [19], an assignment of the form v=x just updates the symbolic value of v with the symbolic value of x, only conditional statements may force concretizations). Another example is EXE [EXE: Automatically Generating Inputs of Death, CCS'2006] where x=getInt(a,b) can be simulated using make_symbolic(&x). Note that the claim on page 13 that “delayed choice execution is complementary to [19,32] and can be used to optimize them” is misleading at best as delayed choice execution is already a particular case (and crude approximation) of what is done in [19,32], among other tools – this point should be clarified. Finally, as pointed out by the authors themselves, delayed choice execution has also been used in static symbolic execution previously, like [22]. (Therefore, the choice of the current vague title for this paper is poor.)
The third claimed contribution is that “delayed choice execution” is an improvement over the “standard” explicit technique used in Java PathFinder. The baseline chosen by the authors for this favorable comparison is the fully-exhaustive explicit interpretation of x=getInt(a,b) (where getInt has for effect to exhaustively enumerate all the integers between a and b), which is obviously dumb in this context and has already been addressed by using symbolic execution techniques in other papers (such as [22]). Thus, strictly speaking, the third claim may be correct, but it is unsurprising and unimpressive.
Note that I am sympathetic with several (good) methodological observations made in the paper, such as the power of using well-chosen hand-crafted nondeterministic test drivers like the one in Figure 7. However, such observations are not new either. For a research paper, such general methodological observations are really too thin for a competitive conference like TACAS.