Researchers

2016

Conference papers

titre

Proving Determinacy of the PharOS Real-Time Operating System

auteur

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz

article

Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩

Accès au texte intégral et bibtex

2014

Conference papers

titre

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

auteur

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz

article

ARQNL 2014 - The first International Workshop on Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. pp.1-16

Accès au texte intégral et bibtex

2012

Conference papers

titre

TLA+ Proofs

auteur

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto

article

18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩

Accès au texte intégral et bibtex

titre

TLA+ Proofs

auteur

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto

article

AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p

Accès au bibtex

2010

Conference papers

titre

The TLA+ Proof System: Building a Heterogeneous Verification Platform

auteur

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz

article

International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩

Accès au bibtex

2008

Conference papers

titre

A TLA+ Proof System

auteur

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz

article

Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar

Accès au texte intégral et bibtex