Predicate abstraction and refinement for verifying multi-threaded programs

DOI10.1145/1926385.1926424zbMATH Open1284.68427OpenAlexW4236040576MaRDI QIDQ5408554FDOQ5408554

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

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

zbMATH Keywords

abstraction refinementsafetyHorn clausesmodular reasoningproof rulemulti-threaded programs(transition) predicate abstractionenvironment transitions

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)

Cited In (19)

• Analysis of correct synchronization of operating system components
• Non-deterministic weighted automata evaluated over Markov chains
• Farkas-based tree interpolation
• Compositional Reasoning
• Title not available (Why is that?)
• Model Checking Concurrent Programs
• On recursion-free Horn clauses and Craig interpolation
• Non-monotonic refinement of control abstraction for concurrent programs
• Predicate Abstraction for Program Verification
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Compositional termination proofs for multi-threaded programs
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Lost in abstraction: monotonicity in multi-threaded programs
• Compositional reasoning for shared-variable concurrent programs
• Verification of concurrent programs using Petri net unfoldings
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Local symmetry and compositional verification
• Verifying Procedural Programs via Constrained Rewriting Induction
• Non-deterministic Weighted Automata on Random Words

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)