"Program verification aims at proving that programs meet their specifications, i.e., that the actual program behaviour coincides with the desired one. Model checking refers to algorithmic techniques for program verification. Model checking has been applied to the verification of temporal properties of reactive and concurrent systems, which has proven successful in the area of Harware, Protocols and Embedded Systems Controllers verification."
While explicit state space exploration is used for model checking
systems with small state spaces,
symbolic model checking based on the Binary Decision Diagrams introduced by Bryant has proved effective in model checking many moderately sized finite state systems. This has found considerable use in Hardware Verification.
"Since its introduction in 1999 by Biere, Cimatti, Clarke and Zhu, Bounded Model Checking has been adopted as a complementary technique to the more traditional BDD based unbounded symbolic model checking. Largely due to the advances in SAT technology in the last few years, Bounded Model Checking became a leading tool in detection of relatively shallow logical errors, outperforming BDD based tools in most of these cases. The large interest in this technology has created a constant stream of new ideas and improvements that make this technique more and more useful."
"The growing importance of model checking in hardware verification and the difficulty of producing correct software are driving a growing interest in the application of model checking to software. This leads to many challenges of scientific and practical interest, both in core model checking technology and in supporting techniques, such as program analyses and transformations that help automate abstraction of the data state and reduction of the control state."
(Excerpts from Recently Held Related Workshops)
Randy Bryant (Carnegie Mellon University)
Alessandro Cimatti (IRST, Trento, Italy)
Sriram Rajamani (Microsoft Research)
Tata Institute of Fundamental Research
Homi Bhabha Road, Colaba
Mumbai 400 005
Date: 14 December 2003
Workshop Email: email@example.com
How to reach TIFR: See http://theory.tifr.res.in/misc/reaching_tifr.html
Paritosh K. Pandya (Coordinator)
School of Technology and Computer Science, TIFR
Homi Bhabha Road, Colaba
Mumbai 400 005
Phone: ++91 22 22804545 Ext. 2551
Supratik Chakraborty (Co-cordinator)
Dept. of Computer Science and Engg.
Powai, Mumbai 400 076
Speaker: Randy Bryant (Carnegie Mellon University)
Title: SAT-Based Decision Procedures for Subsets of First-Order Logic
Abstract: Formal verification tools that operate on finite-state system models, such as symbolic model checkers, have gained widespread acceptance in industry due to their ability to handle large scale designs and to require minimal human guidance. More abstract systems, such as synchronization protocols that work for arbitrary numbers of processes and software programs that work for arbitrary word and memory sizes, call for tools that can verify infinite state systems. Historically, the only way to mechanically verify such systems was to use a general-purpose, automated theorem prover. This requires considerable effort and expertise on the part of the user.
A more recent trend has been to create automatic verification tools for infinite-state systems that use specialized decision procedures for subsets of first-order logic. This talk presents one approach to creating such decision procedures, in which the first-order formula is translated into a satisfiability preserving propositional formula. We then use an existing Boolean satisfiability (SAT) solver to decide the original formula. This approach exploits the tremendous improvements recent SAT solvers have made in both efficiency and capacity.
We describe a very limited class of logic, allowing only uninterpreted functions with equality. We then extend this to include "separation constraints" of the form x <= y + c, where c is an integer constant. We describe different techniques for encoding integer constraints into propositional logic and ways to exploit the structure of the formulas to greatly improve the efficiency of the decision procedure.
Speaker: Alessandro Cimatti (IRST, Trento, Italy)
Title: Symbolic Model Checking: a SAT-based perspective
Abstract: The introduction of symbolic techniques has been the enabling factor
for model checking large sized designs. Traditionally, symbolic model
checking has been based on Binary Decision Diagrams; more recently,
Bounded Model Checking has highlighted the potential for symbolic
techniques based on propositional satisfiability (SAT).
In the first part of the talk, I will overview the field of symbolic
model checking, with particular emphasis on SAT-based methods. In the
second, I will present the MathSAT paradigm, and its applications to
symbolic model checking. MathSAT extends propositional satisfiability
to deal with constraints over numerical variables, and provides a
uniform and efficient way for advanced forms of model checking, such
as word-level reasoning, and reasoning about Timed and Hybrid systems.
Speaker: Sriram Rajamani (Microsoft Research)
Title: Software Model Checking with SLAM
Abstract: Model checking is a technique to find bugs in systems be systematically exploring their state spaces. Due to state space explosion, model checkers typically operate on a manually constructed finite-state abstraction of the system. The goal of the SLAM project is to model check software written in common programming languages directly. SLAM has been successfully used to find and fix errors in Windows device drivers written in the C language.
SLAM operates by automatically constructing and refining model-checkable abstractions (called Boolean Programs) of a C program. The first part of this tutorial will describe how the SLAM project has combined and extended results from the areas of program analysis, model checking and theorem proving to analyze critical properties of systems software written in the C language. The second half of the tutorial will present some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.
SLAM is joint work with Tom Ball, Byron Cook, Vladimir Levin and Jakob Lichtenberg.
|09:15 -- 09:30||Inauguration|
|09:30 -- 10:30||Alessandro Cimatti|
|10:30 -- 11:00||Coffee/Tea|
|11:00 -- 12:00||Alessandro Cimatti|
|12:00 -- 13:00||Sriram Rajamani|
|13:00 -- 14:00||Lunch|
|14:00 -- 15:00||Sriram Rajamani|
|15:00 -- 16:00||Randy Bryant|
|16:00 -- 16:30||Coffee/Tea|
|16:30 -- 17:30||Randy Bryant|
|17:30 -- 17:45||Concluding Remarks|
A bus will be arranged to bring and take back the workshop participants from IIT Mumbai and the Rodas Hotel (near IIT) to TIFR on 14th December. (Timings of this bus and boarding locations will be notified later on this web page.)
Participants of ICLP/ASIAN
conferences and any other participants wishing to attend the workshop must
directly communicate with the workshop coordinator by email after 2nd November
2003 but before 9 December 2003. The email for this should be sent
to firstname.lastname@example.org with Subject: Workshop Registration.
Approved requests will be acknowldeged. Please do not participate without
obtaining such acknowledgement.