2022
Journal articles
- titre
- Prophecy Made Simple
- auteur
- Leslie Lamport, Stephan Merz
- article
- ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, 44 (2), pp.1-27. ⟨10.1145/3492545⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
- auteur
- Igor Konnov, Markus Kuppe, Stephan Merz
- article
- Leveraging Applications of Formal Methods, Verification and Validation. 11th International Symposium, ISoLA 2022, 2022, Rhodes, Greece. pp.88-105, ⟨10.1007/978-3-031-19849-6_6⟩
- Accès au texte intégral et bibtex
-
2021
Conference papers
- titre
- Synchronization Modulo k in Dynamic Networks
- auteur
- Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
- article
- SSS 2021 - International Symposium on Stabilizing, Safety, and Security of Distributed Systems, Nov 2021, Virtual Event, France. pp.425-439, ⟨10.1007/978-3-030-91081-5_28⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Automated Orchestration of Security Chains Driven by Process Learning
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- Communication Networks and Service Management in the Era of Artificial Intelligence and Machine Learning, Wiley, 2021, 978-1-119-67550-1. ⟨10.1002/9781119675525.ch12⟩
- Accès au bibtex
-
2020
Conference papers
- titre
- An Extension of PlusCal for Modeling Distributed Algorithms
- auteur
- Heba Alkayed, Horatiu Cirstea, Stephan Merz
- article
- TLA+ Community Event 2020, Oct 2020, Freiburg (online), Germany
- Accès au texte intégral et bibtex
-
2019
Journal articles
- titre
- Selected Extended Papers of ITP 2016: Preface
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- article
- Journal of Automated Reasoning, 2019, 62 (2), pp.169-170. ⟨10.1007/s10817-018-9470-8⟩
- Accès au texte intégral et bibtex
-
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- Electronic Communications of the EASST, 2019, 076, ⟨10.14279/tuj.eceasst.76.1075.1042⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Integrating satisfiability solving in the assessment of system reliability modeled by dynamic fault trees
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- article
- 29th European Safety and Reliability Conference, ESREL 2019, Sep 2019, Hannover, Germany. ⟨10.3850/981-973-0000-00-0⟩
- Accès au texte intégral et bibtex
-
- titre
- Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry
- article
- ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
- Accès au texte intégral et bibtex
-
- titre
- Automated Factorization of Security Chains in Software-Defined Networks
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- IFIP/IEEE IM 2019 - IFIP/IEEE International Symposium on Integrated Network Management, Apr 2019, Washington, United States
- Accès au texte intégral et bibtex
-
- titre
- A Tool Suite for the Automated Synthesis of Security Function Chains
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- IFIP/IEEE IM 2019 - IFIP/IEEE International Symposium on Integrated Network Management, Apr 2019, Washington, United States
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Formal specification and verification
- auteur
- Stephan Merz
- article
- Dahlia Malkhi. Concurrency: the Works of Leslie Lamport, 29, Association for Computing Machinery, pp.103-129, 2019, ACM Books, ⟨10.1145/3335772.3335780⟩
- Accès au texte intégral et bibtex
-
2018
Journal articles
- titre
- A Machine-Checked Correctness Proof for Pastry
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- article
- Science of Computer Programming, 2018, 158, pp.64-80. ⟨10.1016/j.scico.2017.08.003⟩
- Accès au texte intégral et bibtex
-
- titre
- Encoding TLA+ into unsorted and many-sorted first-order logic
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- Science of Computer Programming, 2018, 158, pp.3-20. ⟨10.1016/j.scico.2017.09.004⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks
- auteur
- Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- AVOCS 2018 - 18th International Workshop on Automated Verification of Critical Systems, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Generation of SDN policies for protecting Android environments based on automata learning
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- NOMS 2018 - IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, Taiwan. ⟨10.1109/NOMS.2018.8406153⟩
- Accès au texte intégral et bibtex
-
- titre
- Synaptic: A formal checker for SDN-based security policies
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- NOMS 2018 - IEEE/IFIP Network Operations and Management Symposium, Apr 2018, Taipei, Taiwan. ⟨10.1109/NOMS.2018.8406122⟩
- Accès au texte intégral et bibtex
-
Documents associated with scientific events
- titre
- Model Checking of Fault-Tolerant Distributed Algorithms: from Classics towards Contemporary
- auteur
- Igor Konnov, Stephan Merz
- article
- BCRB 2018 - DSN Workshop on Byzantine Consensus and Resilient Blockchains, Jun 2018, Luxembourg, Luxembourg
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
- auteur
- Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery
- article
- 2018
- Accès au texte intégral et bibtex
-
2017
Conference papers
- titre
- Satisfiability techniques for computing minimal tie sets in reliability assessment
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- article
- 10th International Conference on Mathematical Methods in Reliability, MMR 2017, Jul 2017, Grenoble, France. pp.1-8
- Accès au texte intégral et bibtex
-
- titre
- Automated Verification of Security Chains in Software-Defined Networks with Synaptic
- auteur
- Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi, Stephan Merz
- article
- NetSoft 2017 - IEEE Conference on Network Softwarization, Jul 2017, Bologna, Italy. 9pp., ⟨10.1109/NETSOFT.2017.8004195⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- Auxiliary Variables in TLA+
- auteur
- Leslie Lamport, Stephan Merz
- article
- [Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Satisfiability techniques for computing minimal tie sets in reliability assessment
- auteur
- Margaux Duroeulx, Nicolae Brinzei, Marie Duflot, Stephan Merz
- article
- 2017
- Accès au texte intégral et bibtex
-
2016
Journal articles
- titre
- Editorial
- auteur
- Stephan Merz, Jun Pang
- article
- Formal Aspects of Computing, 2016, Formal Engineering Methods (vol.1), 28 (3), pp.343-344. ⟨10.1007/s00165-016-0378-y⟩
- Accès au bibtex
-
- titre
- Editorial
- auteur
- Stephan Merz, Jun Pang
- article
- Formal Aspects of Computing, 2016, Formal Engineering Methods (vol.2), 28 (5), pp.723-724. ⟨10.1007/s00165-016-0390-2⟩
- Accès au bibtex
-
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
-
- titre
- A Rigorous Correctness Proof for Pastry
- auteur
- Noran Azmy, Stephan Merz, Christoph Weidenbach
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.86-101, ⟨10.1007/978-3-319-33600-8_5⟩
- Accès au texte intégral et bibtex
-
- titre
- Encoding TLA+ into Many-Sorted First-Order Logic
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, 2016, Linz, Austria. pp.54-69, ⟨10.1007/978-3-319-33600-8_3⟩
- Accès au texte intégral et bibtex
-
Books
- titre
- Interactive Theorem Proving
- auteur
- Jasmin Christian Blanchette, Stephan Merz
- article
- Springer, 9807, 2016, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-43144-4⟩
- Accès au bibtex
-
2015
Conference papers
- titre
- Software Component Design with the B Method — A Formalization in Isabelle/HOL
- auteur
- David Déharbe, Stephan Merz
- article
- Formal Aspects of Component Software - 12th International Conference, FACS 2015, Oct 2015, Niterói, Brazil. pp.31-47, ⟨10.1007/978-3-319-28934-2_2⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Modal Satisfiability via SMT Solving
- auteur
- Carlos Areces, Pascal Fontaine, Stephan Merz
- article
- Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-15545-6_5⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- Encoding TLA+ set theory into many-sorted first-order logic
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- 2015
- Accès au texte intégral et bibtex
-
2014
Journal articles
- titre
- Editorial: Special Issue of Automated Verification of Critical Systems
- auteur
- Gerald Lüttgen, Stephan Merz
- article
- Science of Computer Programming, 2014, Special Issue: Automated Verification of Critical Systems, 96 (3), pp.277-278
- Accès au bibtex
-
- titre
- Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
- auteur
- Jingshu Chen, Marie Duflot, Stephan Merz
- article
- Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14
- Accès au texte intégral et bibtex
-
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
-
- titre
- Proof-by-Instance for Embedded Network Design
- auteur
- Marc Boyer, Loïc Fejoz, Stephan Merz
- article
- Embedded real-time software and systems (ERTS² 2014), Feb 2014, TOULOUSE, France
- Accès au texte intégral et bibtex
-
- titre
- Refinement Types for TLA+
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩
- Accès au bibtex
-
Books
- titre
- Science of Computer Programming Special Issue: Automated Verification of Critical Systems
- auteur
- Gerald Lüttgen, Stephan Merz
- article
- Elsevier, 96 (3), 2014, Science of Computer Programming, Jan Bergstra
- Accès au bibtex
-
Proceedings
- titre
- Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods (ICFEM 2014)
- auteur
- Stephan Merz, Jun Pang
- article
- Stephan Merz; Jun Pang. 16th International Conference on Formal Engineering Methods - ICFEM 2014, Nov 2014, Luxembourg, Luxembourg. 8829, Springer, pp.460, 2014, LNCS - Lecture Notes in Computer Science, 978-3-319-11737-9. ⟨10.1007/978-3-319-11737-9⟩
- Accès au bibtex
-
2013
Conference papers
- titre
- Towards Certifying Network Calculus
- auteur
- Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
- article
- ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.484-489, ⟨10.1007/978-3-642-39634-2_37⟩
- Accès au texte intégral et bibtex
-
- titre
- Certifying Network Calculus in a Proof Assistant
- auteur
- Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz
- article
- EUCASS - 5th European Conference for Aeronautics and Space Sciences, Astrium and Technische Universität München, Jul 2013, Munich, Germany
- Accès au texte intégral et bibtex
-
Books
- titre
- Formal Verification of Distributed Algorithms
- auteur
- Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
- article
- Bernadette Charron-Bost and Stephan Merz and Andrey Rybalchenko and Josef Widder. Dagstuhl, 3, pp.16, 2013, Dagstuhl Reports, ⟨10.4230/DagRep.3.4.1⟩
- Accès au bibtex
-
2012
Conference papers
- titre
- Harnessing SMT Solvers for TLA+ Proofs
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Sep 2012, Bamberg, Germany
- Accès au texte intégral et bibtex
-
- titre
- Formal Verification Of Pastry Using TLA+
- auteur
- Tianxiang Lu, Stephan Merz, Christoph Weidenbach
- article
- International Workshop on the TLA+ Method and Tools, Aug 2012, Paris, France
- 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
- 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
-
- titre
- Combination of disjoint theories: beyond decidability
- auteur
- Pascal Fontaine, Stephan Merz, Christoph Weidenbach
- article
- IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. pp.256-270, ⟨10.1007/978-3-642-31365-3_21⟩
- Accès au bibtex
-
- titre
- Automatic Verification Of TLA+ Proof Obligations With SMT Solvers
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), Mar 2012, Mérida, Venezuela. pp.289-303, ⟨10.1007/978-3-642-28717-6_23⟩
- Accès au texte intégral et bibtex
-
Reports
- titre
- Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
- auteur
- Henri Debrat, Stephan Merz
- article
- [Research Report] 2012
- Accès au bibtex
-
- titre
- Stuttering Equivalence
- auteur
- Stephan Merz
- article
- [Research Report] 2012
- Accès au bibtex
-
2011
Conference papers
- titre
- Formal Verification of Consensus Algorithms Tolerating Malicious Faults
- auteur
- Bernadette Charron-Bost, Henri Debrat, Stephan Merz
- article
- 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. pp.120-134, ⟨10.1007/978-3-642-24550-3_11⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards certification of TLA+ proof obligations with SMT solvers
- auteur
- Stephan Merz, Hernán Vanzetto
- article
- First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wroclaw, Poland
- Accès au texte intégral et bibtex
-
- titre
- Compression of Propositional Resolution Proofs via Partial Regularization
- auteur
- Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
- article
- 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. pp.237-251, ⟨10.1007/978-3-642-22438-6_19⟩
- Accès au bibtex
-
- titre
- Exploiting Symmetry in SMT Problems
- auteur
- David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
- article
- International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. pp.222-236, ⟨10.1007/978-3-642-22438-6_18⟩
- Accès au bibtex
-
- titre
- Towards Verification of the Pastry Protocol Using TLA +
- auteur
- Tianxiang Lu, Stephan Merz, Christoph Weidenbach
- article
- 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.244-258, ⟨10.1007/978-3-642-21461-5_16⟩
- Accès au texte intégral et bibtex
-
- titre
- SimGrid MC: Verification Support for a Multi-API Simulation Platform
- auteur
- Stephan Merz, Martin Quinson, Cristian Rosa
- article
- 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.274-288, ⟨10.1007/978-3-642-21461-5_18⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards Verification of the Pastry Protocol using TLA+
- auteur
- Stephan Merz, Tianxiang Lu, Christoph Weidenbach
- article
- 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems, Jun 2011, Reykjavik, Iceland
- Accès au bibtex
-
2010
Journal articles
- titre
- Specifying and Verifying PLC systems with TLA+: a case study
- auteur
- Hehua Zhang, Stephan Merz, Ming Gu
- article
- Computers & Mathematics with Applications, 2010, 60 (3), pp.695-705. ⟨10.1016/j.camwa.2010.05.017⟩
- Accès au bibtex
-
Conference papers
- titre
- A High-Level Language for Modeling Algorithms and their Properties
- auteur
- Sabina Akhtar, Stephan Merz, Martin Quinson
- article
- 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
- auteur
- Cristian Rosa, Stephan Merz, Martin Quinson
- article
- 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
- 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
-
- titre
- Model Checking the Pastry Routing Protocol
- auteur
- Tianxiang Lu, Stephan Merz, Christoph Weidenbach
- article
- 10th International Workshop Automated Verification of Critical Systems, Sep 2010, Düsseldorf, Germany. pp.19-21
- Accès au texte intégral et bibtex
-
- titre
- Verifying Safety Properties With the TLA+ Proof System
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Exploring and Exploiting Algebraic and Graphical Properties of Resolution
- auteur
- Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
- article
- 8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Formal Verification of Consensus Algorithms in a Proof Assistant
- auteur
- Henri Debrat, Bernadette Charron-Bost, Stephan Merz
- article
- 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany
- Accès au texte intégral et bibtex
-
- titre
- Extending PlusCal: A Language for Describing Concurrent and Distributed Algorithms
- auteur
- Sabina Akhtar, Stephan Merz, Martin Quinson
- article
- 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
-
Books
- titre
- Integrated Formal Methods
- auteur
- Dominique Méry, Stephan Merz
- article
- Dominique Méry and Stephan Merz. Springer, 6396, pp.335, 2010, Lecture Notes in Computer Science, 978-3-642-16264-0. ⟨10.1007/978-3-642-16265-7⟩
- Accès au bibtex
-
2009
Journal articles
- titre
- Formal Verification of a Consensus Algorithm in the Heard-Of Model
- auteur
- Bernadette Charron-Bost, Stephan Merz
- article
- International Journal of Software and Informatics (IJSI), 2009, Formal Methods of Program Development, 3 (2-3), pp.273-303
- Accès au bibtex
-
Conference papers
- titre
- A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
- auteur
- Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz
- article
- Reachability Problems 2009, Sep 2009, Palaiseau, France. pp.93-106, ⟨10.1007/978-3-642-04420-5_10⟩
- Accès au bibtex
-
- titre
- A Formalization of the Semantics of Functional-Logic Programming in Isabelle
- auteur
- Francisco López Fraguas, Stephan Merz, Juan Rodríguez Hortalá
- article
- 22nd International Conference on Theorem Proving in Higher-Order Logics : emerging trends session - TPHOLs 2009, Technische Universität München, Aug 2009, Munich, Germany
- Accès au texte intégral et bibtex
-
- titre
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- auteur
- Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
- article
- 22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009, Aug 2009, Munich, Germany. pp.424-439, ⟨10.1007/978-3-642-03359-9_29⟩
- Accès au bibtex
-
- titre
- Automating model-based software engineering
- auteur
- David Déharbe, Pascal Fontaine, Anamaria Martins Moreira, Stephan Merz, Anderson Santana de Oliveira
- article
- Colloque d'Informatique: Brésil/INRIA (COLIBRI), Jul 2009, Bento Gonçalves, Brazil. pp.22-27
- Accès au bibtex
-
- titre
- Model-checking Distributed Applications with GRAS
- auteur
- Cristian Rosa, Martin Quinson, Stephan Merz
- article
- Exploiting Concurrency Efficiently and Correctly - EC2 workshop associated to CAV 2009, Jun 2009, Grenoble, France
- Accès au texte intégral et bibtex
-
Reports
- titre
- Model-checking Distributed Applications with GRAS
- auteur
- Cristian Rosa, Martin Quinson, Stephan Merz
- article
- [Research Report] RR-7052, INRIA. 2009, pp.11
- Accès au texte intégral et bibtex
-
2008
Conference papers
- titre
- Towards automatic proofs of lock-free algorithms
- auteur
- Loïc Fejoz, Stephan Merz
- article
- Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States
- Accès au texte intégral et bibtex
-
- 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
-
Book sections
- titre
- The Specification Language TLA+
- auteur
- Stephan Merz
- article
- Dines Bjoerner and Martin Henson. Logics of specification languages, Springer, pp.401-452, 2008, Monographs in Theoretical Computer Science, 978-3-540-74106-0
- Accès au bibtex
-
- titre
- An introduction to model checking
- auteur
- Stephan Merz
- article
- Stephan Merz and Nicolas Navet. Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, ISTE Publishing, pp.81-116, 2008, 9781847040244
- Accès au bibtex
-
Books
- titre
- Journal of Automated Reasoning Special Issue: Formal Modeling and Verification of Critical Systems
- auteur
- Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow
- article
- Tobias Nipkow. Springer, 41, pp.209, 2008, Journal of Automated Reasoning
- Accès au bibtex
-
- titre
- Modeling and Verification of Real-Time Systems - Formalisms and Software Tools
- auteur
- Stephan Merz, Nicolas Navet
- article
- Stephan Merz and Nicolas Navet. ISTE Publishing, pp.400, 2008, 9781847040244
- Accès au bibtex
-
- titre
- Temporal Logic and State Systems
- auteur
- Fred Kröger, Stephan Merz
- article
- Springer, pp.436, 2008, Texts in Theoretical Computer Science. An EATCS Series, 978-3-540-67401-6
- Accès au bibtex
-
2007
Journal articles
- titre
- Specification and Refinement of Access Control
- auteur
- Dominique Méry, Stephan Merz
- article
- Journal of Universal Computer Science, 2007, 13 (8), pp.1073-1093
- Accès au bibtex
-
- titre
- Predicate Diagrams for the Verification of Real-Time Systems
- auteur
- Eunyoung Kang, Stephan Merz
- article
- Formal Aspects of Computing, 2007, 19 (3), pp.401-413. ⟨10.1007/s00165-007-0030-y⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions
- auteur
- Clément Hurlin, Amine Chaib, Pascal Fontaine, Stephan Merz, Tjark Weber
- article
- The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13
- Accès au bibtex
-
- titre
- Dérivation d'algorithmes sans verrou à partir d'une spécification atomique
- auteur
- Loïc Fejoz, Stephan Merz
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL07, Marie-Laure Potet (IMAG, Grenoble) ; Pierre-Yves Schobbens (Facultés Universitaires Notre-Dame de la Paix - Namur, Belgique), Jun 2007, Namur, Belgique. pp.213-226
- Accès au texte intégral et bibtex
-
Books
- titre
- Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006)
- auteur
- Stephan Merz, Tobias Nipkow
- article
- Michael Mislove. Elsevier, 185, pp.151, 2007, Electronic Notes in Theoretical Computer Science
- Accès au bibtex
-
2006
Journal articles
- titre
- Specification and Refinement of Mobile Systems in MTLA and Mobile UML
- auteur
- Alexander Knapp, Stephan Merz, Martin Wirsing, Julia Zappe
- article
- Theoretical Computer Science, 2006, 351 (2), pp.184--202. ⟨10.1016/j.tcs.2005.09.067⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Transformation of B Specifications into UML Class Diagrams and State Machines
- auteur
- Houda Fekih, Leila Jemni Ben Ayed, Stephan Merz
- article
- 21st Annual ACM Symposium on Applied Computing - SAC 2006, Apr 2006, Dijon, France, pp.1840-1844
- Accès au texte intégral et bibtex
-
- titre
- Event Systems and Access Control
- auteur
- Dominique Méry, Stephan Merz
- article
- Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, Mar 2006, Vienna/Austria, pp.40-54
- Accès au texte intégral et bibtex
-
- titre
- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
- auteur
- Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Tiu
- article
- 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, pp.167-181, ⟨10.1007/11691372_11⟩
- Accès au bibtex
-
Book sections
- titre
- Model checking : éléments de base
- auteur
- Stephan Merz
- article
- Nicolas Navet. Systèmes Temps Réel - techniques de description et de vérification, Hermes-Science Lavoisier, pp.89-120, 2006, 2-7462-1303-6
- Accès au bibtex
-
2005
Conference papers
- titre
- Predicate Diagrams for the Verification of Real-Time Systems
- auteur
- Eunyoung Kang, Stephan Merz
- article
- The Fifth International Workshop on Automated Verification of Critical Systems 2005 - AVoCS'05, Ranko Lazic, Rajagopal Nagarajan, Nikolaos Papanikolaou, Sep 2005, Coventry/UK
- Accès au texte intégral et bibtex
-
- titre
- DIXIT: a Graphical Toolkit for Predicate Abstractions
- auteur
- Loïc Fejoz, Dominique Méry, Stephan Merz
- article
- Fourth International Workshop on Automated Verification of Infinite-State Systems - AVIS'05, Apr 2005, Edinburgh / U.K., pp.39-48
- Accès au texte intégral et bibtex
-
- titre
- Truly On-The-Fly LTL Model Checking
- auteur
- Moritz Hammer, Alexander Knapp, Stephan Merz
- article
- Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Apr 2005, Edinburgh / U.K., pp.191-205
- Accès au texte intégral et bibtex
-
2004
Conference papers
- titre
- Transformation des spécifications B en des diagrammes UML
- auteur
- Houda Fekih, Leila Jemni, Stephan Merz
- article
- Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'2004, Université de Franche-Comté, 2004, Besançon, France, pp.131-145
- Accès au texte intégral et bibtex
-
- titre
- Refining Mobile UML State Machines
- auteur
- Alexander Knapp, Stephan Merz, Martin Wirsing
- article
- 10th International Conference on Algebraic Methodology and Software Technology - AMAST'2004, 2004, Stirling, Scotland, UK, pp.274--288
- Accès au bibtex
-
Reports
- titre
- TLA+ Case Study: A Resource Allocator
- auteur
- Stephan Merz
- article
- [Intern report] A04-R-101 || merz04a, 2004, 20 p
- Accès au texte intégral et bibtex
-
2003
Journal articles
- titre
- On the Logic of TLA+
- auteur
- Stephan Merz
- article
- Computing and Informatics, 2003, 22 (4), 27 p
- Accès au bibtex
-
Conference papers
- titre
- A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems
- auteur
- Stephan Merz, Martin Wirsing, Julia Zappe
- article
- Fundamental Approaches to Software Engineering '03 - FASE 2003, Lecture Notes in Computer Sciences, 2003, Warsaw, Poland, pp.87-101
- Accès au bibtex
-
- titre
- The QSL platform at LORIA
- auteur
- Mohamed El Habib, Claude Kirchner, Hélène Kirchner, Jean-Yves Marion, Stephan Merz
- article
- First QPQ Workshop on Deductive Software Components, 2003, Miami, Floride, 3 p
- Accès au texte intégral et bibtex
-
Reports
- titre
- Translating B machines into UML diagrams
- auteur
- Houda Fekih, Stephan Merz
- article
- [Intern report] A03-R-502 || fekih03a, 2003, 13 p
- Accès au texte intégral et bibtex
-
- titre
- Emptiness of Linear Weak Alternating Automata
- auteur
- Stephan Merz, Ali Sezgin
- article
- [Intern report] A03-R-503 || merz03c, 2003, 14 p
- Accès au texte intégral et bibtex
-
2001
Conference papers
- titre
- Formal Analysis of a Self-Stabilizing Algorithm - Using Predicate Diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Integrating Diagrammatic and Formal Specification Techniques, GI Fachgruppe 0.1.7 Specification and Semantics, 2001, Wien, Austria, pp.39-45
- Accès au bibtex
-
2000
Journal articles
- titre
- Diagrams Refinement for the Design of Reactive Systems
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Journal of Universal Computer Science, 2000, 7 (2), pp.159-174
- Accès au bibtex
-
Conference papers
- titre
- Verifying Reactive Systems Using Predicate Diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- FM-TOOLS'2000, Wolfgang Reif & Gerhard Schellhorn, 2000, Ulm, 5 p
- Accès au bibtex
-
- titre
- Predicate diagrams for the verification of reactive systems
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Second International Conference on Integrated Formal Methods - IFM'2000, 2000, Dagstuhl Castle, Germany, pp.380-397
- Accès au bibtex
-
- titre
- Predicate diagrams
- auteur
- Dominique Cansell, Dominique Méry, Stephan Merz
- article
- Workshop on Requirement, Design, Correct Construction & Verification, M.V. Cengarle, 2000, Munich, Germany
- Accès au bibtex
-
1999
Conference papers
- titre
- Animating TLA Specifications
- auteur
- Yassine Mokhtari, Stephan Merz
- article
- International Conference on Logic for Programming and Automated Reasoning - LPAR'99, Sep 1999, Tbilisi, Georgia, pp.92--110
- Accès au bibtex
-