Association for Computing (2009)
Formal methods long have been touted as a means to produce “provably correct implementations. ” It is only recently, however, with rather more
Verification Verification of a Multiplier: 64 Bits and Beyond (2007)
R. P. Kurshan, R. P. Kurshan, Leslie Lamport
Abstract. Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the...
Membership Questions for Timed and Hybrid Automata (1998)
Alur, Rajeev, Kurshan, R. P, Viswanathan, M.
Timed and hybrid automata are extensions of finite-state machines for formal modeling of embedded systems with both discrete and continuous components. Reachability problems for these automata are...
Membership Questions for Timed and Hybrid Automata (1998)
R. Alur, R.P. Kurshan, M. Viswanathan
Timed and hybrid automata are extensions of finite-state machines for formal modeling of embedded systems with both discrete and continuous components. Reachability problems for these automata are...
Formal Verification In a Commercial Setting (1997)
This tutorial addresses the following questions: ffl why do formal verification? ffl who is doing it today? ffl what are they doing? ffl how are they doing it? ffl what about the future? Introduction...
Formal Verification in a Commercial Setting (1997)
This tutorial addresses the following questions: ffl why do formal verification? ffl who is doing it today? ffl what are they doing? ffl how are they doing it? ffl what about the future? Introduction...
Efficient Regression Verification (1996)
Hardin Kurshan, R. H. Hardin, R. P. Kurshan, K. L. Mcmillan, J. A. Reeds
A significant problem in commercial-size development projects is to ensure that the process of fixing one design problem does not introduce another. In the context of conventional testing this is...
Modelling Asynchrony with a Synchronous Model (1995)
R. P. Kurshan, M. Merritt, A. Orda, S. R. Sachs
The I/O Automaton paradigm of Lynch and Tuttle models asynchrony through an interleaving parallel composition and generalizes more common interleaving models based upon message-passing, such as...
Verification of a Multiplier: 64 Bits and beyond (1993)
R.P. Kurshan, R. P. Kurshan, Leslie Lamport
. Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the induction...
Verification of a multiplier: 64 bits and beyond (1993)
Abstract. Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the...
Aided Verification Verification of a Multiplier: 64 Bits and Beyond (1993)
R. P. Kurshan, Leslie Lamport, R. P. Kurshan, Leslie Lamport
Abstract. Verifying a 64-bit multiplier has a computational complexity that puts it beyond the grasp of current finite-state algorithms, including those based upon homomorphic reduction, the...
Timing Verification by Successive Approximation (1992)
R. Alur, A. Itai, R. P. Kurshan, M. Yannakakis
. We present an algorithm for verifying that a model M with timing constraints satisfies a given temporal property T . The model M is given as a parallel composition of !-automata P i , where each...
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems (1992)
CLARKE, E. M., GRUMBERG, O., KURSHAN, R. P.
The paper provides a synthesis between two main approaches to automatic verification of finite-state systems: temporal logic model checking and language containment of automata on infinite tapes. A...