Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two new AFP entries: Simpl and BDD

Email Gateway (Aug 18 2022 at 11:30):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
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

Abstract:
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.

and

BDD-Normalisation
by Veronika Ortner and Norbert Schirmer

Abstract:
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
logics.

Cheers,
Gerwin

Last updated: Nov 21 2024 at 12:39 UTC