Inria
Inria.fr
Inria Channel
- Présentation
- Publications HAL
- Rapports d'activité
Equipe de recherche VERIDIS
Publications de l'équipe VERIDIS
2012
Communications avec actes
- Titre
- TLA+ Proofs
- Auteurs
- Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz
; Daniel Ricketts; Hernán Vanzetto - Détail
- Dimitra Giannakopoulou and Dominique Méry. 18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. Springer, FM 2012: Formal Methods 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, 7436, pp. 147-154, Lecture Notes in Computer Science
- Accès au bibtex
-
- Titre
- SMT solvers for Rodin
- Auteurs
- David Déharbe; Pascal Fontaine ; Yoann Guyot; Laurent Voisin
- Détail
- John Derrick and John A. Fitzgerald and Stefania Gnesi and Sarfraz Khurshid and Michael Leuschel and Steve Reeves and Elvinia Riccobene. ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. Springer, Abstract State Machines, Alloy, B, VDM, and Z Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, 7316, pp. 194-207, Lecture Notes in Computer Science
- Accès au bibtex
-
- Titre
- Combination of disjoint theories: beyond decidability
- Auteurs
- Pascal Fontaine ; Stephan Merz; Christoph Weidenbach
- Détail
- Bernhard Gramlich and Dale Miller and Uli Sattler. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. Springer, Automated Reasoning 6th International Joint Conference, IJCAR 2012, 7364, pp. 256-270, Lecture Notes in Computer Science
- Accès au bibtex
-
Communications sans actes
- Titre
- TLA+ Proofs
- Auteurs
- Denis Cousineau; Damien Doligez; Leslie Lamport; Stephan Merz ; Daniel Ricketts; Hernán Vanzetto
- Détail
- AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p.
- Accès au bibtex
-
2011
Communications avec actes
- Titre
- Formal Verification of Consensus Algorithms Tolerating Malicious Faults
- Auteurs
- Bernadette Charron-Bost; Henri Debrat; Stephan Merz
- Détail
- Xavier Défago and Franck Petit and Vincent Villain. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer, Stabilization, Safety, and Security of Distributed Systems, 6976, pp. 120-134, Lecture Notes in Computer Science
- Accès au texte intégral et bibtex
-
- Titre
- Exploiting Symmetry in SMT Problems
- Auteurs
- David Déharbe; Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo
- Détail
- Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans. International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. Springer, 23rd International Conference on Automated Deduction - CADE 23, 6803, pp. 222-236, Lecture Notes in Computer Science
- Accès au bibtex
-
- Titre
- Compression of Propositional Resolution Proofs via Partial Regularization
- Auteurs
- Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo
- Détail
- Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. Springer, CADE, 6803, pp. 237-251, Lecture Notes in Computer Science
- Accès au bibtex
-
- Titre
- Atomic Cut Introduction by Resolution: Proof Structuring and Compression
- Auteurs
- Bruno Woltzenlogel Paleo
- Détail
- Edmund M. Clarke and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Apr 2010, Dakar, Senegal. Springer, 6355, pp. 463-480, 2011, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence
- Accès au texte intégral et bibtex
-
- Titre
- SimGrid MC: Verification Support for a Multi-API Simulation Platform
- Auteurs
- Stephan Merz; Martin Quinson; Cristian Rosa
- Détail
- Roberto Bruni and Juergen Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. Springer, Proceedings of Formal Techniques for Distributed Systems Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 30th IFIP WG 6.1 International Conference - FORTE 2011, 6722, pp. 274-288, Lecture Notes in Computer Science
- Accès au bibtex
-
- Titre
- Towards Verification of the Pastry Protocol using TLA+
- Auteurs
- Stephan Merz; Tianxiang Lu; Christoph Weidenbach
- Détail
- R. Bruni and J. Dingel. 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland. FMOODS/FORTE 2011, 6722
- Accès au bibtex
-
- Titre
- Combining theories: the Ackerman and Guarded Fragments
- Auteurs
- Carlos Areces; Pascal Fontaine
- Détail
- Cesare Tinelli and Viorica Sofronie-Stokkermans. 8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Oct 2011, Saarbrücken, Germany. Springer Verlag, Frontiers of Combining Systems, 6989, pp. 40-54, Lecture Notes in Computer Science
- Accès au bibtex
-
Communications sans actes
- Titre
- A Flexible Proof Format for SMT: a Proposal
- Auteurs
- Frédéric Besson; Pascal Fontaine ; Laurent Théry
- Détail
- Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland.
- Accès au texte intégral et bibtex
-
- Titre
- Towards certification of TLA+ proof obligations with SMT solvers
- Auteurs
- Stephan Merz ; Hernán Vanzetto
- Détail
- Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland.
- Accès au texte intégral et bibtex
-
- Titre
- Quantifier Inference Rules for SMT proofs
- Auteurs
- David Déharbe; Pascal Fontaine ; Bruno Woltzenlogel Paleo
- Détail
- Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland.
- Accès au texte intégral et bibtex
-
Thèses
- Titre
- Fragments de l'arithmétique dans une combinaison de procédures de décision
- Auteurs
- Diego Caminha Barbosa De Oliveira
- Détail
- informatique. Université Nancy II, Mar. 2011. French
- Accès au texte intégral et bibtex
-
2010
Communications avec actes
- Titre
- A High-Level Language for Modeling Algorithms and their Properties
- Auteurs
- Sabina Akhtar; Stephan Merz; Martin Quinson
- Détail
- 13th Brazilian Symposium on Formal Methods - SBMF'2010, Nov 2010, Natal, Brazil.
- Accès au texte intégral et bibtex
-
- Titre
- A Simple Model of Communication APIs Application to Dynamic Partial-order Reduction
- Auteurs
- Cristian Rosa; Stephan Merz; Martin Quinson
- Détail
- 10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Sep 2010, Düsseldorf, Germany.
- Accès au texte intégral et bibtex
-
- Titre
- Model Checking the Pastry Routing Protocol
- Auteurs
- Tianxiang Lu; Stephan Merz; Christoph Weidenbach
- Détail
- Jens Bendisposto and Michael Leuschel and Markus Roggenbach. 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. Universität Düsseldorf, 10th International Workshop Automated Verification of Critical Systems, pp. 19-21
- Accès au texte intégral et bibtex
-
- Titre
- Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms
- Auteurs
- Sabina Akhtar; Stephan Merz; Martin Quinson
- Détail
- Eric Cariou, Laurence Duchien, Yves Ledru. Actes des deuxièmes journées nationales du Groupement De Recherche CNRS du Génie de la Programmation et du Logiciel, Mar 2010, Pau, France.
- Accès au texte intégral et bibtex
-
- Titre
- System Description: The Proof Transformation System CERES
- Auteurs
- Tsvetan Dunchev; Alexander Leitsch; Tomer Libal; Daniel Weller; Bruno Woltzenlogel Paleo
- Détail
- Jürgen Giesl and Reiner Hähnle. International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp. 427-433, Lecture Notes in Computer Science / Lecture Notes in ArtificiaI Intelligence
- Accès au texte intégral et bibtex
-
- Titre
- Verifying Safety Properties With the TLA+ Proof System
- Auteurs
- Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz
- Détail
- Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, Automated Reasoning 5th International Joint Conference, IJCAR 2010 Edinburgh, UK, July 16-19, 2010 Proceedings, 6173, pp. 142-148, Lecture Notes in Artificial Intelligence
- Accès au texte intégral et bibtex
-
Communications sans actes
- Titre
- Physics and Proof Theory
- Auteurs
- Bruno Woltzenlogel Paleo
- Détail
- International Workshop on Physics and Computation, Aug 2010, Luxor, Egypt.
- Accès au texte intégral et bibtex
-
- Titre
- Exploring and Exploiting Algebraic and Graphical Properties of Resolution
- Auteurs
- Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo
- Détail
- 8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom.
- Accès au texte intégral et bibtex
-
- Titre
- Using Proofs to Compute Implicatures Abstract
- Auteurs
- Bruno Woltzenlogel Paleo; Ekaterina Lebedeva
- Détail
- Computability in Europe, Jun 2010, Ponta Delgada, Portugal.
- Accès au bibtex
-
- Titre
- Proof Compression with the CIRes Method Abstract
- Auteurs
- Bruno Woltzenlogel Paleo
- Détail
- Computability in Europa, Jun 2010, Ponta Delgada, Portugal.
- Accès au bibtex
-
- Titre
- Formal Verification of Consensus Algorithms in a Proof Assistant
- Auteurs
- Henri Debrat; Bernadette Charron-Bost; Stephan Merz
- Détail
- Michael Backes and Ralf Küsters. 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany.
- Accès au texte intégral et bibtex
-
Directions d'ouvrages
- Titre
- Integrated Formal Methods
- Auteurs
- Dominique Méry; Stephan Merz
- Détail
- Dominique Méry and Stephan Merz. 6396, Springer, pp. 335, Oct. 2010, Lecture Notes in Computer Science, 978-3-642-16264-0
- Accès au bibtex
-
Archives
En savoir plus
Retrouvez toutes les publications scientifiques de nos équipes de recherche sur HAL Inria
Voir aussi
