CHARME
2001
Springer
14 years 4 months ago
2001
Springer
CHARME
2001
Springer
14 years 4 months ago
2001
Springer
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 ...
CHARME
2001
Springer
14 years 4 months ago
2001
Springer
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...
CHARME
2001
Springer
14 years 4 months ago
2001
Springer
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...
CHARME
2001
Springer
14 years 4 months ago
2001
Springer
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...
CHARME
2001
Springer
14 years 4 months ago
2001
Springer
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 ...
CHARME
2001
Springer
14 years 5 months ago
2001
Springer
CHARME
2001
Springer
14 years 5 months ago
2001
Springer
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 ...
CHARME
2001
Springer
14 years 5 months ago
2001
Springer
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...
CHARME
2001
Springer
14 years 5 months ago
2001
Springer
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...