%0 Conference Proceedings
%T Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata
%+ Department of Information and Computer Science
%A Kindermann, Roland
%A Junttila, Tommi
%A Niemelä, Ilkka
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Stockholm, Sweden
%Y Holger Giese
%Y Grigore Rosu
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7273
%P 84-100
%8 2012-06-13
%D 2012
%R 10.1007/978-3-642-30793-5_6
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. Previous SMT-based BMC approaches for TAs search for finite counter-examples and infinite lasso-shaped counter-examples. This paper shows that lasso-based BMC cannot detect counter-examples for some linear time specifications expressed, e.g., with LTL or Büchi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding Büchi automaton or LTL specification and also, in theory, prove that a specification holds. Different BMC encodings tailored for the supported features of different SMT solvers are compared experimentally to lasso-based BMC and discretization-based SAT BMC.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01528739/document
%2 https://inria.hal.science/hal-01528739/file/978-3-642-30793-5_6_Chapter.pdf
%L hal-01528739
%U https://inria.hal.science/hal-01528739
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-FMOODS
%~ IFIP-LNCS-7273