Automatiserad Verifiering av Ändliga Spåregenskaper för Rekursiva Program

In deductive verification programs are usually checked against contracts consisting of a precondition and postcondition. These conditions establish a relation between a program’s initial and final state of execution. Information about the intermediary states is abstracted away. In order to capture this information, the state sequence generated by a program’s execution can be verified against a temporal specification. Such a specification expresses the property of interest in terms of program traces. In this thesis, we restrict ourselves to finite-trace properties that are described by a modified modal μ-calculus with “chop”. The underlying logic is expressive enough to characterise every terminating program in an imperative recursive programming language. The project’s research question is concerned about whether there is an effective method of deciding that a recursive program is correct with respect to the trace specification. This work extends the scope of the trace logic to more practical applications. We present a formalism that reduces the model-checking problem of a recursive program against a finite-trace property to a satisfaction problem in many-sorted first-order logic. This reduction is proven sound, but incomplete. There are programs satisfying the specification, but the reduced problem is unsatisfiable. A program’s traces are encoded into many-sorted first-order logic, where (recursive) procedures are approximated by Hoare-like contracts. Similarly, the specification formula is encoded into many-sorted first-order logic. Recursive properties give raise to a dependant model-checking sub-problem, which is also encoded into many-sorted first-order logic. These encodings preserve the properties necessary for the soundness of the reduction. Additionally, the theoretical framework is implemented in a proof-of-concept tool written in Haskell using Z3 as a backend-solver.