Thread-modular Counter Abstraction

Thread-modular counter abstraction (TMCA) is a clean, two-step abstraction framework for proving safety and liveness of parameterized programs.

Introductory Talk at FMCAD’20

Implementation

Contact

For enquiries, please contact Thomas Pani.

Publications

2020
[4]Parameterized Program Safety and Liveness via Thread-modular Counter Abstraction
Thomas Pani, Georg Weissenbacher, Florian Zuleger
2020.
Note: Paper presented at the FMCAD'20 student forum
[bibtex]
[3]Rely-Guarantee Bound Analysis of Parameterized Concurrent Shared-Memory Programs
Thomas Pani, Georg Weissenbacher, Florian Zuleger
, 2020.
Note: under submission
[bibtex]
[2] Thread-modular Counter Abstraction for Parameterized Program Safety
Thomas Pani, Georg Weissenbacher, Florian Zuleger
Formal Methods in Computer Aided Design, FMCAD (Alexander Ivrii, Ofer Strichman, eds.), 2020.
Note: to appear
[bibtex] [pdf]
2018
[1] Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
Thomas Pani, Georg Weissenbacher, Florian Zuleger
Formal Methods in Computer Aided Design, FMCAD (Nikolaj Bjørner, Arie Gurfinkel, eds.), pages 1–9, 2018, IEEE.
[bibtex] [pdf] [doi]

Latest News

Jens Pagel wins Bill McCune PhD Award

We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.

Continue reading

Full news archive