BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:REMS lunch
SUMMARY:Algebraic Principles for Program Verification and
Refinement Tools - Victor Gomes
DTSTART;TZID=Europe/London:20150917T143000
DTEND;TZID=Europe/London:20150917T153000
UID:TALK60819AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/60819
DESCRIPTION:A modular approach to the development of verificat
ion and refinement tools for imperative programs b
ased on algebraic principles\, in which the contro
l flow and the data level are cleanly separated\,
is presented. The verification tool uses Kleene a
lgebras with tests (KAT) to model the control flow
of while-programs and their standard relational s
emantics for the data level. This is expanded to a
refinement tool by adding an operation for Morgan
’s specification statement and one single axiom to
the algebra. To include recursive procedures\, KA
T are expanded to quantales with tests\, a more ex
pressive algebraic structure where iteration and t
he specification statement can be defined explicit
ly. Moreover\, stronger program transformation rul
es can be derived. Programming the approach in Isa
belle/HOL yields simple lightweight mathematical c
omponents as well as program verification and refi
nement tools that are correct by construction them
selves. Verification condition generation and refi
nement laws are based on equational reasoning and
supported by powerful Isabelle tactics and automat
ed theorem proving. The framework has also been ex
tended to programs with separating resources\, whe
re a novel algebraic approach to separation logic
is given based on power series. Finally\, concurre
ncy can also be supported by using the rely-guaran
tee method\, where an expansion of bi-Kleene algeb
ras are used to derive inference rules\, and Aczze
l traces are used as program semantics.
LOCATION:FW11
CONTACT:Peter Sewell
END:VEVENT
END:VCALENDAR