APALACHE

Abstraction-based parameterized TLA+ checker

Build status
Bringing state-of-the-art model checking to TLA+

Critical distributed systems are designed to tolerate faults of individual components: they must work even if some of their components fail. In APALACHE, we address two technical and methodological challenges:

  • Domain-specific abstraction for fault-tolerant TLA+ designs.
  • Parameterized model checking techniques for an unbounded number of components.

 

Read more in our recent position paper

Team

igor14 (c) Sebastien Tixeuil HOR_1499
ThanhHaiTran_Photo © Sara Meister jure

Related projects

Parameterized model checking of fault-tolerant distributed algorithms. To see the papers, benchmarks, and tools, check our Byzantine Model Checker .

Recent papers

2017
[9] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017.
[bibtex] [pdf] [doi]
[8] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Inf. Comput., volume 252, pages 95-109, 2017.
[bibtex] [pdf] [doi]
[7] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327
[bibtex] [pdf]
[6]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[bibtex]
2016
[5] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016.
[bibtex] [pdf]
[4] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1-30:16, 2016, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[3] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6-21, 2016, Springer International Publishing.
[bibtex] [pdf]
[2] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
2015
[1] Challenges in Model Checking of Fault-tolerant Designs in TLA+
Igor Konnov, Helmut Veith, Josef Widder
2015, Presentation at the 8th International Workshop on Exploiting Concurrency Efficiently and Correctly, San Francisco, CA, USA, July.
[bibtex] [pdf]

Contact

Address:
Igor Konnov
Technische Universität Wien
Institut für Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien
Austria

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 807
Email: ta.etysrofnull@vonnok
Web: http://forsyte.at/~konnov/

Latest News

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

Helmut Veith 1971-2016

It is with the deepest sadness that we announce Helmut Veith’s passing on March 12, 2016. Helmut was a brilliant researcher, an inspiring collaborator, a stimulating teacher, a generous friend, and a wonderful father and husband. He leaves a void that will be impossible to fill. Our thoughts are with his family and friends.

Continue reading

Full news archive