Mandayam K. Srivas

Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

2021

A formal methods approach to predicting new features of the eukaryotic vesicle traffic system.

[BibT_eX]

[DOI]

Acta Informatica, 2021

2018

2LS: Memory Safety and Non-termination - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

2017

Concurrent Program Verification with Invariant-Guided Underapproximation.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2017

Compositional Safety Refutation Techniques.

[BibT_eX]

[DOI]

Kumar Madhukar

Peter Schrammel

Proceedings of the Automated Technology for Verification and Analysis, 2017

2015

Equivalence Checking Using Trace Partitioning.

[BibT_eX]

[DOI]

Proceedings of the 2015 IEEE Computer Society Annual Symposium on VLSI, 2015

Accelerating Invariant Generation.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Verifying synchronous reactive systems using lazy abstraction.

[BibT_eX]

[DOI]

Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, 2015

2014

Formal Hardware/Software Co-Verification of Embedded Power Controllers.

[BibT_eX]

[DOI]

Pallab Dasgupta

Rajdeep Mukherjee

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014

2003

Formal Verification of a Complex Pipelined Processor.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2003

A Practical Methodology for Verifying Pipelined Microarchitectures.

[BibT_eX]

[DOI]

IEEE Des. Test Comput., 2003

2000

Verifying Advanced Microarchitectures that Support Speculation and Exceptions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Modular Verification of SRT Division.

[BibT_eX]

[DOI]

Harald Rueß

Natarajan Shankar

Formal Methods Syst. Des., 1999

A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Decomposing the Proof of Correctness of pipelined Microprocessors.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

Industrial Strength Formal Verification Techniques for Hardware Designs.

[BibT_eX]

[DOI]

Sreeranga P. Rajan

Natarajan Shankar

Proceedings of the 10th International Conference on VLSI Design (VLSI Design 1997), 1997

Systematic Formal Verification of Interpreters.

[BibT_eX]

[DOI]

David Cyrluk

John M. Rushby

Proceedings of the First IEEE International Conference on Formal Engineering Methods, 1997

Hardware Verification Using PVS.

[BibT_eX]

[DOI]

Harald Rueß

David Cyrluk

Proceedings of the Formal Hardware Verification - Methods and Systems in Comparison, 1997

1996

Applying Formal Verification to the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods.

[BibT_eX]

[DOI]

Steven P. Miller

Formal Methods Syst. Des., 1996

PVS: Combining Specification, Proof Checking, and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods.

[BibT_eX]

[DOI]

Steven P. Miller

Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995

Experiences in applying formal methods to the analysis of software and system requirements.

[BibT_eX]

[DOI]

Alan R. Flora-Holmquist

Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995

Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification.

[BibT_eX]

[DOI]

David Cyrluk

Proceedings of the 1995 International Conference on Computer Design (ICCD '95), 1995

An Integration of Model Checking with Automated Proof Checking.

[BibT_eX]

[DOI]

S. Rajan

Natarajan Shankar

Proceedings of the Computer Aided Verification, 1995

1994

A Tutorial on Using PVS for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

Effective Theorem Proving for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

1993

Using PVS to Prove Some Theorems Of David Parnas.

[BibT_eX]

[DOI]

John M. Rushby

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

1992

Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification.

[BibT_eX]

Proceedings of the Theorem Provers in Circuit Design, 1992

1991

Bridging the formal methods gap: a computer-aided verification tool for hardware designs.

[BibT_eX]

[DOI]

Proceedings of the Compcon Spring '91, San Francisco, 1991

1990

Formal Verification of a Pipelined Microprocessor.

[BibT_eX]

[DOI]

IEEE Softw., 1990

Inference Rules and Proof Procedures for Inequations.

[BibT_eX]

[DOI]

J. Log. Program., 1990

A Computer-Aided Verification Tool for Finite State Controller Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer-Aided Verification, 1990

1989

Negation with Logical Variables in Conditional Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

Verification of a Pipelined Microprocessor Using Clio.

[BibT_eX]

[DOI]

Proceedings of the Hardware Specification, 1989

1988

Computability and Implementability Issues in Abstract Data Types.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1988

Implementing Functional Programs Using Mutable Abstract Data Types.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1988

1987

Automatic Inductive Theorem Proving Using Prolog.

[BibT_eX]

[DOI]

Jieh Hsiang

Theor. Comput. Sci., 1987

Reasoning in Systems of Equations and Inequations.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987

Conditional Specification with Inequational Assumptions.

[BibT_eX]

[DOI]

Proceedings of the Conditional Term Rewriting Systems, 1987

1986

Function Definitions in Term Rewriting and Applicative Programming

[BibT_eX]

[DOI]

Inf. Control., December, 1986

Deriving Module Interconnectivity from Behavioral Specifications and Coupling a VLSI Layout Editor for Error-Free Routing.

[BibT_eX]

Nai-Chi Lee

David R. Smith

Proceedings of the Fall Joint Computer Conference, November 2-6, 1986, Dallas, Texas, USA, 1986

1985

A Rewrite Rule Based Approach for Synthesizing Abstract Data Types.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Software Development, 1985

A PROLOG Environment for Developing and Reasoning about Data Types.

[BibT_eX]

[DOI]

Jieh Hsiang

Proceedings of the Mathematical Foundations of Software Development, 1985

PROLOG-Based Inductive Theorem Proving.

[BibT_eX]

[DOI]

Jieh Hsiang

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1985

1980

Expressiveness of the Operation Set of a Data Abstraction.

[BibT_eX]

[DOI]