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.

• Type: Conference
• Year: 1998
• Where: IPPS
• Authors: Xavier Thirioux
• Keywords: Distributed And Parallel Computing, IPPS 1998, Non Trivial Theorem, Reactive Systems, Safety Properties