Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. Zbl 1180.68240
Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen |
|
2006
|
Temporal logic and state systems. Zbl 1169.03001
Kröger, Fred; Merz, Stephan |
|
2008
|
A reduction theorem for the verification of round-based distributed algorithms. Zbl 1260.68450
Chaouch-Saad, Mouna; Charron-Bost, Bernadette; Merz, Stephan |
|
2009
|
Decidability and incompleteness results for first-order temporal logics of linear time. Zbl 0790.03019
Merz, Stephan |
|
1992
|
Exploiting symmetry in SMT problems. Zbl 1341.68187
Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno |
|
2011
|
A spatio-temporal logic for the specification and refinement of mobile systems. Zbl 1032.03028
Merz, Stephan; Wirsing, Martin; Zappe, Júlia |
|
2003
|
Compression of propositional resolution proofs via partial regularization. Zbl 1341.68188
Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno |
|
2011
|
Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. Zbl 1252.68196
Schimpf, Alexander; Merz, Stephan; Smaus, Jan-Georg |
|
2009
|
Model checking: A tutorial overview. Zbl 0986.68063
Merz, Stephan |
|
2001
|
Truly on-the-fly LTL model checking. Zbl 1087.68591
Hammer, Moritz; Knapp, Alexander; Merz, Stephan |
|
2005
|
Formal stystems specification. The RPC-memory specification case study. Zbl 1060.68504
|
|
1996
|
Specification and refinement of mobile systems in MTLA and mobile UML. Zbl 1086.68016
Knapp, Alexander; Merz, Stephan; Wirsing, Martin; Zappe, Júlia |
|
2006
|
TLA\(^{ + }\) proofs. Zbl 1372.68168
Cousineau, Denis; Doligez, Damien; Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán |
|
2012
|
A more complete TLA. Zbl 0952.03016
Merz, Stephan |
|
1999
|
Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers. Zbl 1352.68159
Merz, Stephan; Vanzetto, Hernán |
|
2012
|
On the logic of \(\text{TLA}^+\). Zbl 1104.68364
Merz, Stephan |
|
2003
|
Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962
Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent |
|
2019
|
An abstract account of composition. Zbl 1193.68159
Abadi, Martín; Merz, Stephan |
|
1995
|
Modal satisfiability via SMT solving. Zbl 1453.03015
Areces, Carlos; Fontaine, Pascal; Merz, Stephan |
|
2015
|
Weak alternating automata in Isabelle/HOL. Zbl 0974.68090
Merz, Stephan |
|
2000
|
Diagram refinements for the design of reactive systems. Zbl 0970.68103
Cansell, Dominique; Mery, Dominique; Merz, Stephan |
|
2001
|
On TLA as a logic. Zbl 0855.03019
Abadi, Martín; Merz, Stephan |
|
1996
|
Towards certifying network calculus. Zbl 1317.68220
Mabille, Etienne; Boyer, Marc; Fejoz, Loïc; Merz, Stephan |
|
2013
|
Temporal logic as a programming language. Zbl 0864.03022
Merz, Stephan |
|
1992
|
Combination of disjoint theories: beyond decidability. Zbl 1358.68253
Fontaine, Pascal; Merz, Stephan; Weidenbach, Christoph |
|
2012
|
Synchronization modulo \(k\) in dynamic networks. Zbl 1521.68019
de Monterno, Louis Penet; Charron-Bost, Bernadette; Merz, Stephan |
|
2021
|
Synchronization modulo \(k\) in dynamic networks. Zbl 1521.68019
de Monterno, Louis Penet; Charron-Bost, Bernadette; Merz, Stephan |
|
2021
|
Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. Zbl 07649962
Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent |
|
2019
|
Modal satisfiability via SMT solving. Zbl 1453.03015
Areces, Carlos; Fontaine, Pascal; Merz, Stephan |
|
2015
|
Towards certifying network calculus. Zbl 1317.68220
Mabille, Etienne; Boyer, Marc; Fejoz, Loïc; Merz, Stephan |
|
2013
|
TLA\(^{ + }\) proofs. Zbl 1372.68168
Cousineau, Denis; Doligez, Damien; Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán |
|
2012
|
Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers. Zbl 1352.68159
Merz, Stephan; Vanzetto, Hernán |
|
2012
|
Combination of disjoint theories: beyond decidability. Zbl 1358.68253
Fontaine, Pascal; Merz, Stephan; Weidenbach, Christoph |
|
2012
|
Exploiting symmetry in SMT problems. Zbl 1341.68187
Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno |
|
2011
|
Compression of propositional resolution proofs via partial regularization. Zbl 1341.68188
Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno |
|
2011
|
A reduction theorem for the verification of round-based distributed algorithms. Zbl 1260.68450
Chaouch-Saad, Mouna; Charron-Bost, Bernadette; Merz, Stephan |
|
2009
|
Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. Zbl 1252.68196
Schimpf, Alexander; Merz, Stephan; Smaus, Jan-Georg |
|
2009
|
Temporal logic and state systems. Zbl 1169.03001
Kröger, Fred; Merz, Stephan |
|
2008
|
Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. Zbl 1180.68240
Fontaine, Pascal; Marion, Jean-Yves; Merz, Stephan; Nieto, Leonor Prensa; Tiu, Alwen |
|
2006
|
Specification and refinement of mobile systems in MTLA and mobile UML. Zbl 1086.68016
Knapp, Alexander; Merz, Stephan; Wirsing, Martin; Zappe, Júlia |
|
2006
|
Truly on-the-fly LTL model checking. Zbl 1087.68591
Hammer, Moritz; Knapp, Alexander; Merz, Stephan |
|
2005
|
A spatio-temporal logic for the specification and refinement of mobile systems. Zbl 1032.03028
Merz, Stephan; Wirsing, Martin; Zappe, Júlia |
|
2003
|
On the logic of \(\text{TLA}^+\). Zbl 1104.68364
Merz, Stephan |
|
2003
|
Model checking: A tutorial overview. Zbl 0986.68063
Merz, Stephan |
|
2001
|
Diagram refinements for the design of reactive systems. Zbl 0970.68103
Cansell, Dominique; Mery, Dominique; Merz, Stephan |
|
2001
|
Weak alternating automata in Isabelle/HOL. Zbl 0974.68090
Merz, Stephan |
|
2000
|
A more complete TLA. Zbl 0952.03016
Merz, Stephan |
|
1999
|
Formal stystems specification. The RPC-memory specification case study. Zbl 1060.68504
|
|
1996
|
On TLA as a logic. Zbl 0855.03019
Abadi, Martín; Merz, Stephan |
|
1996
|
An abstract account of composition. Zbl 1193.68159
Abadi, Martín; Merz, Stephan |
|
1995
|
Decidability and incompleteness results for first-order temporal logics of linear time. Zbl 0790.03019
Merz, Stephan |
|
1992
|
Temporal logic as a programming language. Zbl 0864.03022
Merz, Stephan |
|
1992
|