Principal investigator Javier Esparza
Second proposer Stefan Schwoon
Research Assistant/PhD student Stefan Kiefer
Research Assistant/PhD student Jan Holeček
Student Research Assistant Ganna Monakova
Funding
DFG project
Research
Model checking is a technique for the automatic
verification of computer systems based on exhaustive exploration of the
space of reachable states. It has been very successfully
applied to large hardware systems. The extension and application of
model checking to software is one of the main challenges of today's
research on formal verification. The main difficulty lies in the
infinite-state nature of software systems, as opposed to the finite-state
nature of hardware.
In previous work we have developed model-checking algorithms for
pushdown systems, a class of infinite-state systems able to model programs
with possibly recursive procedures. These have been implemented
in the Moped tool. The algorithms/the tool are currently used in
software model-checking projects at Berkeley, CMU, Graz, Inria, and Winsconsin.
These projects (together with our own experiments on using Moped for the
verification of Windows NT drivers) have exposed the need for further
efficient algorithms allowing to deal with more general systems and
specifications.
On the system side, algorithms are needed for the analysis of programs
interacting with an environment, for multi-threaded programs, and for
real-time programs. On the specification
side, the current specification language LTL needs to be extended to the
branching time logic CTL* with past operators, and to specification
languages allowing to deal with quantitative properties.
The goal of the project is to develop these algorithms, implement them
in Moped, and test them on real code using case studies of the projects
mentioned above.
Implementations
Moped -
the basic tool for model-checking pushdown systems (mainly developed before start of the project)
nMoped -
new Moped implementation with Remopla as input language and CEGAR approach
BnddWpds -
reachability analysis for Presburger pushdown systems (pushdown systems with affine relations)
Publications
2006
Dejvuth Suwimonteerabuth, Stefan Schwoon, and Javier Esparza. Efficient algorithms for alternating pushdown systems: Application to certificate chain discovery with threshold subjects. Technical report, Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, 2006. Submitted for publication.
Michael Luttenberger. Reachability analysis of procedural programs with affine integer arithmetic. In Proceedings of the 11th International Conference on Implementation and Application of Automata, 2006. Accepted for publication.
Somesh Jha, Stefan Schwoon, Hao Wang, and Thomas Reps. Weighted pushdown systems and trust-management systems. In Holger Hermanns and Jens Palsberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of Lecture Notes in Computer Science, pages 1–26, Vienna, Austria, 2006. Springer. Invited paper.
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In Holger Hermanns and Jens Palsberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of Lecture Notes in Computer Science, pages 489–503, Vienna, Austria, 2006.
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček. Reachability analysis of multithreaded software with asynchronous communication. In Ramaswamy Ramanujam and Sandeep Sen, editors, Proceedings of FSTTCS 2005, volume 3821 of Lecture Notes in Computer Science. Springer, December 2005.
Thomas Reps, Stefan Schwoon, Somesh Jha, and David Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming, 58(1–2):206–263, October 2005.
Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms. In Nicolas Halbwachs and Lenore Zuck, editors, Proceedings of the 11th International Conference on Tools and Algorithms for the Const ruction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 174–190, Edinburgh, UK, April 2005. Springer.
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005.
Javier Esparza, Antonín Kučera, and Richard Mayr. Quantitative analysis of probabilistic pushdown automata: Expectations and variances. In LICS 2005, pages 117–126. IEEE Computer Society, 2005.
Tomáš Brádzil, Antonín Kučera, and Javier Esparza. Analysis and prediction of the long-run behaviour of probabilstic sequential programs with recursion. In Proceedings of FOCS 2005, pages 521–530, 2005.
Javier Esparza and Kousha Etessami. Verifying probabilistic procedural programs. In Proceedings of FSTTCS 2004, volume 3328 of LNCS, Lecture Notes in Computer Science, pages 16–31, 2004.
sk) |
© University of Stuttgart |
legal notice