@article{
    TauHel:STTT02,
    author = "Tauriainen, Heikki and Heljanko, Keijo",
    publisher = "Springer-Verlag",
    title = {Testing {LTL} Formula Translation into {B{\"u}chi} Automata},
    url = "http://users.ics.tkk.fi/kepa/publications/",
    journal = "{STTT} - {I}nternational Journal on Software Tools for Technology Transfer",
    number = "1",
    abstract = {Model checkers are often used to verify critical systems, and thus a lot of effort should be put on ensuring their reliability. We describe techniques for testing linear temporal logic (LTL) model checker implementations, focusing especially on LTL-to-B{\"u}chi automata translation. We propose a randomized testing approach based on the cross-comparison of independent translator implementations, and present methods for test failure analysis. We give experimental results using an automated tool implementing the testing methodology. This method has helped to detect errors in model checking tools such as Spin. We also propose extending LTL model checkers with a simple counterexample validation algorithm.},
    volume = "4",
    juforank = "1",
    flags = "copy SA-LO-00-02",
    year = "2002",
    keywords = "verification, model checking, temporal logic, software testing",
    pages = "57--70"
}