SMT-Based Induction Methods for Timed Systems

DOI10.1007/978-3-642-33365-1_13zbMath1374.68293arXiv1204.5639OpenAlexW132127320MaRDI QIDQ4649395

Tommi Junttila, Roland Kindermann, Ilkka Niemelä

Publication date: 21 November 2012

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

Full work available at URL: https://arxiv.org/abs/1204.5639

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (9)

Configurable verification of timed automata with discrete variables ⋮ Lazy Reachability Checking for Timed Automata with Discrete Variables ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ SMT-based satisfiability of first-order LTL with event freezing functions and metric operators ⋮ Verification Modulo theories ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ Abstraction-based incremental inductive coverability for Petri nets

This page was built for publication: SMT-Based Induction Methods for Timed Systems