Applications of real number theorem proving in PVS

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con PVS titulado Applications of real number theorem proving in PVS.

Sus autores son

Su resumen es

Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.

A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

A formalisation of Göodel’s incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows Świerczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of HF is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.

Verified AIG algorithms in ACL2

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en ACL2 titulado Verified AIG algorithms in ACL2.

Sus autores son

Su resumen es

And-Inverter Graphs (AIGs) are a popular way to represent Boolean functions (like circuits). AIG simplification algorithms can dramatically reduce an AIG, and play an important role in modern hardware verification tools like equivalence checkers. In practice, these tricky algorithms are implemented with optimized C or C++ routines with no guarantee of correctness. Meanwhile, many interactive theorem provers can now employ SAT or SMT solvers to automatically solve finite goals, but no theorem prover makes use of these advanced, AIG-based approaches.

We have developed two ways to represent AIGs within the ACL2 theorem prover. One representation, Hons-AIGs, is especially convenient to use and reason about. The other, Aignet, is the opposite; it is styled after modern AIG packages and allows for efficient algorithms. We have implemented functions for converting between these representations, random vector simulation, conversion to CNF, etc., and developed reasoning strategies for verifying these algorithms.

Aside from these contributions towards verifying AIG algorithms, this work has an immediate, practical benefit for ACL2 users who are using GL to bit-blast finite ACL2 theorems: they can now optionally trust an off-the-shelf SAT solver to carry out the proof, instead of using the built-in BDD package. Looking to the future, it is a first step toward implementing verified AIG simplification algorithms that might further improve GL performance

El trabajo se ha presentado en el ACL2 2013 (Eleventh International Workshop on the ACL2 Theorem Prover and Its Applications).

A formal model and correctness proof for an access control policy framework

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Isabelle/HOL titulado A formal model and correctness proof for an access control policy framework.

Sus autores son

Su resumen es

If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model—a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security com- promise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson’s inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.

El trabajo se presentará en diciembre en el CPP 2013 (3rd Conference on Certified Programs and Proofs.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

The ontological argument in PVS

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en PVS titulado The ontological argument in PVS.

Su autor es John Rushby (del SRI International).

Su resumen es

The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in PVS and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.