Linear Encodings of Bounded LTL Model Checking
From MaRDI portal
Publication:5310676
DOI10.2168/LMCS-2(5:5)2006zbMath1127.68057MaRDI QIDQ5310676
Viktor Schuppan, Armin Biere, Tommi Junttila, Timo Latvala, Keijo Heljanko
Publication date: 11 October 2007
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (19)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ A collaborative approach for multi-threaded SAT solving ⋮ SAT-Based Model Checking ⋮ Checking EMTLK properties of timed interpreted systems via bounded model checking ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Exhaustive property oriented model-based testing with symbolic finite state machines ⋮ HRELTL: a temporal logic for hybrid systems ⋮ Solving parity games by a reduction to SAT ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ Constraint LTL satisfiability checking without automata ⋮ Bounded semantics ⋮ Unnamed Item ⋮ On simulation-based probabilistic model checking of mixed-analog circuits ⋮ Efficient data validation for geographical interlocking systems ⋮ TOrPEDO : witnessing model correctness with topological proofs ⋮ Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time ⋮ Counterexample-preserving reduction for symbolic model checking ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic
Uses Software
This page was built for publication: Linear Encodings of Bounded LTL Model Checking
