@inproceedings{
    Makela:safety,
    editor = "Lakos, Charles and Esser, Robert and Kristensen, Lars M. and Billington, Jonathan",
    author = {M{\"a}kel{\"a}, Marko},
    publisher = "Australian Computer Society Inc.",
    title = "Efficiently verifying safety properties with idle office computers",
    series = "Conferences in Research and Practice in Information Technology",
    booktitle = "Formal Methods in Software Engineering and Defence Systems 2002",
    month = "June",
    flags = "public",
    pages = "11--16",
    year = "2002",
    keywords = "model checking, distributed algorithm, state space enumeration",
    pdf = "safety.pdf",
    abstract = "Assuring the quality of safety-critical software systems requires more rigorous methods than testing. Model checking by exhaustive state space enumeration, ``testing all executions,'' is an alternative, but the use of state and memory reduction techniques makes runtime a major limiting factor. We describe a simple parallel version of a state space enumeration algorithm that utilises the unused computing power of office workstations while not congesting their memories. In an experiment with a complex data link protocol, our implementation of the algorithm achieves close to linear speedups on a heterogeneous network of workstations."
}