Verification, Model Checking, and Abstract Interpretation

DOI10.1007/b94790zbMath1202.68244MaRDI 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

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

Related Items

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, A tool for deciding the satisfiability of continuous-time metric temporal logic, Bounded model checking of ETL cooperating with finite and looping automata connectives, SAT-solving in CSP trace refinement, Constraint LTL satisfiability checking without automata, Bounded semantics, On the completeness of bounded model checking for threshold-based distributed algorithms: reachability, \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms, Computation of the transient in max-plus linear systems via SMT-solving, TOrPEDO : witnessing model correctness with topological proofs, Counterexample-preserving reduction for symbolic model checking, 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, Linear Completeness Thresholds for Bounded Model Checking