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.
...