Steven M. German

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2007

Transaction Based Modeling and Verification of Hardware Protocols.

[BibT_eX]

[DOI]

Xiaofang Chen

Ganesh Gopalakrishnan

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

2006

Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications.

[BibT_eX]

[DOI]

Ritwik Bhattacharya

Ganesh Gopalakrishnan

Proceedings of the Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30, 2006

2005

Symbolic Partial Order Reduction for Rule Based Transition Systems.

[BibT_eX]

[DOI]

Ritwik Bhattacharya

Ganesh Gopalakrishnan

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Functional verification of the z990 superscalar, multibook microprocessor complex.

[BibT_eX]

[DOI]

Dean G. Bair

William D. Wollyung

Edward J. Kaminski Jr.

IBM J. Res. Dev., 2004

2003

Formal Design of Cache Memory Protocols in IBM.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2003

2001

Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic.

[BibT_eX]

[DOI]

Randal E. Bryant

Miroslav N. Velev

ACM Trans. Comput. Log., 2001

2000

Executable Protocol Specification in ESL.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

Introduction to the Special Issue on Verification of Arithmetic Hardware.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Verifying the SRT Division Algorithm Using Theorem Proving Techniques.

[BibT_eX]

[DOI]

Xudong Zhao

Formal Methods Syst. Des., 1999

Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.

[BibT_eX]

[DOI]

Randal E. Bryant

Miroslav N. Velev

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999

Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions.

[BibT_eX]

[DOI]

Randal E. Bryant

Miroslav N. Velev

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1996

Research Goals for Formal Methods.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

1992

Semantics and Reasoning with Free Procedures.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1992

Reasoning about Systems with Many Processes.

[BibT_eX]

[DOI]

A. Prasad Sistla

J. ACM, 1992

Programming in a General Model of Synchronization.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '92, 1992

1989

Reasoning about Procedures as Parameters in the Language L4

[BibT_eX]

[DOI]

Inf. Comput., December, 1989

1987

Reasoning with Many Processes

[BibT_eX]

A. Prasad Sistla

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986

True Relative Completeness of an Axiom System for the Language L4 (Abridged)

[BibT_eX]

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

1985

Zeus: A Language for Expressing Algorithms in Hardware.

[BibT_eX]

[DOI]

Karl J. Lieberherr

Computer, 1985

1984

Monitoring for Deadlock and Blocking in Ada Tasking.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1984

1983

Effective Axiomatizations of Hoare Logics

[BibT_eX]

[DOI]

J. ACM, July, 1983

Reasoning About Procedures as Parameters.

[BibT_eX]

[DOI]

Proceedings of the Logics of Programs, 1983

1982

Monitoring for deadlocks in Ada tasking.

[BibT_eX]

[DOI]

David P. Helmbold

David C. Luckham

Proceedings of the AdaTEC Conference on Ada, 1982

1978

Automating Proofs of the Absence of Common Runtime Errors.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, 1978

1975

A Synthesizer of Inductive Assertions.

[BibT_eX]

[DOI]