Stephan Merz - RankMe

119 papers A* 1A 6B 17C 8Misc 2Journal 44Unranked 35

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Reconstruction of SMT proofs with Lambdapi. Acta Informatica Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
2025	—	`conf`	Checking Linear Integer Arithmetic Proofs in Lambdapi. FroCoS Alessio Coltellacci, Stephan Merz
2024	—	`conf`	Reconstruction of SMT Proofs with Lambdapi. SMT@CAV Alessio Coltellacci, Stephan Merz, Gilles Dowek
2024	—	`conf`	Scalable Verification and Validation of Concurrent and Distributed Systems (ScaVeri) (Track Summary). ISoLA (3) Marieke Huisman, Stephan Merz, Cristina Seceleanu
2024	B	`conf`	Validating Traces of Distributed Programs Against TLA SEFM Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz
2024	J	`jnl`	Validating Traces of Distributed Programs Against TLA+ Specifications. CoRR Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz
2023	B	`conf`	Extending PlusCal for Modeling Distributed Algorithms. iFM Horatiu Cirstea, Stephan Merz
2023	J	`jnl`	Synchronization modulo Theor. Comput. Sci. Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
2023	C	`conf`	Towards an Automatic Proof of the Bakery Algorithm. FORTE Aman Goel, Stephan Merz, Karem A. Sakallah
2022	J	`jnl`	Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph. Arch. Formal Proofs Stephan Merz, Vincent Trélat
2022	J	`jnl`	Prophecy Made Simple. ACM Trans. Program. Lang. Syst. Leslie Lamport, Stephan Merz
2022	—	`conf`	Specification and Verification with the TLA ISoLA (1) Igor Konnov, Markus Kuppe, Stephan Merz
2022	J	`jnl`	Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS. CoRR Igor Konnov, Markus Kuppe, Stephan Merz
2021	C	`conf`	Synchronization Modulo k in Dynamic Networks. SSS Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz
2019	B	`conf`	A Tool Suite for the Automated Synthesis of Security Function Chains. IM Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2019	B	`conf`	Automated Factorization of Security Chains in Software-Defined Networks. IM Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2019	B	`conf`	Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
2019	—	`ch.`	Formal specification and verification. Concurrency: the Works of Leslie Lamport Stephan Merz
2019	J	`jnl`	Selected Extended Papers of ITP 2016: Preface. J. Autom. Reason. Jasmin Christian Blanchette, Stephan Merz
2018	J	`jnl`	A machine-checked correctness proof for Pastry. Sci. Comput. Program. Noran Azmy, Stephan Merz, Christoph Weidenbach
2018	J	`jnl`	Encoding TLA Sci. Comput. Program. Stephan Merz, Hernán Vanzetto
2018	J	`jnl`	Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. CoRR Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
2018	B	`conf`	Generation of SDN policies for protecting android environments based on automata learning. NOMS Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2018	J	`jnl`	Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2018	B	`conf`	Synaptic: A formal checker for SDN-based security policies. NOMS Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2017	B	`conf`	Automated verification of security chains in software-defined networks with synaptic. NetSoft Nicolas Schnepf, Remi Badonnel, Abdelkader Lahmadi, Stephan Merz
2017	J	`jnl`	Auxiliary Variables in TLA+. CoRR Leslie Lamport, Stephan Merz
2016	C	`conf`	A Rigorous Correctness Proof for Pastry. ABZ Noran Azmy, Stephan Merz, Christoph Weidenbach
2016	J	`jnl`	Editorial. Formal Aspects Comput. Stephan Merz, Jun Pang, Jin Song Dong
2016	J	`jnl`	Editorial. Formal Aspects Comput. Stephan Merz, Jun Pang, Jin Song Dong
2016	C	`conf`	Encoding TLA ^+ + into Many-Sorted First-Order Logic. ABZ Stephan Merz, Hernán Vanzetto
2016	B	`ed.`	Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings ITP Jasmin Christian Blanchette, Stephan Merz
2016	C	`conf`	Proving Determinacy of the PharOS Real-Time Operating System. ABZ Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
2015	J	`jnl`	Encoding TLA+ set theory into many-sorted first-order logic. CoRR Stephan Merz, Hernán Vanzetto
2015	—	`conf`	Modal Satisfiability via SMT Solving. Software, Services, and Systems Carlos Areces, Pascal Fontaine, Stephan Merz
2015	—	`conf`	Software Component Design with the B Method - A Formalization in Isabelle/HOL. FACS David Déharbe, Stephan Merz
2014	J	`jnl`	Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations. CoRR Jingshu Chen, Marie Duflot, Stephan Merz
2014	J	`jnl`	Analyzing Conflict Freedom for Multi-threaded Programs With Time Annotations. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Jingshu Chen, Marie Duflot, Stephan Merz
2014	—	`conf`	Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. ARQNL@IJCAR Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
2014	J	`jnl`	Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. CoRR Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz
2014	C	`ed.`	Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings ICFEM Stephan Merz, Jun Pang
2014	—	`conf`	Refinement Types for tla +. NASA Formal Methods Stephan Merz, Hernán Vanzetto
2014	J	`jnl`	Special issue on Automated Verification of Critical Systems (AVoCS'12). Sci. Comput. Program. Gerald Lüttgen, Stephan Merz
2013	J	`jnl`	Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141). Dagstuhl Reports Bernadette Charron-Bost, Stephan Merz, Andrey Rybalchenko, Josef Widder
2013	B	`conf`	Towards Certifying Network Calculus. ITP Etienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz
2012	B	`conf`	Automatic Verification of TLA + Proof Obligations with SMT Solvers. LPAR Stephan Merz, Hernán Vanzetto
2012	A	`conf`	Combination of Disjoint Theories: Beyond Decidability. IJCAR Pascal Fontaine, Stephan Merz, Christoph Weidenbach
2012	J	`jnl`	Harnessing SMT Solvers for TLA+ Proofs. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Stephan Merz, Hernán Vanzetto
2012	J	`jnl`	Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Gerald Lüttgen, Stephan Merz
2012	—	`conf`	Proofs and Proof Certification in the TLA PxTP Stephan Merz
2012	J	`jnl`	Stuttering Equivalence. Arch. Formal Proofs Stephan Merz
2012	B	`conf`	TLA + Proofs. FM Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
2012	J	`jnl`	TLA+ Proofs CoRR Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto
2012	J	`jnl`	Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model. Arch. Formal Proofs Henri Debrat, Stephan Merz
2011	J	`jnl`	A Definitional Encoding of TLA* in Isabelle/HOL. Arch. Formal Proofs Gudmund Grov, Stephan Merz
2011	A	`conf`	Compression of Propositional Resolution Proofs via Partial Regularization. CADE Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
2011	A	`conf`	Exploiting Symmetry in SMT Problems. CADE David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
2011	C	`conf`	Formal Verification of Consensus Algorithms Tolerating Malicious Faults. SSS Bernadette Charron-Bost, Henri Debrat, Stephan Merz
2011	—	`conf`	SimGrid MC: Verification Support for a Multi-API Simulation Platform. FMOODS/FORTE Stephan Merz, Martin Quinson, Cristian Daniel Rosa
2011	—	`conf`	Towards Verification of the Pastry Protocol Using TLA FMOODS/FORTE Tianxiang Lu, Stephan Merz, Christoph Weidenbach
2011	—	`conf`	Towards certification of TLA+ proof obligations with SMT solvers. PxTP Stephan Merz, Hernán Vanzetto
2010	—	`conf`	A High-Level Language for Modeling Algorithms and Their Properties. SBMF Sabina Akhtar, Stephan Merz, Martin Quinson
2010	J	`jnl`	A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Cristian Daniel Rosa, Stephan Merz, Martin Quinson
2010	B	`ed.`	Integrated Formal Methods - 8th International Conference, IFM 2010, Nancy, France, October 11-14, 2010. Proceedings IFM Dominique Méry, Stephan Merz
2010	J	`jnl`	Specifying and verifying PLC systems with TLA Comput. Math. Appl. Hehua Zhang, Stephan Merz, Ming Gu
2010	C	`conf`	The TLA ICTAC Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2010	J	`jnl`	Verifying Safety Properties With the TLA+ Proof System CoRR Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2010	A	`conf`	Verifying Safety Properties with the TLA+ Proof System. IJCAR Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2009	J	`jnl`	A Formalization of the Semantics of Functional-Logic Programming in Isabelle CoRR Francisco Javier López-Fraguas, Stephan Merz, Juan Rodríguez-Hortalá
2009	—	`conf`	A Reduction Theorem for the Verification of Round-Based Distributed Algorithms. RP Mouna Chaouch-Saad, Bernadette Charron-Bost, Stephan Merz
2009	—	`conf`	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. TPHOLs Alexander Schimpf, Stephan Merz, Jan-Georg Smaus
2009	J	`jnl`	Formal Verification of a Consensus Algorithm in the Heard-Of Model. Int. J. Softw. Informatics Bernadette Charron-Bost, Stephan Merz
2009	Misc	`conf`	Specifying and Verifying PLC Systems with TLA+. TASE Hehua Zhang, Stephan Merz, Ming Gu
2008	J	`jnl`	A TLA+ Proof System CoRR Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2008	—	`conf`	A TLA+ Proof System. LPAR Workshops Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2008	J	`jnl`	Preface. J. Autom. Reason. Serge Autexier, Heiko Mantel, Stephan Merz, Tobias Nipkow
2008	—	`book`	Temporal Logic and State Systems Fred Kröger, Stephan Merz
2007	J	`jnl`	Predicate diagrams for the verification of real-time systems. Formal Aspects Comput. Eun-Young Kang, Stephan Merz
2007	—	`ed.`	Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, AVoCS 2006, Nancy, France, September 18-19, 2006 AVoCS Stephan Merz, Tobias Nipkow
2007	J	`jnl`	Specification and Refinement of Access Control. J. Univers. Comput. Sci. Dominique Méry, Stephan Merz
2006	J	`jnl`	Event Systems and Access Control CoRR Dominique Méry, Stephan Merz
2006	A	`conf`	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. TACAS Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu
2006	—	`conf`	Preface -- Workshop Trustworthy Software 2006. Trustworthy Software Serge Autexier, Stephan Merz, Leendert W. N. van der Torre, Reinhard Wilhelm, Pierre Wolper
2006	—	`conf`	Preface. AVoCS Stephan Merz, Tobias Nipkow
2006	J	`jnl`	Specification and refinement of mobile systems in MTLA and mobile UML. Theor. Comput. Sci. Alexander Knapp, Stephan Merz, Martin Wirsing, Júlia Zappe
2006	Misc	`conf`	Transformation of B specifications into UML class diagrams and state machines. SAC Houda Fekih, Leila Jemni Ben Ayed, Stephan Merz
2006	—	`ed.`	Workshop "Trustworthy Software" 2006, Saarland University, Saarbrücken, Germany, May 18-19, 2006 Trustworthy Software Serge Autexier, Stephan Merz, Leendert W. N. van der Torre, Reinhard Wilhelm, Pierre Wolper
2005	—	`conf`	Predicate Diagrams for the Verification of Real-Time Systems. AVoCS Eun-Young Kang, Stephan Merz
2005	J	`jnl`	Proving the Correctness of Disk Paxos. Arch. Formal Proofs Mauro Jaskelioff, Stephan Merz
2005	J	`jnl`	Truly On-The-Fly LTL Model Checking CoRR Moritz Hammer, Alexander Knapp, Stephan Merz
2005	A	`conf`	Truly On-the-Fly LTL Model Checking. TACAS Moritz Hammer, Alexander Knapp, Stephan Merz
2004	—	`conf`	Refining Mobile UML State Machines. AMAST Alexander Knapp, Stephan Merz, Martin Wirsing
2003	B	`conf`	A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems. FASE Stephan Merz, Martin Wirsing, Júlia Zappe
2003	J	`jnl`	On the Logic of TLA+. Comput. Artif. Intell. Stephan Merz
2002	—	`conf`	Model Checking - Timed UML State Machines and Collaborations. FTRTFT Alexander Knapp, Stephan Merz, Christopher Rauh
2002	J	`jnl`	Model Checking Techniqes for the Analysis of Reactive Systems. Synth. Stephan Merz
2001	J	`jnl`	Diagram Refinements for the Design of Reactive Systems. J. Univers. Comput. Sci. Dominique Cansell, Dominique Méry, Stephan Merz
2001	—	`conf`	Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams. GI Jahrestagung (1) Dominique Cansell, Dominique Méry, Stephan Merz
2001	—	`conf`	Model checking UML state machines and collaborations. Workshop on Software Model Checking @ CAV Timm Schäfer, Alexander Knapp, Stephan Merz
2000	—	`conf`	Model Checking: A Tutorial Overview. MOVEP Stephan Merz
2000	B	`conf`	Predicate Diagrams for the Verification of Reactive Systems. IFM Dominique Cansell, Dominique Méry, Stephan Merz
2000	—	`conf`	Weak Alternating Automata in Isabelle/HOL. TPHOLs Stephan Merz
1999	—	`conf`	A More Complete TLA. World Congress on Formal Methods Stephan Merz
1999	B	`conf`	Animating TLA Specifications. LPAR Yassin Mokhtari, Stephan Merz
1997	—	`conf`	Rules for Abstraction. ASIAN Stephan Merz
1997	A*	`conf`	Type-Checking Higher-Order Polymorphic Multi-Methods. POPL François Bourdoncle, Stephan Merz
1996	—	`ed.`	Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994) Formal Systems Specification Manfred Broy, Stephan Merz, Katharina Spies
1996	—	`conf`	On TLA as a logic. NATO ASI DPD Martín Abadi, Stephan Merz
1995	B	`conf`	An Abstract Account of Composition. MFCS Martín Abadi, Stephan Merz
1995	—	`conf`	Modular Description and Verification of Concurrent Objects. OBPDC Jean Paul Bahsoun, Stephan Merz, Corinne Servieres
1995	—	`conf`	Steam Boiler Control Specification Problem: A TLA Solution. Formal Methods for Industrial Applications Frank Leßke, Stephan Merz
1994	—	`conf`	A TLA Solution to the RPC-Memory Specification Problem. Formal Systems Specification Martín Abadi, Leslie Lamport, Stephan Merz
1994	—	`conf`	Specifying and Verifying Fault-Tolerant Systems. FTRTFT Leslie Lamport, Stephan Merz
1994	—	`conf`	The RPC-Memory Case Study: A Synopsis. Formal Systems Specification Manfred Broy, Stephan Merz, Katharina Spies
1993	—	`conf`	A Framework for Programming and Formalizing Concurrent Objects. SIGSOFT FSE Jean Paul Bahsoun, Stephan Merz, Corinne Servieres
1993	—	`conf`	Efficiently Executable Temporal Logic Programs. Executable Modal and Temporal Logics Stephan Merz
1992	J	`jnl`	Decidability and incompleteness results for first-order temporal logics of linear time. J. Appl. Non Class. Logics Stephan Merz
1992	—	`—`	Temporal logic as a programming language. Stephan Merz
1991	J	`jnl`	Temporal logic and recursion. Fundam. Informaticae Fred Kröger, Stephan Merz