![]() |
![]() |
University of Birmingham > Talks@bham > Computer Science Departmental Series > Verification Tool DIY
Verification Tool DIYAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsParticle Physics Seminars Applied Topology Colloquium CargoOther talksProofs of Turán's theorem Quantum Sensing in Space TBA The tragic destiny of Mileva Marić Einstein Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Life : it’s out there, but what and why ? |