@inproceedings{
    KindermannJunttilaNiemela:FORTE2012,
    editor = "Giese, Holger and Rosu, Grigore",
    author = {Kindermann, Roland and Junttila, Tommi and Niemel{\"a}, Ilkka},
    isbn = "978-3-642-30792-8",
    series = "Lecture Notes in Computer Science",
    abstract = "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 lassoshaped 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¨uchi automata. This paper introduces a new SMT-based BMC approach that can find a counter-example to any non-holding B¨uchi 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.",
    il = "no",
    year = "2012",
    keywords = "bounded model checking, timed automata, satisfiability modulo theories, symbolic model checking",
    title = "Beyond Lassos: Complete {SMT}-Based Bounded Model Checking for Timed Automata",
    eventlocation = "Stockholm, Sweden",
    booktitle = "Formal Techniques for Distributed Systems",
    juforank = "1",
    unitcode = "T306-99, T312-1",
    impactfactor = "A4",
    eventtime = "June 13-16",
    responsibleauthor = {Kindermann, Roland and Junttila, Tommi and Niemel{\"a}, Ilkka},
    pages = "84--100",
    volume = "7273",
    publisher = "Springer",
    language = "eng",
    url = "http://dx.doi.org/10.1007/978-3-642-30793-5_6",
    country = "Germany",
    issn = "0302-9743",
    flags = "COIN,HIIT,StMcDes,logic",
    pdf = "FORTE12.pdf"
}