Automated compositional abstraction refinement for concurrent C programs: a two-level approach

MaRDI QIDQ2845499zbMATH OpenFDO

Authors Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund Clarke

Publication date 30 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105800040

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)

Recommendations

• Efficient verification of sequential and concurrent C programs
• Tools and Algorithms for the Construction and Analysis of Systems
• Concurrent software verification with states, events, and deadlocks
• Formal verification for C program
• Counterexample-guided abstraction refinement for symmetric concurrent programs

Cited in

(6)

• SAT-solving in CSP trace refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• Boosting Lazy Abstraction for SystemC with Partial Order Reduction
• Compositional abstraction refinement for control synthesis
• Concurrent software verification with states, events, and deadlocks
• Automated Assume-Guarantee Reasoning by Abstraction Refinement

Describes a project that uses

Uses Software

• MAGIC
• Bandera

This page was built for publication: Automated compositional abstraction refinement for concurrent C programs: a two-level approach

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