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 2020. Note: Paper presented at the FMCAD'20 student forum |
[3] | Rely-Guarantee Bound Analysis of Parameterized Concurrent Shared-Memory Programs , 2020. Note: under submission |
[2] | Thread-modular Counter Abstraction for Parameterized Program Safety Formal Methods in Computer Aided Design, FMCAD (Alexander Ivrii, Ofer Strichman, eds.), 2020. Note: to appear |
2018 | |
[1] | Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Formal Methods in Computer Aided Design, FMCAD (Nikolaj Bjørner, Arie Gurfinkel, eds.), pages 1–9, 2018, IEEE. |