Abstract

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.