scientific article; zbMATH DE number 1953038

MaRDI QIDQ4414397zbMATH OpenFDO

Authors Daniel Kroening, Ofer Strichman

Publication date 25 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2575/25750298.htm

Mathematics Subject Classification ID

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

Recommendations

• Verified over-approximation of the diameter of propositionally factored transition systems
• Accelerating bounded model checking of safety properties
• On the magnitude of completeness thresholds in bounded model checking
• Verification, Model Checking, and Abstract Interpretation
• Theory and Applications of Models of Computation

Cited in

(16)

• Formally verified algorithms for upper-bounding state space diameters
• Incremental bounded model checking for embedded software
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Efficient counting of degree sequences
• Automated formal synthesis of provably safe digital controllers for continuous plants
• Verification of SpecC using predicate abstraction
• Compressing BMC encodings with QBF
• Verified over-approximation of the diameter of propositionally factored transition systems
• SAT-Based Model Checking
• Constraint LTL satisfiability checking without automata
• Bounded semantics
• Proving safety with trace automata and bounded model checking
• Partially Bounded Context-Aware Verification
• SAT-based learning of computation tree logic
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• Automatic analysis of DMA races using model checking and k-induction

This page was built for publication:

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