Bounded model checking of concurrent programs

DOI10.1007/11513988_9MaRDI QIDQ5716600zbMATH OpenOpenAlexFDO

Authors Ishai Rabinovitz, Orna Grumberg

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b138445

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-bounded model checking of concurrent software
• A bounded model checker for three-valued abstractions of concurrent software systems
• Accelerating bounded model checking of safety properties
• Model Checking Software
• Theory and Applications of Models of Computation

Cited in

(25)

• Compact and efficiently verifiable models for concurrent systems
• Model checking concurrency and causality
• Incremental bounded model checking for embedded software
• A bounded model checker for three-valued abstractions of concurrent software systems
• Model checking of concurrent software systems via heuristic-guided SAT solving
• Verification of SpecC using predicate abstraction
• Scaling bounded model checking by transforming programs with arrays
• BDD vs. constraint-based model checking: An experiment evaluation for asynchronous concurrent systems
• Unbounded-thread program verification using thread-state equations
• Model checking concurrent programs with nondeterminism and randomization
• SAT-Based Model Checking
• Model checking concurrent programs
• scientific article; zbMATH DE number 5353387 (Why is no real title available?)
• Symbolic predictive analysis for concurrent programs
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Concurrent program verification with invariant-guided underapproximation
• Bounded model checking of C programs using event automaton specifications
• Model Checking Software
• Model checking with bounded context switching
• Computer Science Logic
• Context-bounded model checking of concurrent software
• Wolf -- bug hunter for concurrent software using formal methods
• Extracting safe thread schedules from incomplete model checking results
• Efficient loop conditions for bounded model checking hyperproperties
• A bounded model checking technique for higher-order programs

Describes a project that uses

Uses Software

• Zing

This page was built for publication: Bounded model checking of concurrent programs

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