Sciweavers

Share
ICCD
2000
IEEE
119views Hardware» more  ICCD 2000»
9 years 10 months ago
Source-Level Transformations for Improved Formal Verification
A major obstacle to widespread acceptance of formal verification is the difficulty in using the tools effectively. Although learning the basic syntax and operation of a formal ver...
Brian D. Winters, Alan J. Hu
FSTTCS
2000
Springer
9 years 10 months ago
Formal Verification of the Ricart-Agrawala Algorithm
Abstract. This paper presents the first formal verification of the RicartAgrawala algorithm [RA81] for distributed mutual exclusion of an arbitrary number of nodes. It uses the Tem...
Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ar...
FMCAD
2000
Springer
9 years 10 months ago
Do You Trust Your Model Checker?
Abstract. In this paper we describe the formal specification and verification of the efficient algorithm for real-time model checking implemented in the model checker RAVEN. It was...
Wolfgang Reif, Jürgen Ruf, Gerhard Schellhorn...
CHARME
2003
Springer
97views Hardware» more  CHARME 2003»
9 years 10 months ago
Coverage Metrics for Formal Verification
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete ...
Hana Chockler, Orna Kupferman, Moshe Y. Vardi
CHARME
2001
Springer
92views Hardware» more  CHARME 2001»
9 years 10 months ago
Formal Verification of the VAMP Floating Point Unit
We report on the formal verification of the floating point unit used in the VAMP processor. The FPU is fully IEEE compliant, and supports denormals and exceptions in hardware. The ...
Christoph Berg, Christian Jacobi 0002
DATE
2004
IEEE
97views Hardware» more  DATE 2004»
9 years 10 months ago
A Formal Verification Methodology for Checking Data Integrity
Formal verification techniques have been playing an important role in pre-silicon validation processes. One of the most important points considered in performing formal verificati...
Yasushi Umezawa, Takeshi Shimizu
ASIAN
2006
Springer
118views Algorithms» more  ASIAN 2006»
9 years 10 months ago
An Approach to Formal Verification of Arithmetic Functions in Assembly
Abstract. It is customary to write performance-critical parts of arithmetic functions in assembly: this enables finely-tuned algorithms that use specialized processor instructions....
Reynald Affeldt, Nicolas Marti
HYBRID
2007
Springer
9 years 11 months ago
Safety Verification of an Aircraft Landing Protocol: A Refinement Approach
Abstract. In this paper, we propose a new approach for formal verification of hybrid systems. To do so, we present a new refinement proof technique, a weak refinement using step in...
Shinya Umeno, Nancy A. Lynch
GLVLSI
2007
IEEE
151views VLSI» more  GLVLSI 2007»
9 years 11 months ago
Hand-in-hand verification of high-level synthesis
This paper describes a formal verification methodology of highnthesis (HLS) process. The abstraction level of the input to HLS is so high compared to that of the output that the v...
Chandan Karfa, Dipankar Sarkar, Chittaranjan A. Ma...
ASYNC
2007
IEEE
129views Hardware» more  ASYNC 2007»
9 years 11 months ago
Formal Verification of CHP Specifications with CADP Illustration on an Asynchronous Network-on-Chip
Few formal verification techniques are currently available for asynchronous designs. In this paper, we describe a new approach for the formal verification of asynchronous architec...
Gwen Salaün, Wendelin Serwe, Yvain Thonnart, ...
books