Sriram Rajamani, Microsoft Research
Joint Work with James Larus and Jakob Rehof
Abstract: I will present recent work on a language extension to C#, called Sharpie for writing asynchronous programs. Sharpie adds 3 new constructs: futures, joins and contracts. Futures and joins are used to write asynchronous function calls, and contracts are used to write specifications for services. Conformance of a Sharpie program with its contracts is done using a combination of type checking and model checking.
Sagar Chaki, Carnegie Mellon University
Joint Work with Edmund Clarke, Alex Groce, Somesh Jha, Joel Ouaknine, Ofer Strichman, Helmut Veith, Karen Yorav
Abstract: Over the last year or so, our group has been working on a project aimed at specifying and verifying safety properties of industrial scale concurrent programs written in C. The salient features of this work are:
1) Specifications are expressed using finite labeled transition systems (LTSs) where the transitions are labeled by actions.
2) A LTS model is extracted from the C code using predicate abstraction.
3) Verification involves checking a conformance relation between the specification and the model. Currently we can check both trace containment and weak simulation. The conformance checking problem is reduced to a N-HORNSAT instance.
4) The verification can be done modularly. Individual procedures can be specified and verified. The specification of a procedure foo can be used as a "stub" when verifying a procedure bar that calls foo.
5) Fully automated counterexample guided abstraction refinement is used to discover predicates. Attempt is made to ensure that the set of predicates is "minimal" w.r.t. the verification task.
6) Concurrent programs are assumed to interleave arbitrarily and communicate via shared actions. A two-level abstraction-refinement scheme is used to mitigate the statespace explosion due to concurrency.
The culmination of our efforts so far has been the tool MAGIC (Modular Analysis of proGrams In C). In this talk I will give an overview of the technicalities and our experiences in this research.James C. Browne, The University of Texas at Austin
Joint work with Robert P. Kurshan, Vladimir Levin, Natasha Sharygina and Fei Xie
Abstract: Although model checking of hardware has become mainstream, having entered the commercial domain, model checking techniques for software are still in relative infancy. Attempts to apply directly the techniques that work for hardware have met limited success.
In this paper we show through a case study of model checking a NASA Robot Controller, how hardware model checking techniques can be successfully modified and used to handle software. It starts with design-for-verification. With sufficient structure, we demonstrate that compositional techniques can succeed with software. Since standard software development languages are ill-suited for model checking in general, it is necessary to devise a plan to translate a sufficient subset of the software development language into the finite state language of the model checker. It is possible to identify such a "sufficient subset" when the design has been suitably structured with this process in mind.
The NASA software that we analyzed is the control subsystem of an operational robotics system. The paper attempts an objective assessment of the effectiveness of model checking for software systems which implement control and to provide transferable understanding what worked and what did not work and why.
Matthew B. Dwyer, Kansas State University
Joint work with John Hatcliff, Robby, Venkatesh Prasad Ranganath
Abstract: We propose several partial order reduction strategies for model-checking concurrent object-oriented software that are based on detecting heap objects that are "thread-local", i.e., reachable from a single thread only. We show how thread-local information appropriate for driving these reductions can be obtained by static analysis (using adaptations of existing escape analyses).
We also show that in many cases, existing static analyses targeted to compiler optimizations fail to detect thread-local information that can lead to significant savings in model-checking.
We describe a heap analysis that is carried out on-the-fly during model-checking to drive partial order reductions. We explain how, relative to static escape analysis, this on-the-fly analysis is actually simpler to implement in our model checking framework, introduces only moderate run-time overhead, and can significantly reduce the memory usage. We present a few preliminary results that show upwards of 20 times state-space reduction on realistic programs.
Willem Visser, NASA Ames
Abstract: This talk will give an overview of how the JPF model checker has evolved over the last three years and what we believe the future holds. Although JPF has been quite successful inside and outside of NASA, we have learned a number of lessons from wrong turns, mostly due to our unrealistic believe of what a model checker for Java could do one day.
The talk will highlight some of these misguided believes and how we have adjusted our goals within the JPF project as well as our research group at NASA Ames.
The talk will also introduce some of the new extensions we have made to the architecture of the tool and to the reasoning capabilities. Lastly some highlights will be given of how model checking performed in a recent study where we compared the effectiveness of model checking, static analysis, runtime analysis and testing for finding seeded errors in the executive of the K9 Mars Rover.
Daniel Kroening, Carnegie Mellon University
Joint work with Ed Clarke and Karen Yorav
Abstract: We present an algorithm that checks behavioral consistency between an ANSI-C program and a circuit given in Verilog using Bounded Model Checking. Both the circuit and the program are unwound and translated into a formula that represents behavioral consistency. The formula is then checked using a SAT solver. We are able to translate C programs that make use of side effects, pointers, dynamic memory allocation, and loops with conditions that cannot be evaluated statically. We describe experimental results on various reactive circuits and programs, including a small processor given in Verilog and its Instruction Set Architecture given in ANSI-C.
Shaz Qadeer, Microsoft Research
Joint work with Cormac Flanagan (HP Systems Research Center), Stephen N. Freund (Williams College), and Sanjit A.Seshia (Carnegie Mellon University).
Abstract: Ensuring the reliability of multithreaded software systems through testing is difficult, because of nondeterministic and subtle interactions between threads. Static checking, which has the potential to analyze the program's behavior over all execution paths and for all thread interleavings, is a promising complementary technique. We have built a scalable and expressive static checker called Calvin for multithreaded Java programs. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. The checker leverages off existing techniques based on verification conditions and automatic theorem proving.
To evaluate the checker, we have applied it to several real-world programs. Our experience indicates that Calvin has a moderate annotation overhead and can catch defects in multithreaded programs, including synchronization errors and violation of data invariants.