Catálogo de publicaciones - libros

Our study was part of a project aiming at the design and verification of a circuit for secure communications between a computer and a terminal smart card reader. A SHA-1 component is included in the circuit. SHA-1 is a cryptographic primive that produces, for any message, a 160 bit message digest. We formalize the standard specification in ACL2, then automatically produce the ACL2 model for the VHDL RTL design; finally, we prove the implementation compliant with the specification. We apply a stepwise approach that proves theorems about each computation step of the RTL design, using intermediate digest functions.

Using the HOL theorem prover, we proved the correctness of a translation from a subset of Accellera’s property specification language PSL to linear temporal logic LTL. Moreover, we extended the temporal logic hierarchy of LTL that distinguishes between safety, liveness, and more difficult properties to PSL . The combination of the translation from PSL to LTL with already available translations from LTL to corresponding classes of -automata yields an efficient translation from PSL to -automata. In particular, this translation generates liveness or safety automata for corresponding PSL fragments, which is important for several applications like bounded model checking.

In this paper we present a formalization and proof of Higman’s Lemma in ACL2. We formalize the constructive proof described in [10] where the result is proved using a termination argument justified by the multiset extension of a well-founded relation. To our knowledge, this is the first mechanization of this proof.

We briefly describe a mechanically checked proof of Dijkstra’s shortest path algorithm for finite directed graphs with nonnegative edge lengths. The algorithm and proof are formalized in ACL2.

Structural recursion over sets is meaningful only if the result is independent of the order in which the set’s elements are enumerated. This paper outlines a theory of function definition for finite sets, based on the fold functionals often used with lists. The fold functional is introduced as a relation, which is then shown to denote a function under certain conditions. Applications include summation and maximum. The theory has been formalized using Isabelle/HOL .

We discuss methods for dealing effectively with -bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translation from the -calculus to combinators. This approach copes with the usual encodings of paired abstraction, ensures that bound variable names are preserved, and uses only conventional simplification technology.