Sciweavers

IFL
2000
Springer
14 years 4 months ago
Verifying Generic Erlang Client-Server Implementations
Thomas Arts, Thomas Noll
FTRTFT
2000
Springer
14 years 4 months ago
Modeling Faults of Distributed, Reactive Systems
Formal methods can improve the development of systems with high quality requirements, since they usually o er a precise, nonambiguous speci cation language and allow rigorous veri ...
Max Breitling
FMCAD
2000
Springer
14 years 4 months ago
Visualizing System Factorizations with Behavior Tables
Abstract. Behavior tables are a design formalization intended to support interactive design derivation for hardware and embedded systems. It is a reformulation of the DDD transform...
Alex Tsow, Steven D. Johnson
FMCAD
2000
Springer
14 years 4 months ago
Monitor-Based Formal Specification of PCI
Bus protocols are hard to specify correctly, and yet it is often critical and highly beneficial that their specifications are correct, complete, and unambiguous. The informal speci...
Kanna Shimizu, David L. Dill, Alan J. Hu
FMCAD
2000
Springer
14 years 4 months ago
Checking Safety Properties Using Induction and a SAT-Solver
We take a fresh look at the problem of how to check safety properties of finite state machines. We are particularly interested in checking safety properties with the help of a SAT-...
Mary Sheeran, Satnam Singh, Gunnar Stålmarck
FMCAD
2000
Springer
14 years 4 months ago
Formal Verification of Floating Point Trigonometric Functions
Abstract. We have formal verified a number of algorithms for evaluating transcendental functions in double-extended precision floating point arithmetic in the Intel
John Harrison
FMCAD
2000
Springer
14 years 4 months ago
SAT-Based Image Computation with Application in Reachability Analysis
Image computation nds wide application in VLSI CAD, such as state reachability analysis in formal veri cation and synthesis, combinational veri cation, combinational and sequential...
Aarti Gupta, Zijiang Yang, Pranav Ashar, Anubhav G...
FMCAD
2000
Springer
14 years 4 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...
FMCAD
2000
Springer
14 years 4 months ago
The Semantics of Verilog Using Transition System Combinators
Abstract. Since the advent of model checking it is becoming more common for languages to be given a semantics in terms of transition systems. Such semantics allow to model check pr...
Gordon J. Pace