| CAV 2006 | Computer-Aided Verification Seattle, August 17 - 20, 2006 |
CAV on Friday, August 18th
Invited Talk (09:00‑10:00)
Chair:
Ed Clarke
| 09:00‑10:00 | Tony Hoare
(Microsoft Research) The Ideal of Verified Software [ppt] I will argue that that the fundamental questions of Computer Science are similar to those of other branches of pure and applied science. Whatever the subject of study, these questions are 'What does it do?' , 'How does it work?' , 'Why does it work?' , and 'How can we be sure of the answers to these questions?' In the case of software, the research techniques of program verification provide us with the means to answer such questions. I will further ague that the ideal of program correctness is a scientific ideal like those of other branches of science: accuracy of measurement in physics, purity of materials in chemistry, rigour of argument in mathematics, etc. Perfection must always be pursued by scientists, in the sure knowledge that it will never be achieved. It is worth pursuing for its own sake, quite apart from its possible application to the making or the saving of money. It is only by adherence to an ideal that a professional specialist can deserve and win the necessary trust to apply scientific knowledge for the practical benefit of clients. I will conclude with a speculation that progress in our science may be accelerated by following the example of other branches of 'big science' , which plan a major long-term collaborative projects under the title of a Grand Challenge. A Grand Challenge in Verified Software would involve the development of theories, the construction of toolsets, and the conduct of significant experiments to test and improve the tools. |
Break (10:00‑10:30)
Session 5: Abstraction/Refinement (10:30‑12:00)
Chair:
Orna Grumberg
| 10:30‑11:00 | Kenneth McMillan
(Cadence Berkeley Labs) Lazy Abstraction with Interpolants We describe a model checker for infinite-state sequential programs, based on Craig interpolation and the lazy abstraction paradigm. On device driver benchmarks, we observe a speedup of up to two orders of magnitude relative to a similar tool using predicate abstraction. |
| 11:00‑11:30 | Himanshu Jain
(Carnegie Mellon University) Franjo Ivancic (NEC Laboratories USA) Aarti Gupta (NEC Laboratories USA) Ilya Shlyakhter (NEC Laboratories USA) Chao Wang (NEC Laboratories America) Using Statically Computed Invariants inside the Predicate Abstraction and Refinement Loop Predicate abstraction is a powerful technique for extracting finite-state models from often complex source code. This paper reports on the usage of statically computed invariants inside the predicate abstraction and refinement loop. The main idea is to selectively strengthen (conjunct) the concrete transition relation at a given program location by efficiently computed invariants that hold at that program location. We experimentally demonstrate the usefulness of transition relation strengthening in the predicate abstraction and refinement loop. We use invariants of the form ax + by <= c where a,b belong to {-1,1}, c is a constant and x,y are program variables for transition relation strengthening. These invariants can be discovered efficiently at each program location using the octagon abstract domain. We observe that the abstract models produced by predicate abstraction of strengthened transition relation are more precise leading to fewer spurious counterexamples, thus, decreasing the total number of abstraction-refinement iterations. Furthermore, the length of relevant fragments of spurious traces needing refinement shortens. This leads to an addition of fewer predicates for refinement. We found a consistent reduction in the total number of predicates, maximum number of predicates tracked at a given program location, and the overall verification time. |
| 11:30‑12:00 | Daniel Kroening
(ETH Zurich) Georg Weissenbacher (ETH Zurich) Counterexamples with Loops for Predicate Abstraction Predicate abstraction is a major abstraction technique for the verification of software. Data is abstracted by means of Boolean variables, which keep track of predicates over the data. In many cases, the technique suffers from the fact that it requires one predicate for each iteration of a loop construct in the program. We propose to extract looping counterexamples from the abstract model, and to parameterize the simulation instance in the number of loop iterations. |
Session 6: Tools Papers (12:00‑12:30)
Chair:
Orna Grumberg
| 12:00‑12:15 | Nikhil Sethi
(New York University) Clark Barrett (New York University) Cascade: C Assertion Checker and Deductive Engine We present a tool, called Cascade, to check assertions in C programs as part of a multi-stage verification strategy. Cascade takes as input a C program and a control file (the output of an earlier stage) that specifies one or more assertions to be checked together with (optionally) some restrictions on program behaviors. For each assertion, Cascade produces either a concrete trace violating the assertion or a deduction (proof) that the assertion cannot be violated. |
| 12:15‑12:30 | Arie Gurfinkel
(University of Toronto) Ou Wei (University of Toronto) marsha chechik (university of toronto) Yasm: A Software Model-Checker for Verification and Refutation This paper describes Yasm -- a symbolic software model-checker, based on the CEGAR approach. Yasm enables simultaneous reasoning about over- and under-approximating abstractions. Not only is the tool performance comparable to its standard counterparts such as SLAM and BLAST, but more importantly, combining both approximations opens out an array of interesting analyses and optimizations. |
Lunch break (12:30‑14:00)
Session 7: Symbolic Trajectory Evaluation (14:00‑15:00)
Chair:
Fabio Somenzi
| 14:00‑14:30 | Jan-Willem Roorda
(Chalmers University of Technology) Koen Claessen (Chalmers Technical University) SAT-based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation We present a SAT-based algorithm for assisting users of Symbolic Trajectory Evaluation (STE) in manual abstraction refinement. We demonstrate the usefulness of the algorithm on a larger case study (the verification of a CAM). |
| 14:30‑15:00 | Rachel Tzoref (IBM/Technion) Orna Grumberg (Prof. Dept. of Computer Science, Technion) Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation Symbolic Trajectory Evaluation (STE) is a powerful technique for model checking. It is based on 3-valued symbolic simulation, using 0,1 and X ("unknown"). The X value is used to abstract away parts of the circuit. The abstraction is derived from the user's specification. Currently the process of abstraction and refinement in STE is performed manually. This paper presents an automatic refinement technique for STE. The technique is based on a clever selection of constraints that are added to the specification so that on the one hand the semantics of the original specification is preserved, and on the other hand, the part of the state space in which the "unknown" result is received is significantly decreased or totally eliminated. In addition, this paper raises the problem of vacuity of passed and failed specifications. This problem was never discussed in the framework of STE. We describe when an STE specification may vacuously pass or fail, and propose a method for vacuity detection in STE. |
Session 8: Property Specification and Verification (15:00‑16:00)
Chair:
Fabio Somenzi
Break (16:00‑16:30)
Session 9: Time (16:30‑18:00)
Chair:
Holger Hermanns
| 16:30‑17:00 | Marta Kwiatkowska
(University of Birmingham) Gethin Norman (University of Birmingham) David Parker (University of Birmingham) Symmetry Reduction for Probabilistic Model Checking We present an approach for applying symmetry reduction techniques to probabilistic model checking, a formal verification method for the quantitative analysis of systems with stochastic characteristics. We target systems with a set of non-trivial, but interchangeable, components such as those which commonly arise in randomised distributed algorithms or probabilistic communication protocols. We show, for three types of probabilistic models, that symmetry reduction, similarly to the non-probabilistic case, allows verification to instead be performed on a bisimilar quotient model which may be up to factorially smaller. We then propose an efficient algorithm for the construction of the quotient model using a symbolic implementation based on multi-terminal binary decision diagrams (MTBDDs) and, using four large case studies, demonstrate that this approach offers not only a dramatic increase in the size of probabilistic model which can be quantitatively analysed but also a significant decrease in the corresponding run-times. |
| 17:00‑17:30 | Pavel Krcal
(PhD student) Wang Yi (Professor) Communicating Timed Automata: The More Synchronous, the More Difficult to Verify We study channel systems whose transitions (sending and receiving messages via unbounded FIFO channels) must follow given timing constraints specifying the relative execution speeds of the local components. We adopt Communicating Timed Automata (CTA) to model such systems. The goal is to study the borderline between decidable and undecidable classes of channel systems in the timed setting. Our technical results include: (1) CTA with one channel without shared states in the form (A1,A2,c1,2) is equivalent to one-counter machine, implying that verification problems such as checking state reachability and channel boundedness are decidable, and (2) CTA with two channels without sharing states in the form (A1,A2,A3, c1,2,c2,3) has the power of Turing machines. Note that in the untimed setting, these systems are no more expressive than finite state machines. It is somewhat surprising that the capability of synchronizing on time makes it substantially more difficult to verify channel systems. |
| 17:30‑18:00 | Grigore Rosu
(University of Illinois at Urbana-Champaign) Saddek Bensalem (VERIMAG) Allen Linear (Interval) Temporal Logic -- Translation to LTL and Monitor Synthesis The relationship between two well established formalisms for temporal reasoning is first investigated, namely between Allen's interval algebra (or Allen's temporal logic, abbreviated ATL) and linear temporal logic (LTL). A discrete variant of ATL is defined, called Allen linear temporal logic (ALTL), whose models are omega-sequences of timepoints, like in LTL. It is shown that any ALTL formula can be linearly translated into an equivalent LTL formula, thus enabling the use of LTL techniques and tools when requirements are expressed in ALTL. Then the monitoring problem for ALTL is discussed, showing that it is NP-complete despite the fact that the similar problem for LTL is EXPSPACE-complete. An effective monitoring algorithm for ALTL is given, which has been implemented and experimented with in the context of planning applications. |
Session 10: Tools Papers (18:00‑18:30)
Chair:
Holger Hermanns
| 18:00‑18:15 | Jiri Barnat (Masaryk University) Lubos Brim (Masaryk University) Ivana Cerna (Masaryk University) Pavel Moravec (Masaryk University) Petr Rockai (Masaryk University) Pavel Simecek (Masaryk University) DiVinE - A Tool for Distributed Verification We present a tool for distributed-memory LTL model-checking and reachability analysis that employs clusters of workstations. The tool incorporates several novel distributed-memory algorithms and provides unique interface to use them. We describe the basic structure of the tool, discuss main architecture decisions made, and briefly explain how the tool is used. |
| 18:15‑18:30 | Flavio M. de Paula
(University of British Columbia) Alan Hu (University of British Columbia) EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation Abstraction-guided simulation is a general framework for automatically harnessing, during simulation, information from abstraction and model checking. EverLost is our platform for industrial-strength usage of abstraction-guided simulation. EverLost takes an RTL Verilog design and preimage/abstraction information from any abstraction/model-checking tool, and automatically generates code that implements abstraction-guided simulation and directly compiles with the design under the widely-used Synopsys VCS simulator. The platform enables flexible exploration of abstraction-guided simulation --- different formal tools and different guidance heuristics are easily inserted --- while providing the capacity, speed, and Verilog compatibility of a leading industry-standard tool. |
CAV-IJCAR Joint Cruise/Banquet (19:00‑22:30)
Location:
depart Spirit of Seattle from Pier 55
| 19:00‑19:30 |
CAV-IJCAR Joint Cruise/Banquet Boarding from Pier 55 (walking distance from hotel) |
| 19:30‑22:30 |
CAV-IJCAR Joint Cruise/Banquet
|
