Co-inductive Axiomatization of a Synchronous Language

Abstract. Over the last decade, the increasing demand for the validation of safety critical systems lead to the development of domain-specific programming languages (e.g. synchronous languages) and automatic verification tools (e.g. model checkers). Conventionally, the verification of a reactive system is implemented by specifying a discrete model of the system (i.e. a finite-state machine) and then checking this model against temporal properties (e.g. using an automata-based tool). We investigate the use of a theorem prover, Coq, for the specification of infinite state systems and for the verification of co-inductive properties.

• Type: Conference
• Year: 1998
• Where: TPHOL
• Authors: David Nowak, Jean-René Beauvais, Jean-Pierre Talpin
• Keywords: Automated Reasoning, Automatic Verification Tools, Domain-specific Programming Languages, Safety Critical Systems, TPHOL 1998