agitate
发表于 2025-3-25 03:37:45
Formal verification of counterflow pipeline architecture,Some properties of the Sproull counterflow pipeline architecture are formally verified using automata theory and higher order logic in the HOL theorem prover. The proof steps are presented. Despite the pipeline being a non-deterministic asynchronous system, the verification proceeded with minimal time and effort.
OREX
发表于 2025-3-25 08:44:31
http://reply.papertrans.cn/43/4270/426976/426976_22.png
landfill
发表于 2025-3-25 14:28:49
http://reply.papertrans.cn/43/4270/426976/426976_23.png
hazard
发表于 2025-3-25 17:28:28
Floating point verification in HOL,nsive and rigorous theory of real analysis. We explain how it can be used in floating point verification, illustrating our remarks with complete verifications of simple square-root and (natural) logarithm algorithms.
嫌恶
发表于 2025-3-25 23:24:42
978-3-540-60275-0Springer-Verlag Berlin Heidelberg 1995
宿醉
发表于 2025-3-26 03:12:20
Higher Order Logic Theorem Proving and Its Applications978-3-540-44784-9Series ISSN 0302-9743 Series E-ISSN 1611-3349
增减字母法
发表于 2025-3-26 06:36:30
http://reply.papertrans.cn/43/4270/426976/426976_27.png
环形
发表于 2025-3-26 11:08:06
0302-9743 n Aspen Grove, Utah, USA in September 1995..The 26 papers selected by the program committee for inclusion in this volume document the advances in the field achieved since the predecessor conference. The papers presented fall into three general categories: representation of formalisms in higher order
Haphazard
发表于 2025-3-26 13:00:00
Combining decision procedures in the HOL system,ables are the only information that need be communicated between them. Thus, code for deciding the component theories can be reused in a combined procedure and the latter can easily be extended. In addition, efficiency techniques used in the component procedures can be retained in the combined procedure.
支柱
发表于 2025-3-26 16:54:45
A practical method for reasoning about distributed systems in a theorem prover,in the system LAMBDA is described. Motivated by the importance of practicality in an industrial setting, a simple representation of TLA is combined with extended reasoning functions. Translation of user programs, safety, liveness, and refinement proofs are depicted by way of a parametric mutual exclusion algorithm.