University of Birmingham > Talks@bham > Computer Science Departmental Series > Verification Tool DIY

Verification Tool DIY

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.