Verification, Model Checking, and Abstract Interpretation

DOI10.1007/B94790zbMath1202.68244OpenAlexW3146639584MaRDI QIDQ5901905

Edmund M. Clarke, Joël Ouaknine, Daniel Kroening, Ofer Strichman

Publication date: 15 May 2009

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

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

Mathematics Subject Classification ID

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

Related Items (16)

Periodicity based decidable classes in a first order timed logic ⋮ Bounded model checking of infinite state systems ⋮ Linear templates of ACTL formulas with an application to SAT-based verification ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Verifying Real-Time Properties of Multi-agent Systems via SMT-Based Bounded Model Checking ⋮ Intuitive modelling and formal analysis of collective behaviour in foraging ants ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ SAT-solving in CSP trace refinement ⋮ Constraint LTL satisfiability checking without automata ⋮ Bounded semantics ⋮ Computation of the transient in max-plus linear systems via SMT-solving ⋮ On the completeness of bounded model checking for threshold-based distributed algorithms: reachability ⋮ Linear Completeness Thresholds for Bounded Model Checking ⋮ TOrPEDO : witnessing model correctness with topological proofs ⋮ Counterexample-preserving reduction for symbolic model checking ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic

This page was built for publication: Verification, Model Checking, and Abstract Interpretation