Crocos: An integrated environment for interactive verification of SDL specifications

Abstract

We are interested by proofs of concurrent programs properties, such as invariance and eventuality. They are connected with execution of a program, and, in order to discuss them, we introduce an operational model of the language and show that the deductive system is consistent with respect to it. The studied language is a selected subset of the SDL language. A system for computer-aided reasoning on programs is derived as follows: we implement the deductive system in Isabelle [24] and then integrate it into a programming environment developed under Concerto namely Crocos [19]. The prover proceeds in an interactive way in which the user’s intervention may be required at several stages of the proof derivation.