 |
 |
 |
|
|
||
|---|---|---|
|
inria-00338299v1
Conference papers
A TLA+ Proof System Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar |
||
|
hal-01499969v1
Conference papers
A concurrent, generational garbage collector for a multithreaded implementation of ML POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. pp.113-123, ⟨10.1145/158511.158611⟩ |
||
|
hal-01322335v1
Conference papers
Proving Determinacy of the PharOS Real-Time Operating System 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⟩ |
||
|
inria-00521886v1
Conference papers
The TLA+ Proof System: Building a Heterogeneous Verification Platform International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩  |
||
|
hal-00726631v1
Conference papers
TLA+ Proofs 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩ |
||
|
hal-00726632v1
Conference papers
TLA+ Proofs AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p |
||
|
hal-01125667v2
Conference papers
Trusted Software within Focal C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. pp.162-179 |
||
|
inria-00315920v1
Conference papers
Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. pp.151-165, ⟨10.1007/978-3-540-75560-9_13⟩ |
||
|
hal-00930213v6
Reports
The OCaml system release 4.09: Documentation and user's manual [Intern report] Inria. 2019, pp.1-789 |
||
|
hal-01801276v1
Reports
Compiling Programs and Proofs: FoCaLiZe Internals [Research Report] Ensta ParisTech. 2018 |
||
|
hal-00909688v1
Conference papers
Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa |
||
|
hal-00909784v1
Conference papers
Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩ |
||
|
hal-01063512v1
Conference papers
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics ARQNL 2014 - Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria |
||
|
hal-00773654v1
Conference papers
Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment. A case study within the FoCaLiZe environment PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Jun 2012, Beijing, China. ⟨10.1145/2336717.2336726⟩ |
||
|
inria-00534821v1
Conference papers
Verifying Safety Properties With the TLA+ Proof System Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142--148, ⟨10.1007/978-3-642-14203-1_12⟩ |
||
|
hal-00297708v2
Preprints, Working Papers, ...
A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking 2008 |
||
|
hal-01204701v2
Conference papers
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58 |
||
|
hal-01244623v1
Conference papers
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. pp.1-16 |
||
|
|
||
