Stephan Merz

Theor. Comput. Sci., 2023

Extending PlusCal for Modeling Distributed Algorithms.

[BibT_eX]

[DOI]

Horatiu Cirstea

Proceedings of the iFM 2023 - 18th International Conference, 2023

Towards an Automatic Proof of the Bakery Algorithm.

[BibT_eX]

[DOI]

Aman Goel

Karem A. Sakallah

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2023

2022

Prophecy Made Simple.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2022

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.

[BibT_eX]

[DOI]

Igor Konnov

Markus Kuppe

CoRR, 2022

Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph.

[BibT_eX]

[DOI]

Vincent Trélat

Arch. Formal Proofs, 2022

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS.

[BibT_eX]

[DOI]

Igor Konnov

Markus Kuppe

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

2021

Synchronization Modulo k in Dynamic Networks.

[BibT_eX]

[DOI]

Louis Penet de Monterno

Jasmin Christian Blanchette

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2021

2019

Selected Extended Papers of ITP 2016: Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

A Tool Suite for the Automated Synthesis of Security Function Chains.

[BibT_eX]

[DOI]

Proceedings of the IFIP/IEEE International Symposium on Integrated Network Management, 2019

Automated Factorization of Security Chains in Software-Defined Networks.

[BibT_eX]

[DOI]

Proceedings of the IFIP/IEEE International Symposium on Integrated Network Management, 2019

Formal specification and verification.

[BibT_eX]

[DOI]

Proceedings of the Concurrency: the Works of Leslie Lamport, 2019

2018

Encoding TLA+ into unsorted and many-sorted first-order logic.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2018

A machine-checked correctness proof for Pastry.

[BibT_eX]

[DOI]

Noran Azmy

Sci. Comput. Program., 2018

Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle.

[BibT_eX]

[DOI]

CoRR, 2018

Generation of SDN policies for protecting android environments based on automata learning.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

Synaptic: A formal checker for SDN-based security policies.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE/IFIP Network Operations and Management Symposium, 2018

2017

Auxiliary Variables in TLA+.

[BibT_eX]

[DOI]

CoRR, 2017

Automated verification of security chains in software-defined networks with synaptic.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE Conference on Network Softwarization, 2017

2016

Editorial.

[BibT_eX]

[DOI]

Jun Pang

Jin Song Dong

Formal Aspects Comput., 2016

Encoding TLA ^+ + into Many-Sorted First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

A Rigorous Correctness Proof for Pastry.

[BibT_eX]

[DOI]

Noran Azmy

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Proving Determinacy of the PharOS Real-Time Operating System.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

2015

Encoding TLA+ set theory into many-sorted first-order logic.

[BibT_eX]

[DOI]

CoRR, 2015

Software Component Design with the B Method - A Formalization in Isabelle/HOL.

[BibT_eX]

[DOI]

David Déharbe

Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

Modal Satisfiability via SMT Solving.

[BibT_eX]

[DOI]

Carlos Areces

Proceedings of the Software, 2015

2014

