BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Algebraic Principles for Program Verification and Refinement Tools
  - Victor Gomes
DTSTART:20150917T133000Z
DTEND:20150917T143000Z
UID:TALK60819@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:A modular approach to the development of verification and refi
 nement tools for imperative programs based on algebraic principles\, in wh
 ich the control flow and the data level are cleanly separated\, is present
 ed.  The verification tool uses Kleene algebras with tests (KAT) to model 
 the control flow of while-programs and their standard relational semantics
  for the data level. This is expanded to a refinement tool by adding an op
 eration for Morgan’s specification statement and one single axiom to the
  algebra. To include recursive procedures\, KAT are expanded to quantales 
 with tests\, a more expressive algebraic structure where iteration and the
  specification statement can be defined explicitly. Moreover\, stronger pr
 ogram transformation rules can be derived. Programming the approach in Isa
 belle/HOL yields simple lightweight mathematical components as well as pro
 gram verification and refinement tools that are correct by construction th
 emselves. Verification condition generation and refinement laws are based 
 on equational reasoning and supported by powerful Isabelle tactics and aut
 omated theorem proving. The framework has also been extended to programs w
 ith separating resources\, where a novel algebraic approach to separation 
 logic is given based on power series. Finally\, concurrency can also be su
 pported by using the rely-guarantee method\, where an expansion of bi-Klee
 ne algebras are used to derive inference rules\, and Aczzel traces are use
 d as program semantics.
LOCATION:FW11
END:VEVENT
END:VCALENDAR