Verification Based on Algebra and Automated Deduction

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

• Georg Struth, Sheffield University
• Friday 02 May 2008, 14:00-15:00
• Room FW11, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.