Technical Report CS0957

Title: Static Analysis for Reductions that preserve Temporal Logic
Authors: Karen Yorav (Laster) and Orna Grumberg
Abstract: In this paper we present a method that uses static analysis of programs to create reduced models of the programs. Our algorithm examines the control-flow graph of a program (the syntax) and creates a significantly smaller transition system than would have been created otherwise. The smaller transition system is equivalent to the original transition system of the program with respect to \ctlsx\ specifications. Our algorithm is based on syntactic manipulation of expressions. This enables us to handle programs with variables over finite as well as infinite domains. Our method can easily be combined with either explicit state or symbolic methods. An important advantage of using static analysis is that in order to implement our reduction changes are made only to the compiler (which is relatively simple) and there is no need to change the verification tool or the verification algorithm. This enables integration with existing tools at a very low cost. We used the Murphi verifier to test the amount of reduction achieved by our method. We let Murphi perform a DFS search and compared the sizes of the original and reduced transition systems. The results show that the reduced system is significantly smaller than the original.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1999
To the main CS technical reports page

Computer science department, Technion