University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Verification Based on Algebra and Automated Deduction

Verification Based on Algebra and Automated Deduction

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

If you have a question about this talk, please contact Matthew Parkinson.

The formal formal analysis and verification of computing systems has so far been dominated by model checkers and other decision procedures which are fully automated, but limited in expressive power, and by interactive theorem provers which are quite expressive, but limited in automation. Due to improved hardware and theoretical developments, automated deduction is currently emerging as a third way in which expressivity and computational power are differently balanced and which conveniently complements the other approaches.

I will present a new approach to formal verification in which computational algebras are combined with off-the-shelf automated theorem provers for first-order equational logic. The algebras considered are variants of Kleene algebras and their extensions by modal operators. Particular strengths of these structures are syntactic simplicity, wide applicability, concise elegant equational proofs, easy mechanisability and strong decidability.

I will sketch the axiomatisation and calculus of Kleene algebras and modal Kleene algebras, discuss some computationally interesting models, such as traces, graphs, languages and relations, and point out their relationship to popular verification formalisms, including dynamic logic, temporal logic and Hoare logic. I will also report on some automation results in the areas of action system refinement, termination analysis and program verification that demonstrate the benefits and the potential of the algebraic approach.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity