- Projects:
- I am involved in many projects, here are some of general interest.
- Recent Papers, Reports, and Slides:
-
- A Brief Overview of PVS
Invited talk at TPHOLs08, August 2008.
- A Brief Overview of the PVS User
Interface
Invited tutorial at the UITP workshop, August 2008.
- Higher-Order Functions and
Recursive Types in PVS
Presented at the Interactive Theorem Proving class at Stanford: http://verify.stanford.edu/CS359
on April 18, 2005
- Integrating Verification
Components: The Interface is the Message
by: Leonardo de Moura, Sam Owre, John Rushby, Harald Rueß, and
Natarajan Shankar
presented at The
Monterey Workshop Series 2004
- SAL 2
by: Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, N. Shankar, Maria Sorea, and Ashish Tiwari
presented at CAV 2004
- The ICS Decision Procedures for
Embedded Deduction
by: Leonardo de Moura, Sam Owre, Harald Rueß, John Rushby, and N. Shankar
Presented at IJCAR 2004
- Writing PVS Proof Strategies
by: Sam Owre and N. Shankar
Presented at STRATA 2003
- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
by: Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, and Sam Owre
Presented at TPHOLs2001
- ICS: Integrated Canonizer and Solver
by: Jean-Christophe Filliâtre and Sam Owre and Harald Rueß and N. Shankar
Presented at CAV'2001
-
Incremental Verification by Abstraction
by: Yassine Lakhnech and Saddek Bensalem and Sergey Berezin and Sam Owre
Presented at TACAS 2001
-
Theory Interpretations in PVS
by: Sam Owre and N. Shankar
CSL SRI Tech Report
-
Coalgebras in PVS (slides)
by: Sam Owre
Presented at the IFIP
WG1.3 Meeting
-
Integrating WS1S with PVS
by: Sam Owre and Harald Rueß
Presented at CAV 2000
-
An Overview of SAL
by: Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saïdi, N. Shankar, Eli Singerman and Ashish Tiwari
Appears in the Fifth NASA Langley Formal
Methods Workshop (Lfm2000)
-
Principles and Pragmatics
of Subtyping in PVS. Presented at the 14th International Workshop
on Algebraic Development Techniques WADT'99, September, 1999,
Toulouse, France.
-
Towards Light-Weight Verication and Heavy-Weight Testing (gzipped
postscript)
by: Stephan Pfab, Harald Rueß, Sam Owre, and Friedrich W. von Henke
in Tool Support for System Specification, Development, and Verification, R. Bergahmmer and Y. Lakhnech Eds., Springer Advances in Computing Science, May 1999.
-
PVS: An Experience Report
by: Sam Owre, John Rushby, N. Shankar, and David Stringer-Calvert
Appears in Applied Formal
Methods--FM-Trends 98, Dieter Hutter, Werner Stephan, Paolo
Traverso, and Markus Ullman Eds., Springer Verlag Lecture Notes in
Computer Science Vol. 1641, pp. 338--345, Boppard, Germany, October
1998
-
PVS Semantics document (revised March, 1999)
-
Subtypes for Specifications: Predicate Subtypes in PVS
by
John Rushby Sam Owre, and N. Shankar.
To appear in IEEE Transactions on Software Engineering, 1998.
-
Computing Abstractions of Infinite State
Systems Compositionally and Automatically by Saddek Bensalem, Yassine
Lakhnech, and Sam Owre, presented at the Conference for Computer-Aided
Verification (CAV'98), Vancouver, BC, Canada, June/July 1998. Appears in
volume 1427 of Lecture Notes in Computer Science, pages 319-331.
-
InVeSt: A Tool for the Verification of
Invariants by Saddek Bensalem, Yassine Lakhnech, and Sam Owre,
presented at the Conference for Computer-Aided Verification (CAV'98),
Vancouver, BC, Canada, June/July 1998. Appears in volume 1427 of Lecture
Notes in Computer Science, pages 505-510.
-
Integration in PVS: Tables, Types, and
Model Checking by Sam Owre, John Rushby, and Natarajan Shankar,
presented at the Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS '97),
Enschede, The Netherlands, April 1997.
Appears in volume 1217 of Lecture Notes in Computer Science, pages 366-383.
-
Abstract Datatypes in PVS by S. Owre and
N. Shankar. SRI Technical Report CSL-93-9R (Revised June 1997)
-
Integration in PVS: Tables, Types, and
Model Checking by Sam Owre, John Rushby, and Natarajan Shankar,
presented at the Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS '97),
Enschede, The Netherlands, April 1997.
Appears in volume 1217 of Lecture Notes in Computer Science, pages 366-383.
-
PVS: A Prototype Verification System
by Sam Owre, Natarajan Shankar, and John Rushby, from CADE 11, Saratoga
Springs, NY, June 1992.
Sam Owre:
Owre@csl.sri.com