Algebraic Principles for Program Verification and Refinement Tools

Add to your list(s) Download to your calendar using vCal

• Victor Gomes
• Thursday 17 September 2015, 14:30-15:30
• FW11.

If you have a question about this talk, please contact Peter Sewell.

A modular approach to the development of verification and refinement tools for imperative programs based on algebraic principles, in which the control flow and the data level are cleanly separated, is presented. 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 operation 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 program transformation rules can be derived. Programming the approach in Isabelle/HOL yields simple lightweight mathematical components as well as program verification and refinement tools that are correct by construction themselves. Verification condition generation and refinement laws are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. The framework has also been extended to programs with separating resources, where a novel algebraic approach to separation logic is given based on power series. Finally, concurrency can also be supported by using the rely-guarantee method, where an expansion of bi-Kleene algebras are used to derive inference rules, and Aczzel traces are used as program semantics.

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.