Predicate abstraction and refinement for verifying multi-threaded programs

DOI10.1145/1926385.1926424zbMath1284.68427OpenAlexW4236040576MaRDI QIDQ5408554

Ashutosh Gupta, Andrey Rybalchenko, Corneliu 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

safetyHorn clausesmulti-threaded programsabstraction refinementmodular reasoningproof rule(transition) predicate abstractionenvironment transitions

Mathematics Subject Classification ID

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

Related Items

Verifying Procedural Programs via Constrained Rewriting Induction, Local Symmetry and Compositional Verification, Compositional Reasoning, Predicate Abstraction for Program Verification, Model Checking Concurrent Programs, Counterexample-guided abstraction refinement for symmetric concurrent programs, Analysis of correct synchronization of operating system components, Farkas-based tree interpolation, Verification of concurrent programs using Petri net unfoldings, Non-deterministic Weighted Automata on Random Words, Non-deterministic weighted automata evaluated over Markov chains, Compositional reasoning for shared-variable concurrent programs, Lost in abstraction: monotonicity in multi-threaded programs, On recursion-free Horn clauses and Craig interpolation