papers
Publications (11)
cs.PL2014
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
Jingshu Chen, Marie Duflot, Stephan Merz
cs.LO2005
Truly On-The-Fly LTL Model Checking
Moritz Hammer, Alexander Knapp, Stephan Merz
cs.LO2018
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
Ran Chen, Cyril Cohen, Jean-Jacques Levy +2
cs.SE2012
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport +3
cs.LO2010
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport +1
cs.LO2014
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Damien Doligez, Jael Kriener, Leslie Lamport +2
cs.LO2009
A Formalization of the Semantics of Functional-Logic Programming in Isabelle
Francisco López Fraguas, Stephan Merz, Juan RodrÃguez Hortalá
cs.LO2006
Event Systems and Access Control
Dominique Méry, Stephan Merz
cs.LO2015
Encoding TLA+ set theory into many-sorted first-order logic
Stephan Merz, Hernán Vanzetto
cs.LO2008
A TLA+ Proof System
Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport +1
cs.LO2017
Auxiliary Variables in TLA+
Leslie Lamport, Stephan Merz