Sciweavers

FAC
1998
111views more  FAC 1998»
13 years 10 months ago
A Formal Axiomatization for Alphabet Reasoning with Parametrized Processes
In the process-algebraic veri cation of systems with three or more components put in parallel, alphabet axioms are considered to be very useful. These are rules that exploit the i...
Henri Korver, M. P. A. Sellink
TPCD
1994
157views Hardware» more  TPCD 1994»
14 years 4 days ago
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization
Theorem proving techniques are particularly well suited for reasoning about arithmetic above the bit level and for relating di erent f abstraction. In this paper we show how a non-...
John W. O'Leary, Miriam Leeser, Jason Hickey, Mark...
FTCS
1998
84views more  FTCS 1998»
14 years 5 days ago
On the Use of Formal Techniques for Validation
The traditional use of formal methods has been for the veri cation of algorithms or protocols. Given the high cost and limitations in state space coverage provided by conventional...
Neeraj Suri, Purnendu Sinha
REX
1991
14 years 2 months ago
Logics and Models of Real Time: A Survey
We survey logic-based and automata-based languages and techniques for the speci cation and veri cation of real-time systems. In particular, we discuss three syntactic extensions of...
Rajeev Alur, Thomas A. Henzinger
MPC
1995
Springer
116views Mathematics» more  MPC 1995»
14 years 2 months ago
Computer-Aided Computing
PVS is a highly automated framework for speci cation and veri cation. We show how the language and deduction features of PVS can be used to formalize, mechanize, and apply some us...
Natarajan Shankar
FMCAD
2000
Springer
14 years 2 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...
ICALP
1992
Springer
14 years 2 months ago
What Good Are Digital Clocks?
Real-time systems operate in \real," continuous time and state changes may occur at any real-numbered time point. Yet many veri cation methods are based on the assumption that...
Thomas A. Henzinger, Zohar Manna, Amir Pnueli
CAV
1992
Springer
96views Hardware» more  CAV 1992»
14 years 2 months ago
State-Space Caching Revisited
State-space caching is a veri cation technique for nite-state concurrent systems. It performs an exhaustive exploration of the state space of the system being checked while storin...
Patrice Godefroid, Gerard J. Holzmann, Didier Piro...
ICALP
1994
Springer
14 years 2 months ago
Liveness in Timed and Untimed Systems
When provingthe correctness of algorithmsin distributed systems, one generally considers safety conditions and liveness conditions. The Input Output I O automaton model and its ti...
Rainer Gawlick, Roberto Segala, Jørgen F. S...
LICS
1993
IEEE
14 years 2 months ago
Verifying Programs with Unreliable Channels
We consider the veri cation of a particular class of in nite-state systems, namely systems consisting of nite-state processes that communicate via unbounded lossy FIFO channels. T...
Parosh Aziz Abdulla, Bengt Jonsson