Re: [isabelle] do hardware verification by Isabelle

Hi Li,

in addition to Julian's work in Verisoft's automotive sub project, Sergey Tverdyshev et al. have worked on the verification of a comlex out-of-order microprocessor design (the VAMP processor); see e.g. [1,2]. For additional information about recent work in the automotive sub project see also [3,4].

Best regards,


[1] @inproceedings{Alkassar_AHK-,
AUTHOR = {Alkassar, E. and Hillebrand, M. and Knapp, S. and Rusev, R. and Tverdyshev, S.},
TITLE = {Formal Device and Programming Model for a Serial Interface},
YEAR = {2007},
PAGES = {4--20},
URL = {},
BOOKTITLE = {Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany},
PUBLISHER = {CEUR-WS Workshop Proceedings},
EDITOR = {B. Beckert},
EE = {},

[2] @inproceedings{Tv05,
AUTHOR = {Tverdyshev, Sergey},
TITLE = {Combination of Isabelle/HOL with Automatic Tools},
VOLUME = {3717},
YEAR = {2005},
PAGES = {302-309},
URL = {},
SERIES = {Lecture Notes in Computer Science},
BOOKTITLE = {FroCoS 2005},
PUBLISHER = {Springer Verlag},
EDITOR = {Bernhard Gramlich},
SCHOOL = {Saarland University},
EE = {},

[3] @inproceedings{Alkassar_DIPES08-??,
AUTHOR = {Alkassar, Eyad and Böhm, Peter and Knapp, Steffen},
TITLE = {Formal Correctness of a Gate-Level Automotive Bus Controller Implementation},
YEAR = {2008},
BOOKTITLE = {6th IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES08). To appear},
PUBLISHER = {Springer Science and Business Media},

[4] inproceedings{ABK08:Memo08-??,
AUTHOR = {Alkassar, Eyad and Böhm, Peter and Knapp, Steffen},
TITLE = {Correctness of a Fault-Tolerant Real-Time Scheduler Algorithm and its Hardware Implementation},
YEAR = {2008},
PAGES = {175--186},
BOOKTITLE = {Formal Methods and Models for Codesign (MEMOCODE'2008)},
PUBLISHER = {IEEE Computer Society Press},

Julien Schmaltz wrote:
Hi Li,
The german Verisoft project includes hardware verification using Isabelle,
and also using a combination of the NuSMV model checker with Isabelle. You
may find papers about that on their website:

When I was involved in this project, I worked on the verification of low
level time-triggered hardware:

A Formal Model of Clock Domain Crossing and Automated Verification of
Time-Triggered Hardware.
 Julien Schmaltz. 7th International Conference on Formal Methods in
Computer-Aided Design (FMCAD'07), pp. 223-230, Austin, TX, USA, November
11-14, IEEE Society, 2007 (c)IEEE

On-line at:

Best regards,


On Thu, Jul 10, 2008 at 2:58 AM, Jeremy Dawson <jeremy at>

li yongjian wrote:

  I want to know who has done some theorem proof work on
hardware verification by using Isabelle.

  I know HOL has been extensively used in harware by Mike
Gordon, Tom mellem, and so on. There are large nuber of papers,
 case studies, proofs
  But I found little  work which does harware verification by
  By google search, I found larry's old project introduction:
Combining HOL with Isabelle. But I can not find intereting papers
on this field.

  I fact, I have a HOL proof theories which I'm interested  in, but
I'm not familar with HOL. Do I need rewrite a new version of
Isabelle script basing on the HOL, or learn  HOL to do harware


The L4 project includes substantial hardware verification, and there are
papers about that, including my

Jeremy E. Dawson, Isabelle Theories for Machine Words. In Seventh
International Workshop on Automated Verification of Critical Systems
(AVOCS'07), Oxford, September 2007, Electronic Notes in Theoretical Computer
Science, Elsevier, to appear. (Also in Proceedings of TPHOLs 2007 Emerging
Trends, Internal Report 364/07, Department of Computer Science, University
of Kaiserslautern)

On-line at


Dirk Leinenbach
German Research Center for Artificial Intelligence
Saarbrücken, Germany
Building E1 1, Room 4.06

phone: +49 - 681 / 302 - 57379
fax:   +49 - 681 / 302 - 4132

Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH Trippstadter
Strasse 122, D-67663 Kaiserslautern, Germany

Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.