@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",

}