2003 |
34 | EE | Ravi Hosabettu,
Ganesh Gopalakrishnan,
Mandayam K. Srivas:
Formal Verification of a Complex Pipelined Processor.
Formal Methods in System Design 23(2): 171-213 (2003) |
33 | EE | Ravi Hosabettu,
Ganesh Gopalakrishnan,
Mandayam K. Srivas:
A Practical Methodology for Verifying Pipelined Microarchitectures.
IEEE Design & Test of Computers 20(4): 4-14 (2003) |
2000 |
32 | | Ravi Hosabettu,
Ganesh Gopalakrishnan,
Mandayam K. Srivas:
Verifying Advanced Microarchitectures that Support Speculation and Exceptions.
CAV 2000: 521-537 |
1999 |
31 | EE | Ravi Hosabettu,
Ganesh Gopalakrishnan,
Mandayam K. Srivas:
A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer.
CHARME 1999: 8-22 |
30 | | Harald Rueß,
Natarajan Shankar,
Mandayam K. Srivas:
Modular Verification of SRT Division.
Formal Methods in System Design 14(1): 45-73 (1999) |
1998 |
29 | | Ravi Hosabettu,
Mandayam K. Srivas,
Ganesh Gopalakrishnan:
Decomposing the Proof of Correctness of pipelined Microprocessors.
CAV 1998: 122-134 |
1997 |
28 | | Mandayam K. Srivas,
Harald Rueß,
David Cyrluk:
Hardware Verification Using PVS.
Formal Hardware Verification 1997: 156-205 |
27 | | David Cyrluk,
John M. Rushby,
Mandayam K. Srivas:
Systematic Formal Verification of Interpreters.
ICFEM 1997: 140- |
26 | EE | S. P. Rajan,
Natarajan Shankar,
Mandayam K. Srivas:
Industrial Strength Formal Verification Techniques for Hardware Designs.
VLSI Design 1997: 208-212 |
1996 |
25 | | Mandayam K. Srivas,
Albert John Camilleri:
Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings
Springer 1996 |
24 | | Harald Rueß,
Natarajan Shankar,
Mandayam K. Srivas:
Modular Verification of SRT Division.
CAV 1996: 123-134 |
23 | | Sam Owre,
S. Rajan,
John M. Rushby,
Natarajan Shankar,
Mandayam K. Srivas:
PVS: Combining Specification, Proof Checking, and Model Checking.
CAV 1996: 411-414 |
22 | | Mandayam K. Srivas,
Steven P. Miller:
Applying Formal Verification to the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods.
Formal Methods in System Design 8(2): 153-188 (1996) |
1995 |
21 | | S. Rajan,
Natarajan Shankar,
Mandayam K. Srivas:
An Integration of Model Checking with Automated Proof Checking.
CAV 1995: 84-97 |
20 | EE | David Cyrluk,
Mandayam K. Srivas:
Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification.
ICCD 1995: 538- |
1994 |
19 | | David Cyrluk,
S. Rajan,
Natarajan Shankar,
Mandayam K. Srivas:
Effective Theorem Proving for Hardware Verification.
TPCD 1994: 203-222 |
18 | | Sam Owre,
John M. Rushby,
Natarajan Shankar,
Mandayam K. Srivas:
A Tutorial on Using PVS for Hardware Verification.
TPCD 1994: 258-279 |
1993 |
17 | | John M. Rushby,
Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas.
HUG 1993: 163-173 |
1992 |
16 | | Mark Bickford,
Mandayam K. Srivas:
Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification.
TPCD 1992: 225-251 |
1990 |
15 | | Mandayam K. Srivas,
Mark Bickford:
Formal Verification of a Pipelined Microprocessor.
IEEE Software 7(5): 52-64 (1990) |
14 | | Chilukuri K. Mohan,
Mandayam K. Srivas,
Deepak Kapur:
Inference Rules and Proof Procedures for Inequations.
J. Log. Program. 9(1): 75-104 (1990) |
1989 |
13 | | Mark Bickford,
Mandayam K. Srivas:
Verification of a Pipelined Microprocessor Using Clio.
Hardware Specification, Verification and Synthesis 1989: 307-332 |
12 | | Chilukuri K. Mohan,
Mandayam K. Srivas:
Negation with Logical Variables in Conditional Rewriting.
RTA 1989: 292-310 |
1988 |
11 | | Ganesh Gopalakrishnan,
Mandayam K. Srivas:
Implementing Functional Programs Using Mutable Abstract Data Types.
Inf. Process. Lett. 26(6): 277-286 (1988) |
10 | | Deepak Kapur,
Mandayam K. Srivas:
Computability and Implementability Issues in Abstract Data Types.
Sci. Comput. Program. 10(1): 33-63 (1988) |
1987 |
9 | | Chilukuri K. Mohan,
Mandayam K. Srivas:
Conditional Specification with Inequational Assumptions.
CTRS 1987: 161-178 |
8 | | Chilukuri K. Mohan,
Mandayam K. Srivas,
Deepak Kapur:
Reasoning in Systems of Equations and Inequations.
FSTTCS 1987: 305-325 |
7 | | Jieh Hsiang,
Mandayam K. Srivas:
Automatic Inductive Theorem Proving Using Prolog.
Theor. Comput. Sci. 54: 3-28 (1987) |
1986 |
6 | | Nai-Chi Lee,
David R. Smith,
Mandayam K. Srivas:
Deriving Module Interconnectivity from Behavioral Specifications and Coupling a VLSI Layout Editor for Error-Free Routing.
FJCC 1986: 864-869 |
5 | | Chilukuri K. Mohan,
Mandayam K. Srivas:
Function Definitions in Term Rewriting and Applicative Programming
Information and Control 71(3): 186-217 (1986) |
1985 |
4 | | Jieh Hsiang,
Mandayam K. Srivas:
PROLOG-Based Inductive Theorem Proving.
FSTTCS 1985: 129-149 |
3 | | Deepak Kapur,
Mandayam K. Srivas:
A Rewrite Rule Based Approach for Synthesizing Abstract Data Types.
TAPSOFT, Vol.1 1985: 188-207 |
2 | | Jieh Hsiang,
Mandayam K. Srivas:
A PROLOG Environment for Developing and Reasoning about Data Types.
TAPSOFT, Vol.2 1985: 276-293 |
1980 |
1 | | Deepak Kapur,
Mandayam K. Srivas:
Expressiveness of the Operation Set of a Data Abstraction.
POPL 1980: 139-153 |