Verification of Boolean programs with unbounded thread creation
From MaRDI portal
Publication:2464944
DOI10.1016/j.tcs.2007.07.050zbMath1143.68043OpenAlexW2155394073MaRDI QIDQ2464944
Byron Cook, Daniel Kroening, Natasha Sharygina
Publication date: 18 December 2007
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2007.07.050
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Context-aware counter abstraction, A model checking-based approach for security policy verification of mobile systems, Counterexample-guided abstraction refinement for symmetric concurrent programs, Analysis of correct synchronization of operating system components, Lost in abstraction: monotonicity in multi-threaded programs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model checking JAVA programs using JAVA PathFinder
- Predicate abstraction of ANSI-C programs using SAT
- On the analysis of interacting pushdown systems
- Counterexample-guided abstraction refinement for symbolic model checking
- Verifying safety properties of concurrent Java programs using 3-valued logic
- Logical characterizations of heap abstractions
- Verification: Theory and Practice
- CONCUR 2004 - Concurrency Theory
- CONCUR 2004 - Concurrency Theory
- Model Checking Software
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
