Sciweavers

Share
TPHOL
2007
IEEE

Building Formal Method Tools in the Isabelle/Isar Framework

9 years 14 days ago
Building Formal Method Tools in the Isabelle/Isar Framework
Abstract We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible state components and extensible syntax that can be bound to tactical ML programs. Thus the Isabelle/Isar architecture may be understood as an extension and refinement of the traditional “LCF approach”, with explicit infrastructure for building derivative systems. To demonstrate the technical potential of the framework, we apply it to a concrete formal methods tool: the HOL-Z 3.0 environment, which is geared towards the analysis of Z specifications and formal proof of forward-refinements.
Makarius Wenzel, Burkhart Wolff
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TPHOL
Authors Makarius Wenzel, Burkhart Wolff
Comments (0)
books