Sciweavers

Share
ISSTA
2004
ACM

An optimizing compiler for batches of temporal logic formulas

11 years 10 months ago
An optimizing compiler for batches of temporal logic formulas
Model checking based on validating temporal logic formulas has proven practical and effective for numerous software engineering applications. As systems based on this approach have become more mainstream, a need has arisen to deal effectively with large batches of formulas over a common model. Presently, most systems validate formulas one at a time, with little or no interaction between validation of separate formulas. This is the case despite the fact that, for a wide range of applications, a certain level of redundancy between domain-related formulas can be anticipated. This paper presents an optimizing compiler for batches of temporal logic formulas. A component of the Carnauba model checking system, this compiler addresses the need to handle batches of temporal logic formulas by leveraging the framework common to optimizing programming language compilers. Just as traditional optimizing compilers attempt to exploit redundancy and other solvable properties in a program to reduce t...
James Ezick
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where ISSTA
Authors James Ezick
Comments (0)
books