Counterexample-guided abstraction refinement for symmetric concurrent programs

DOI10.1007/S10703-012-0155-3MaRDI QIDQ2441711zbMATH OpenOpenAlexWikidataFDO

Authors Alexander D. Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl, Alastair Donaldson

Publication date 28 March 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://ora.ox.ac.uk/objects/uuid:b812ccac-2412-454c-8e05-570f6ad071de

zbMATH Keywords

symmetry reductionpredicate abstractionconcurrent programsCEGAR

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) 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

• Symbolic Counter Abstraction for Concurrent Software
• Context-aware counter abstraction
• Model checking: from hardware to software.
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1670775

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• Automatic symmetry detection for Promela
• Context-aware counter abstraction
• Predicate abstraction and refinement for verifying multi-threaded programs
• Tentative steps toward a development method for interfering programs
• Thread-modular abstraction refinement.
• 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

Cited in

(8)

• Symbolic Counter Abstraction for Concurrent Software
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Context-aware counter abstraction
• scientific article; zbMATH DE number 1973975 (Why is no real title available?)
• Counter-example guided program verification
• Lost in abstraction: monotonicity in multi-threaded programs
• Automated compositional abstraction refinement for concurrent C programs: a two-level approach
• Thread-modular abstraction refinement.

Describes a project that uses

Uses Software

• MAGIC
• Threader
• SymmPa
• SymmExtractor
• SLAM

This page was built for publication: Counterexample-guided abstraction refinement for symmetric concurrent programs

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