 |
Members
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 Wisconsin.
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. Algorithms are needed for the analysis of programs
interacting with an environment, for multi-threaded programs.
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
- jMoped -
a Java frontend for Moped
- WPDS -
weighted pushdown library
- BnddWpds -
reachability analysis for Presburger pushdown systems (pushdown systems with affine relations)
Publications
To appear | |
Stefan Kiefer, Michael Luttenberger, and Javier Esparza. On the convergence of Newton's method for monotone systems of polynomial equations. In Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), San Diego, California, USA, to appear. |
|
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. An extension of Newton's method to  -continuous semirings. In Proceedings of the 11th International Conference on Developments in Language Theory (DLT), Lecture Notes in Computer Science, Turku, Finland, to appear. |
|
2007 | |
Javier Esparza, Stefan Kiefer, and Michael Luttenberger. On fixed point equations over commutative semirings. In Wolfgang Thomas and Pascal Weil, editors, Proceedings of the 24th International Symposium on Theoretical Aspects of Computer Science (STACS), volume 4393 of Lecture Notes in Computer Science, pages 296–307, Aachen, Germany, 2007. |
|
2006 | |
A. Bouajjani and J. Esparza. Rewriting models of boolean programs. In Proceedings of RTA 2006, Seattle, USA, 2006. |
|
|
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. In Proceedings of ATVA 2006, Beijing, China, 2006. |
|
|
G. Delzanno, J. Esparza, and J. Srba. Monotonic set-extended prefix rewriting and verification of recursive ping-pong protocols. Technical report, BRICS, 2006. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Logical Methods in Computer Science, 2006. |
|
|
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. |
|
|
Michael Luttenberger. Reachability analysis of procedural programs with affine integer arithmetic. In Oscar H. Ibarra and Hsu-Chun Yen, editors, Proceedings of the 11th Conference on Implementation and Application of Automata, volume 4094 of LNCS, 2006. |
|
|
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. |
|
2005 | |
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, pages 348–359. 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. Special Issue on the Static Analysis Symposium 2003. |
|
|
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 Construction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 174–190, Edinburgh, UK, April 2005. Springer. |
|
|
Tomáš Brádzil, Antonín Kučera, and Javier Esparza. Analysis and prediction of the long-run behaviour of probabilistic sequential programs with recursion. In Proceedings of FOCS 2005, pages 521–530, 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. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Quantitative analysis of probabilistic pushdown automata: Expectations and variances. Technical Report FIMU-RS-2005-07, Masaryk University, 2005. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. Electronic Notes in Theoretical Computer Science, 138(3):153–178, 2005. |
|
|
Stefan Kiefer. Abstraction refinement for pushdown systems. Master's thesis, Universität Stuttgart, 2005. |
|
2004 | |
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. |
|
|
Ahmed Bouajjani, Javier Esparza, and Tayssir Touili. Reachability analysis of synchronized PA-systems. In Proceedings of Infinity 2004, 2004. |
|
|
Javier Esparza, Antonín Kučera, and Richard Mayr. Model checking probabilistic pushdown automata. Technical report, Faculty of Informatics, Masaryk University, Brno, 2004. |
|
|
|
sk) |
© University of Stuttgart |
legal notice