Special issue on Automated Verification of Critical Systems (AVoCS'12).

[BibT_eX]

[DOI]

Gerald Lüttgen

Sci. Comput. Program., 2014

Analyzing Conflict Freedom for Multi-threaded Programs With Time Annotations.

[BibT_eX]

[DOI]

Jingshu Chen

Marie Duflot

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

Refinement Types for tla +.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

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

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013

Formal Verification of Distributed Algorithms (Dagstuhl Seminar 13141).

[BibT_eX]

[DOI]

Andrey Rybalchenko

Josef Widder

Dagstuhl Reports, 2013

Towards Certifying Network Calculus.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Harnessing SMT Solvers for TLA+ Proofs.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Preface.

[BibT_eX]

[DOI]

Gerald Lüttgen

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Stuttering Equivalence.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2012

Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model.

[BibT_eX]

[DOI]

Henri Debrat

Arch. Formal Proofs, 2012

Proofs and Proof Certification in the TLA+ Proof System.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

Automatic Verification of TLA + Proof Obligations with SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

TLA + Proofs.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Combination of Disjoint Theories: Beyond Decidability.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

A Definitional Encoding of TLA* in Isabelle/HOL.

[BibT_eX]

[DOI]

Gudmund Grov

Arch. Formal Proofs, 2011

Formal Verification of Consensus Algorithms Tolerating Malicious Faults.

[BibT_eX]

[DOI]

Henri Debrat

Proceedings of the Stabilization, Safety, and Security of Distributed Systems, 2011

Towards certification of TLA+ proof obligations with SMT solvers.

[BibT_eX]

[DOI]

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

SimGrid MC: Verification Support for a Multi-API Simulation Platform.

[BibT_eX]

[DOI]

Martin Quinson

Cristian Daniel Rosa

Proceedings of the Formal Techniques for Distributed Systems, 2011

Towards Verification of the Pastry Protocol Using TLA + .

[BibT_eX]

[DOI]

Tianxiang Lu

Proceedings of the Formal Techniques for Distributed Systems, 2011

Compression of Propositional Resolution Proofs via Partial Regularization.

[BibT_eX]

[DOI]

Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Exploiting Symmetry in SMT Problems.

[BibT_eX]

[DOI]

David Déharbe

Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction.

[BibT_eX]

[DOI]

Cristian Daniel Rosa

Martin Quinson

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

Specifying and verifying PLC systems with TLA+ : A case study.

[BibT_eX]

[DOI]

Hehua Zhang

Ming Gu

Comput. Math. Appl., 2010

A High-Level Language for Modeling Algorithms and Their Properties.

[BibT_eX]

[DOI]

Sabina Akhtar

Martin Quinson

Proceedings of the Formal Methods: Foundations and Applications, 2010

The TLA+ Proof System: Building a Heterogeneous Verification Platform.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2010

Verifying Safety Properties with the TLA+ Proof System.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Formal Verification of a Consensus Algorithm in the Heard-Of Model.

[BibT_eX]

[DOI]

Francisco Javier López-Fraguas

Int. J. Softw. Informatics, 2009

A Formalization of the Semantics of Functional-Logic Programming in Isabelle

[BibT_eX]

[DOI]

Juan Rodríguez-Hortalá

CoRR, 2009

Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.

[BibT_eX]

[DOI]

Alexander Schimpf

Jan-Georg Smaus

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Specifying and Verifying PLC Systems with TLA+.

[BibT_eX]

[DOI]

Hehua Zhang

Ming Gu

Proceedings of the TASE 2009, 2009

A Reduction Theorem for the Verification of Round-Based Distributed Algorithms.

[BibT_eX]

[DOI]

Mouna Chaouch-Saad

Proceedings of the Reachability Problems, 3rd International Workshop, 2009

2008

Temporal Logic and State Systems

[BibT_eX]

[DOI]

Fred Kröger

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-68635-4, 2008

Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

A TLA+ Proof System.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2008 Workshops, 2008

2007

Specification and Refinement of Access Control.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2007

Predicate diagrams for the verification of real-time systems.

[BibT_eX]

[DOI]

Eun-Young Kang

Formal Aspects Comput., 2007

2006

Specification and refinement of mobile systems in MTLA and mobile UML.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Preface.

[BibT_eX]

[DOI]

Tobias Nipkow

Proceedings of the 6th International Workshop on Automated Verification of Critical Systems, 2006

Event Systems and Access Control

[BibT_eX]

[DOI]

CoRR, 2006

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Transformation of B specifications into UML class diagrams and state machines.

[BibT_eX]

[DOI]

Houda Fekih

Leila Jemni Ben Ayed

Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

Preface -- Workshop Trustworthy Software 2006.

[BibT_eX]

[DOI]

Serge Autexier

Leendert W. N. van der Torre

Reinhard Wilhelm

Pierre Wolper

Proceedings of the Workshop "Trustworthy Software" 2006, 2006

2005

Proving the Correctness of Disk Paxos.

[BibT_eX]

[DOI]

Mauro Jaskelioff

Arch. Formal Proofs, 2005

Truly On-the-Fly LTL Model Checking.

[BibT_eX]

[DOI]

Moritz Hammer

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

2004

Refining Mobile UML State Machines.

[BibT_eX]

[DOI]

Martin Wirsing

Proceedings of the Algebraic Methodology and Software Technology, 2004

2003

On the Logic of TLA+.

[BibT_eX]

[DOI]

Comput. Artif. Intell., 2003

A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems.

[BibT_eX]

[DOI]

Martin Wirsing

Júlia Zappe

Proceedings of the Fundamental Approaches to Software Engineering, 2003

2002

Model Checking Techniqes for the Analysis of Reactive Systems.

[BibT_eX]

[DOI]

Synth., 2002

Model Checking - Timed UML State Machines and Collaborations.

[BibT_eX]

[DOI]

Christopher Rauh

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

2001

Diagram Refinements for the Design of Reactive Systems.

[BibT_eX]

[DOI]

Dominique Cansell

J. Univers. Comput. Sci., 2001

Model checking UML state machines and collaborations.

[BibT_eX]

[DOI]

Timm Schäfer

Proceedings of the Workshop on Software Model Checking 2001, 2001

Formal Analysis of a Self-Stabilizing Algorithm Using Predicate Diagrams.

[BibT_eX]

Dominique Cansell

Proceedings of the Tagungsband der GI/OCG-Jahrestagung - 31. Jahrestagung der Gesellschaft für Informatik, Wirtschaft und Wissenschaft in der Network Economy, 2001

2000

Weak Alternating Automata in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Model Checking: A Tutorial Overview.

[BibT_eX]

[DOI]

Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Predicate Diagrams for the Verification of Reactive Systems.

[BibT_eX]

[DOI]

Dominique Cansell

Proceedings of the Integrated Formal Methods, Second International Conference, 2000

1999

Animating TLA Specifications.

[BibT_eX]

[DOI]

Yassin Mokhtari

Proceedings of the Logic Programming and Automated Reasoning, 6th International Conference, 1999

A More Complete TLA.

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

1997

Type-Checking Higher-Order Polymorphic Multi-Methods.

[BibT_eX]

[DOI]

François Bourdoncle

Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

Rules for Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1997

1996

On TLA as a logic.

[BibT_eX]

Martín Abadi

Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996

1995

Modular Description and Verification of Concurrent Objects.

[BibT_eX]

[DOI]

Jean Paul Bahsoun

Corinne Servieres

Proceedings of the Object-Based Parallel and Distributed Computation, 1995

An Abstract Account of Composition.

[BibT_eX]

[DOI]

Martín Abadi

Proceedings of the Mathematical Foundations of Computer Science 1995, 1995

Steam Boiler Control Specification Problem: A TLA Solution.

[BibT_eX]

[DOI]

Frank Leßke

Proceedings of the Formal Methods for Industrial Applications, 1995

1994

Specifying and Verifying Fault-Tolerant Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

The RPC-Memory Case Study: A Synopsis.

[BibT_eX]

[DOI]

Manfred Broy

Katharina Spies

Proceedings of the Formal Systems Specification, 1994

A TLA Solution to the RPC-Memory Specification Problem.

[BibT_eX]

[DOI]

Martín Abadi