@inproceedings{
    TauHel:SPIN2000,
    editor = "Havelund, Klaus and Penix, John and Visser, Willem",
    author = "Tauriainen, Heikki and Heljanko, Keijo",
    publisher = "Springer-Verlag",
    title = {Testing {SPIN}'s {LTL} formula conversion into {B\"uchi} automata with randomly generated input},
    url = "http://users.ics.tkk.fi/kepa/publications/",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 7th International {SPIN} Workshop on Model Checking of Software ({SPIN}'2000)",
    address = "Stanford University, California, USA",
    abstract = {The use of model checking tools in the verification of reactive systems has become into widespread use. Because the model checkers are often used to verify critical systems, a lot of effort should be put on ensuring the reliability of their implementation. We describe techniques which can be used to test and improve the reliability of linear temporal logic (LTL) model checker implementations based on the automata-theoretic approach. More specifically, we will concentrate on the LTL-to-{B}\"uchi automata conversion algorithm implementations, and propose using a random testing approach to improve their robustness. As a case study, we apply the methodology to the testing of this part of the SPIN model checker. We also propose adding a simple counterexample validation algorithm to LTL model checkers to double check the counterexamples generated by the main LTL model checking algorithm.},
    month = "August",
    volume = "1885",
    juforank = "1",
    flags = "copy SA-LO-00-02",
    year = "2000",
    keywords = {LTL, B{\"u}chi automata},
    pages = "54--72"
}