Sciweavers

IPPS
1998
IEEE

Automatically Proving UNITY Safety Properties with Arrays and Quantifiers

13 years 7 months ago
Automatically Proving UNITY Safety Properties with Arrays and Quantifiers
Abstract. We address the general problem of automatically proving safety properties of reactive systems within the UNITY model. We take up a relational and set-based approach, and define some techniques to represent instructions and properties, allowing us to deal with arrays and quantification. An integration of these techniques into the OMEGA calculator, which we make use of with a significant example, now allows us to think of deep automation of non trivial theorem proving.
Xavier Thirioux
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where IPPS
Authors Xavier Thirioux
Comments (0)