Email Gateway (Aug 18 2022 at 12:10): Email Gateway (Aug 18 2022 at 12:10):From: li yongjian <lyj238@gmail.com>
Hi,
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
Isabelle.
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 verification.
regards!
Email Gateway (Aug 18 2022 at 12:10):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
li yongjian wrote:
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 http://users.rsise.anu.edu.au/~jeremy/pubs/l4/
Jeremy
Email Gateway (Aug 18 2022 at 12:10):From: Julien Schmaltz <julien.schmaltz@googlemail.com>
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: www.verisoft.de.
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.
[more]<http://www.cs.ru.nl/~julien/Julien%20at%20Nijmegen/FMCAD07.html>
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: http://www.cs.ru.nl/~julien/Julien%20at%20Nijmegen/FMCAD07.html
Best regards,
Julien
Email Gateway (Aug 18 2022 at 12:10):From: Dirk Leinenbach <Dirk.Leinenbach@dfki.de>
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,
Dirk
[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 = {http://www-wjp.cs.uni-sb.de/publikationen/Alkassar_AHK-.pdf},
BOOKTITLE = {Proceedings, 4th International Verification Workshop
(VERIFY), Bremen, Germany},
PUBLISHER = {CEUR-WS Workshop Proceedings},
EDITOR = {B. Beckert},
EE = {http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/},
}
[2] @inproceedings{Tv05,
AUTHOR = {Tverdyshev, Sergey},
TITLE = {Combination of Isabelle/HOL with Automatic Tools},
VOLUME = {3717},
YEAR = {2005},
PAGES = {302-309},
URL = {http://www-wjp.cs.uni-sb.de/publikationen/Tv05.pdf},
SERIES = {Lecture Notes in Computer Science},
BOOKTITLE = {FroCoS 2005},
PUBLISHER = {Springer Verlag},
EDITOR = {Bernhard Gramlich},
SCHOOL = {Saarland University},
EE = {http://dx.doi.org/10.1007/11559306_18},
}
[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:
Last updated: May 03 2024 at 08:18 UTC