[isabelle] Two new AFP entries: Simpl and BDD

We are pleased to announce the availability of two new entries in the Archive of Formal Proofs [http://afp.sf.net].

                                --- Simpl ---
       A Sequential Imperative Programming Language
       Syntax, Semantics, Hoare Logics and Verification Environment

by Norbert Schirmer

We present the theory of Simpl, a sequential imperative programming language. We introduce its syntax, its semantics (big and small-step operational semantics) and Hoare logics for both partial as well as total correctness. We prove soundness and completeness of the Hoare logic. We integrate and automate the Hoare logic in Isabelle/HOL to obtain a practically usable verification environment for imperative programs.

Simpl is independent of a concrete programming language but expressive
enough to cover all common language features: mutually recursive
procedures, abrupt termination and exceptions, runtime faults, local
and global variables, pointers and heap, expressions with side
effects, pointers to procedures, partial application and closures,
dynamic method invocation and also unbounded nondeterminism.


by Veronika Ortner and Norbert Schirmer

We present the verification of the normalisation of a binary decision
diagram (BDD). The normalisation follows the original algorithm
presented by Bryant in 1986 and transforms an ordered BDD in a
reduced, ordered and shared BDD. The verification is based on Hoare


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.