caldron
发表于 2025-3-23 13:00:10
A functional approach for formalizing regular hardware structures,ut on regular hardware structures which are described by means of primitive recursion. PML-descriptions can easily be converted to syntactic structures, called hardware formulae, which can then be verified by the MEPHISTO system.
粗俗人
发表于 2025-3-23 15:50:33
Alternative proof procedures for finite-state machines in higher-order logic,entable proof methods which do not use knowledge of fixpoint theorems are given. Since these methods are incomplete, the second category exploits an external program for computing fixpoint lemmata which can then be easily proved in HOL.
Aggrandize
发表于 2025-3-23 20:50:22
A formalization of abstraction in LAMBDA,model only if they are satisfied in the model itself. We illustrate how the proof of an inductive step in the verification of a satisfaction relation for an infinite model can be reduced to the verification of a satisfaction relation for a very small finite model.
cavity
发表于 2025-3-23 22:46:12
Report on the UCD microcoded Viper verification project, We redesigned Viper as a hierarchy of five interpreters, each of which is an instance of the generic interpreter. The top level specifies the Viper instruction set and the lowest level specifies an abstraction of a conventional electronic block model. The design and verification was carried out in approximately one person-year.
江湖郎中
发表于 2025-3-24 04:34:57
0302-9743 umbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contain
LANCE
发表于 2025-3-24 10:30:05
978-3-540-57826-0Springer-Verlag Berlin Heidelberg 1994
小虫
发表于 2025-3-24 13:27:17
Higher Order Logic Theorem Proving and Its Applications978-3-540-48346-5Series ISSN 0302-9743 Series E-ISSN 1611-3349
Introduction
发表于 2025-3-24 18:06:52
http://reply.papertrans.cn/43/4270/426975/426975_18.png
噱头
发表于 2025-3-24 21:36:50
https://doi.org/10.1007/3-540-57826-9Automatisches Beweisen; Hardwareverifikation; Higher Order Logic System (HOL); Higher-Order-Logic Syste
过剩
发表于 2025-3-24 23:43:28
Structure and behaviour in hardware verification,In this paper we review how hardware has been described in the formal hardware verification community. Recent developments in hardware description are evaluated against the background of the use of hardware description languages, and also in relation to programming languages. The notions of structure and behaviour are crucial to this discussion.