Symbolic Counter Abstraction for Concurrent Software

DOI10.1007/978-3-642-02658-4_9MaRDI QIDQ3636854zbMATH OpenOpenAlexFDO

Authors Gérard Basler, Michele Mazzucchi, Thomas Wahl, Daniel Kroening

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_9

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Context-aware counter abstraction
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• scientific article; zbMATH DE number 1701765
• Model checking: from hardware to software.
• Thread-modular abstraction refinement.

Cited in

(23)

• Modeling and efficient verification of wireless ad hoc networks
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Multi-scale verification of distributed synchronisation
• Analysis of correct synchronization of operating system components
• Finding cut-offs in leaderless rendez-vous protocols is easy
• Reducing extension edges of concurrent programs for reachability analysis
• Concurrent software verification with states, events, and deadlocks
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Verification of Boolean programs with unbounded thread creation
• scientific article; zbMATH DE number 1701765 (Why is no real title available?)
• Counter abstraction in the CSP/FDR setting
• SAT-Based Model Checking
• Lost in abstraction: monotonicity in multi-threaded programs
• Model checking in bits and pieces
• Abstracting and counting synchronizing processes
• Correct Hardware Design and Verification Methods
• Thread-modular abstraction refinement.
• Context-aware counter abstraction
• Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy
• Counter abstraction for regular open teams
• Automatic WSTS-based repair and deadlock detection of parameterized systems
• Lost in abstraction: monotonicity in multi-threaded programs
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability

Describes a project that uses

Uses Software

• Zing
• SatAbs

This page was built for publication: Symbolic Counter Abstraction for Concurrent Software

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