Lost in abstraction: monotonicity in multi-threaded programs

DOI10.1016/J.IC.2016.03.003MaRDI QIDQ729809zbMATH OpenOpenAlexFDO

Authors Daniel Kroening, Thomas Wahl, Alexander D. Kaiser

Publication date 22 December 2016

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2016.03.003

zbMATH Keywords

monotonicitypredicate abstractionmulti-threaded softwareparameterized verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Lost in abstraction: monotonicity in multi-threaded programs
• MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
• Symbolic Counter Abstraction for Concurrent Software
• Thread-modular abstraction refinement.
• Non-monotonic refinement of control abstraction for concurrent programs

Cites work

• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 108539 (Why is no real title available?)
• scientific article; zbMATH DE number 2080051 (Why is no real title available?)
• scientific article; zbMATH DE number 1796136 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• All for the price of few (parameterized verification through view abstraction)
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Efficient coverability analysis by proof minimization
• Inductive data flow graphs
• Lossy counter machines decidability cheat sheet
• Monotonic abstraction in parameterized verification
• Predicate abstraction and refinement for verifying multi-threaded programs
• Predicate abstraction for software verification
• Reasoning about systems with many processes
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of Boolean programs with unbounded thread creation
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Verification, Model Checking, and Abstract Interpretation
• Well (and better) quasi-ordered transition systems
• Well-structured transition systems everywhere!

Cited in

(5)

• Lost in abstraction: monotonicity in multi-threaded programs
• Delay-bounded scheduling without delay!
• Lazy constrained monotonic abstraction
• monabs
• Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation

Describes a project that uses

Uses Software

• SAS
• SymmPa
• SLAB
• Threader
• MAGIC
• DDVerify

This page was built for publication: Lost in abstraction: monotonicity in multi-threaded programs

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