Sam Owre

Indranil Saha

Proceedings of the FM 2012: Formal Methods, 2012

2011

Solving the First Verified Software Competition Problems Using PVS.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling: Actors, Open Systems, Biological Systems, 2011

2008

A Brief Overview of PVS.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2004

SAL 2.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

The ICS Decision Procedures for Embedded Deduction.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2001

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

Incremental Verification by Abstraction.

[BibT_eX]

[DOI]

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

ICS: Integrated Canonizer and Solver.

[BibT_eX]

[DOI]

Jean-Christophe Filliâtre

Harald Rueß

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Integrating WS1S with PVS.

[BibT_eX]

[DOI]

Harald Rueß

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

1999

Principles and Pragmatics of Subtyping in PVS.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Algebraic Development Techniques, 1999

1998

Subtypes for Specifications: Predicate Subtyping in PVS.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1998

Towards Light-Weight Verification and Heavy-Weight Testing.

[BibT_eX]

[DOI]

Stephan Pfab

Harald Rueß

Friedrich W. von Henke

Proceedings of the International Workshop Tool Support for System Specification, 1998

PVS: An Experience Report.

[BibT_eX]

[DOI]

David W. J. Stringer-Calvert

Proceedings of the Applied Formal Methods, 1998

InVeST: A Tool for the Verification of Invariants.

[BibT_eX]

[DOI]

Saddek Bensalem

Yassine Lakhnech

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

Computing Abstractions of Infinite State Systems Compositionally and Automatically.

[BibT_eX]

[DOI]

Saddek Bensalem

Yassine Lakhnech

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

1997

Integration in PVS: Tables, Types, and Model Checking.

[BibT_eX]

[DOI]

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

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 for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.

[BibT_eX]

[DOI]

Friedrich W. von Henke

IEEE Trans. Software Eng., 1995

1994

A Tutorial on Using PVS for Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Provers in Circuit Design, 1994

1993

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned.

[BibT_eX]

[DOI]

Friedrich W. von Henke

Proceedings of the FME '93: Industrial-Strength Formal Methods, 1993

1992

PVS: A Prototype Verification System.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1987

Muse - A Computer Assisted Verification System.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1987

1985

Programmable heuristics for theorem provers.

[BibT_eX]

[DOI]

William F. Wilson

ACM SIGSOFT Softw. Eng. Notes, 1985

The Sytek theorem prover.

[BibT_eX]

[DOI]