scientific article; zbMATH DE number 2090318
From MaRDI portal
Publication:4809077
zbMath1072.68602MaRDI QIDQ4809077
Harald Ruess, Leonardo de Moura, Maria Sorea
Publication date: 12 August 2004
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2392/23920438.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)
Related Items (21)
Bounded model checking of infinite state systems ⋮ Answer set programming based on propositional satisfiability ⋮ HySAT: An efficient proof engine for bounded model checking of hybrid systems ⋮ Verification Modulo theories ⋮ Synchronous counting and computational algorithm design ⋮ Superposition as a decision procedure for timed automata ⋮ A decidability result for the model checking of infinite-state systems ⋮ Towards SMT Model Checking of Array-Based Systems ⋮ Constraint LTL satisfiability checking without automata ⋮ Complexity-sensitive decision procedures for abstract argumentation ⋮ Abstraction-Based Algorithm for 2QBF ⋮ Unnamed Item ⋮ Light-Weight SMT-based Model Checking ⋮ Composing model programs for analysis ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Combining Equational Reasoning ⋮ Theory decision by decomposition ⋮ An interpolating theorem prover ⋮ Rewrite-Based Decision Procedures ⋮ Bounded Model Checking with Parametric Data Structures ⋮ Solving QBF with counterexample guided refinement
Uses Software
This page was built for publication: