Thread-Modular Verification Is Cartesian Abstract Interpretation

DOI10.1007/11921240_13MaRDI QIDQ3525149zbMATH OpenOpenAlexFDO

Authors Alexander Malkis, Andreas Podelski, Andrey Rybalchenko

Publication date 11 September 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11921240_13

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Precise Thread-Modular Verification
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Abstract threads
• Thread-modular abstraction refinement.
• scientific article; zbMATH DE number 1982207

Cited in

(11)

• Complexity of pattern-based verification for multithreaded programs
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Precise Thread-Modular Verification
• Improving thread-modular abstract interpretation
• Static analysis of embedded real-time concurrent software with dynamic priorities
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Abstract threads
• Thread-modular abstraction refinement.
• Clustered relational thread-modular abstract interpretation with local traces

This page was built for publication: Thread-Modular Verification Is Cartesian Abstract Interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3525149)