Email Gateway (Aug 18 2022 at 11:30): 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: May 03 2024 at 08:18 UTC