Counterexample-guided abstraction refinement for symmetric concurrent programs

DOI10.1007/s10703-012-0155-3zbMath1284.68179OpenAlexW1991405126WikidataQ124843770 ScholiaQ124843770MaRDI QIDQ2441711

Daniel Kroening, Thomas Wahl, Michael Tautschnig, Alexander D. Kaiser, Alastair F. 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

concurrent programssymmetry reductionpredicate abstractionCEGAR

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions ⋮ Lost in abstraction: monotonicity in multi-threaded programs

Uses Software

• SLAM
• SymmExtractor
• SymmPa
• Threader
• MAGIC

Cites Work

• Unnamed Item
• Unnamed Item
• Context-aware counter abstraction
• Automatic symmetry detection for Promela
• Verification of Boolean programs with unbounded thread creation
• Tentative steps toward a development method for interfering programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Predicate abstraction and refinement for verifying multi-threaded programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

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