Sciweavers

CHARME
2001
Springer
98views Hardware» more  CHARME 2001»
13 years 7 months ago
Temporal Properties of Self-Timed Rings
Anthony Winstanley, Mark R. Greenstreet
CHARME
2001
Springer
136views Hardware» more  CHARME 2001»
13 years 7 months ago
Deriving Real-Time Programs from Duration Calculus Specifications
In this paper we present a syntactical approach for deriving real-time programs from a formal specification of the requirements of real-time systems. The main idea of our approach ...
François Siewe, Dang Van Hung
CHARME
2001
Springer
162views Hardware» more  CHARME 2001»
13 years 7 months ago
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
We consider the formal verification of the cache coherence protocol of the Stanford FLASH multiprocessor for N processors. The proof uses the SMV proof assistant, a proof system ba...
Kenneth L. McMillan
CHARME
2001
Springer
107views Hardware» more  CHARME 2001»
13 years 7 months ago
Using Combinatorial Optimization Methods for Quantification Scheduling
Model checking is the process of verifying whether a model of a concurrent system satisfies a specified temporal property. Symbolic algorithms based on Binary Decision Diagrams (BD...
Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, Jame...
CHARME
2001
Springer
92views Hardware» more  CHARME 2001»
13 years 7 months ago
Induction-Oriented Formal Verification in Symmetric Interconnection Networks
The framework of this paper is the formal specification and proof of applications distributed on symmetric interconnection networks, e.g. the torus or the hypercube. The algorithms...
Eric Gascard, Laurence Pierre
CHARME
2001
Springer
92views Hardware» more  CHARME 2001»
13 years 7 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
CHARME
2001
Springer
109views Hardware» more  CHARME 2001»
13 years 8 months ago
Formally-Based Design Evaluation
Kenneth J. Turner, Ji He
CHARME
2001
Springer
117views Hardware» more  CHARME 2001»
13 years 8 months ago
A Higher-Level Language for Hardware Synthesis
We describe SAFL+: a call-by-value, parallel language in the style of ML which combines imperative, concurrent and functional programming. Synchronous channels allow communication ...
Richard Sharp, Alan Mycroft
CHARME
2001
Springer
105views Hardware» more  CHARME 2001»
13 years 8 months ago
Net Reductions for LTL Model-Checking
We present a set of reduction rules for LTL model-checking of 1-safe Petri nets. Our reduction techniques are of two kinds: (1) Linear programming techniques which are based on wel...
Javier Esparza, Claus Schröter
CHARME
2001
Springer
133views Hardware» more  CHARME 2001»
13 years 8 months ago
View from the Fringe of the Fringe
Formal analysis remains outside the mainstream of system design practice. Interactive methods and tools are regarded by some to be on the margin of useful research in this area. Al...
Steven D. Johnson