Overview
Isabelle is described as a proof assistant based on a kernel that ensures logical correctness. It is customizable to multiple logics, including first-order logic, Zermelo-Fraenkel set theory, and especially higher-order logic (HOL). In this setting, Isabelle/HOL refers to the HOL instance, which is supported by components for specification constructs such as type definitions, recursive function definitions with termination proofs, and inductive set definitions. [isabelle-proof-assistant-and-hol]
Capabilities
The evidence characterizes Isabelle as an interactive development environment that provides immediate feedback during formal proof attempts and symbolic computations. It also includes automatic reasoning support, including a term rewriting engine and decision procedures. Beyond its role as a verification environment, Isabelle is described as a framework for building formal-methods tools. [isabelle-interactive-and-tool-framework]
Role in HOL-TestGen
HOL-TestGen is described as a formal tool built on top of Isabelle/HOL. While Isabelle/HOL is usually viewed as a proof assistant, HOL-TestGen uses it as a document-centric modeling environment for test background theories, test specifications, and test generation methods implemented with Isabelle tactic procedures. [hol-testgen-built-on-isabelle]
In the cited case study, HOL-TestGen benefits from Isabelle/HOL because test specifications are expressed in higher-order logic and can directly reuse existing verification models. The paper highlights the tight integration of verification and testing as a distinguishing feature of HOL-TestGen. [hol-testgen-reuses-verification-models]
Use in the Verisoft VAMP case study
In the Verisoft project, a formal model for a processor and a small operating system was developed in Isabelle/HOL. The case study reused the processor model to generate test cases for checking whether hardware conforms to the VAMP processor model. [verisoft-models-in-isabelle]
The evidence also states that, in the Verisoft context, an Isabelle/HOL programmer’s-model specification of the VAMP processor was introduced. The VAMP processor model is defined as transitions over instruction-set-architecture configurations. These configurations include a program counter, delayed program counter, general-purpose registers, special-purpose registers, and a memory model. [vamp-programmers-model]
The VAMP assembler model was represented as an Isabelle theory abstracting the instruction-set architecture: addresses are represented by natural numbers, register and memory contents by integers, instructions by an abstract datatype with readable names, and the assembler configuration by a HOL record type with fields including program counters, register lists, and a memory mapping. [vamp-assembler-theory]
Technical significance in the cited work
The cited microprocessor test-generation study built on an existing model developed in Isabelle/HOL and used HOL-TestGen, an Isabelle/HOL extension, to synthesize conformance test programs. The generated programs were used in scenarios involving real hardware in the loop, and the approach directly benefited from existing Isabelle/HOL models and formal proofs. [case-study-isabelle-hol-and-hol-testgen]