Predicate abstraction and refinement for verifying multi-threaded programs

DOI10.1145/1926385.1926424MaRDI QIDQ5408554zbMATH OpenOpenAlexFDO

Authors Ashutosh Gupta, Andrey Rybalchenko, C. Popeea

Publication date 10 April 2014

Published in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1926385.1926424

zbMATH Keywords

(transition) predicate abstractionabstraction refinementenvironment transitionsHorn clausesmodular reasoningmulti-threaded programsproof rulesafety

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Abstract threads
• Efficient verification of sequential and concurrent C programs
• Predicate abstraction for program verification
• Non-monotonic refinement of control abstraction for concurrent programs
• Predicate Abstraction in Program Verification: Survey and Current Trends

Cited in

(19)

• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Non-deterministic weighted automata evaluated over Markov chains
• Compositional reasoning for shared-variable concurrent programs
• Analysis of correct synchronization of operating system components
• Farkas-based tree interpolation
• Verification of concurrent programs using Petri net unfoldings
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Local symmetry and compositional verification
• Compositional termination proofs for multi-threaded programs
• Compositional reasoning
• Predicate abstraction for program verification
• Model checking concurrent programs
• Non-monotonic refinement of control abstraction for concurrent programs
• Non-deterministic Weighted Automata on Random Words
• Verifying procedural programs via constrained rewriting induction
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Lost in abstraction: monotonicity in multi-threaded programs
• On recursion-free Horn clauses and Craig interpolation

This page was built for publication: Predicate abstraction and refinement for verifying multi-threaded programs

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