Verification Tool DIY

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

• Professor Georg Struth, Department of Computer Science, University of Sheffield
• Thursday 11 December 2014, 16:00-17:00
• Hills Building, Room 120.

If you have a question about this talk, please contact Mohammad Tayarani.

Host: Mohammad Tayarani, m.tayarani@cs.bham.ac.uk

I present a principled approach to the design of program verification and correctness tools which aims at a clean separation between the control flow and the data flow of programs. The aim is to find simple algebraic semantics for the control flow and combine them with detailed set-theoretic models for data and memory domains. The approach is implemented in the Isabelle/HOL theorem prover, and its principles will be illustrated through three example tools, all of which are correct by construction. The first one is a program verification and refinement tool for simple while-programs, which uses Kleene algebras with tests for the control flow and a standard relational semantics for the data flow. The second tool implements separation logic using a novel algebraic semantics for the control flow and an extended relational model for the data flow on store and heap. The third one is based on the rely-guarantee approach to shared-variable concurrency, using concurrent Kleene algebras for the control flow and trace-based models for the data flow, once again with novel axioms for interference constraints. If time permits I will show these tools at work on a number of algorithmic verification and refinement examples.

This talk is part of the Computer Science Departmental Series series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Hills Building, Room 120
• computer sience

Note that ex-directory lists are not shown.