Lost in abstraction: monotonicity in multi-threaded programs

DOI10.1016/J.IC.2016.03.003zbMATH Open1355.68055OpenAlexW2293697645MaRDI QIDQ729809FDOQ729809

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

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

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)

Cites Work

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

Cited In (5)

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

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)