11 citations · 19 across the 5 of their papers we have counts for
5 papers
Low Cost High Integrity Platform
Thierry Lecomte, David Deharbe, Denis Sabatier +6
Developing safety critical applications often require rare human resources to complete successfully while off-the-shelf block solutions appear difficult to adapt especially during…
FAR-Cubicle - A new reachability algorithm for Cubicle
Sylvain Conchon, Amit Goel, Sava Krstic +2
We present a fully automatic algorithm for verifying safety properties of parameterized software systems. This algorithm is based on both IC3 and Lazy Annotation. We implemented it…
Parameterized Model Checking Modulo Explicit Weak Memory Models
Sylvain Conchon, David Declerck, Fatiha Zaïdi
We present a modular framework for model checking parameterized array-based transition systems with explicit access operations on weak memory. Our approach extends the MCMT (Model…
AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo
Sylvain Conchon, Mohamed Iguernlala, Alain Mebsout
Due to undecidability and complexity of first-order logic, SMT solvers may not terminate on some problems or require a very long time. When this happens, one would like to find the…
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala
AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm…