Sciweavers

FROCOS
2005
Springer

Combination of Isabelle/HOL with Automatic Tools

13 years 9 months ago
Combination of Isabelle/HOL with Automatic Tools
We describe results and status of a sub project of the Verisoft [1] project. While the Verisoft project aims at verification of a complete computer system starting with hardware and up to user applications, the goal of our sub project is an efficient hardware verification. We use the Isabelle theorem prover [2] as the major tool for hardware design and verification. Since many hardware verification problems can be efficiently solved by automatic tools, we combine Isabelle with model checkers and SAT solvers. This combination of tools speeds up verification of hardware and simplifies sharing of the results with verification of the whole computer system. To increase the range of problems which can be solved by external tools we implemented in Isabelle several algorithms for handling uninterpreted functions and traction. The resulting combination was applied to verify many different hardware circuits, automata, and processors. In our project we use open source tools that are free...
Sergey Tverdyshev
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FROCOS
Authors Sergey Tverdyshev
Comments (0)