Verification of Boolean programs with unbounded thread creation

DOI10.1016/j.tcs.2007.07.050zbMath1143.68043MaRDI QIDQ2464944

Natasha Sharygina, Daniel Kroening, Byron Cook

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

zbMATH Keywords

reachability; model checking; program verification; Boolean programs

Mathematics Subject Classification ID

68Q55: Semantics in the theory of computing

68Q60: Specification and verification (program logics, model checking, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

• Zing
• NuSMV
• Java PathFinder
• Bebop
• TLPVS
• SatAbs
• MAGIC

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item