Documents
Research Publications
Extrapolation-based Path Invariants
07/12/2010 02:23 pm
Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems¶
Alexander Heußner, Tristan Le Gall, Grégoire Sutre: "Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems", in Corina Păsăreanu (ed.): Proceedings of the 16th Int. Workshop on Model Checking of Software (SPIN 2009), Grenoble, June 2009, LNCS 5578, pp. 107–124, Springer 2009
...
Extrapolation-based Path Invariants (long version)
07/15/2011 11:14 am
Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems¶
Alexander Heußner, Tristan Le Gall, Grégoire Sutre: "Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems", LaBRI Rapport de Recherche RR-1459-09, Mai 2009
...
Global State Estimates for Distributed Systems
08/31/2011 06:14 pm
Global State Estimates for Distributed Systems¶
G. Kalyon, T. Le Gall, H. Marchand, T. Massart: "Global State Estimates for Distributed Systems", in 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE, Reykjavik, Iceland, June 2011.
...
The McScM Framework
04/18/2012 02:03 pm
The McScM Framework¶
Heußner, A.; Gall, T. L. & Sutre, G. McScM: A General Framework for the Verification of Communicating Machines Proc. of TACAS'12, Springer, 2012, 7214, 478-484
abstract¶
We present McScM, a platform for implementing and comparing verification algorithms for the class of finite-state processes exchanging messages over reliable, unbounded FIFO channels. McScM provides tools for the safety verification and controller synthesis of these infinite-state models. Our verification tool implements several model-checking techniques: CEGAR with different abstraction-refinement methods, abstract interpretation, abstract regular model checking, and lazy abstraction. Seen as a general framework for the class of transition systems with finite control/infinite data, McScM delivers the basic infrastructure for implementing verification algorithms, and privileges to conveniently implement new ideas on a high level of abstraction. It also allows us to compare and benchmark different algorithmic approaches with the same backend.
...