Verification of Boolean programs with unbounded thread creation

DOI10.1016/J.TCS.2007.07.050MaRDI QIDQ2464944zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

model checkingreachabilityprogram verificationBoolean programs

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Unbounded-thread program verification using thread-state equations
• Analysis of Boolean Programs
• Symbolic Counter Abstraction for Concurrent Software
• scientific article; zbMATH DE number 1670555
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1982200 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 1834570 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 794257 (Why is no real title available?)
• CONCUR 2004 - Concurrency Theory
• CONCUR 2004 - Concurrency Theory
• Counterexample-guided abstraction refinement for symbolic model checking
• Logical characterizations of heap abstractions
• Model Checking Software
• Model checking JAVA programs using JAVA PathFinder
• On the analysis of interacting pushdown systems
• Predicate abstraction of ANSI-C programs using SAT
• Reachability analysis of synchronized PA systems
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verifying safety properties of concurrent Java programs using 3-valued logic
• \textsc{tlpvs}: A \textsc{pvs}-based \textsc{ltl} verification system

Cited in

(8)

• Analysis of correct synchronization of operating system components
• Foundations of Boolean stream runtime verification
• A model checking-based approach for security policy verification of mobile systems
• Context-aware counter abstraction
• The complexity of bounded context switching with dynamic thread creation
• Unbounded-thread program verification using thread-state equations
• Lost in abstraction: monotonicity in multi-threaded programs
• Counterexample-guided abstraction refinement for symmetric concurrent programs

Describes a project that uses

Uses Software

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

This page was built for publication: Verification of Boolean programs with unbounded thread creation

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