@inproceedings{61aa77b129de46f9a2b8a58310f7f985,
title = "Factorising Temporal Specifications",
abstract = "This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that there exists a group of threads that establishes the property of interest, while the remaining threads do not affect it. We fine-tune the method by identifying for each property particular conditions under which the preservation is necessary. As a specification language we use the so-called specification patterns developed as part of the Bandera project at Kansas State University. For each specification pattern we propose a decomposition rule. We have shown the soundness of each rule using the pattern mappings as defined for LTL. The proofs have been formalised using the theorem prover Isabelle.",
author = "Marieke Huisman and Kerry Trentelman",
year = "2005",
language = "English",
series = "Conferences in Research and Practice in Information Technology",
publisher = "Australian Computer Society",
pages = "87--96",
editor = "Atkinson, {Mike D.} and Dehne, {Frank K. H. A.}",
booktitle = "Theory of Computing 2005, Eleventh CATS 2005, Computing: The Australasian Theory Symposium, Newcastle, NSW, Australia, January/February 2005",
address = "Australia",
note = "Computing: the Australasian Theory Symposium, CATS 2005, CATS 2005 ; Conference date: 29-01-2005 Through 01-02-2005",
}