Seminars

View all Seminars  |  Download ICal for this event

Proving and Programming with PVS

Series: CSA Distinguished Lecture

Speaker: Natarajan Shankar

Date/Time: Feb 14 11:30:00

Location: CSA Seminar Hall (Room No. 254, First Floor)

Abstract:
SRI's Prototype Verification System is an interactive proof assistant
that has been in active development and use for over thirty years. PVS features
a specification language based on a richly typed higher-order logic with
algebraic datatypes, dependent predicate subtypes, and parametric theories. The
interactive theorem prover employs a range of automated proof strategies for
simplification, rewriting, and case analysis, along with built-in decision
procedures for SAT and SMT solving. The applicative fragment of PVS can be
viewed as a functional programming language, and executable code can be
generated in Common Lisp and C, among other languages. PVS includes extensive
libraries spanning a range of topics in mathematics and computing. Since the
formalizations include a significant amount of computational content in the form
of executable programs, it is useful to generate code from the programs that
executes efficiently. The generated code can be integrated as verified
components within larger systems or employed as reference implementations. The
talk is an informal overview of the underlying theoretical foundations, and the
proof and code generation capabilities of PVS.

Speaker Bio:
Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI Fellow at the SRI Computer Science Laboratory. He received a B.Tech degree in Electrical Engineering from the Indian Institute of Technology, Madras, and a Ph.D. in Computer Science from the University of Texas at Austin. He is a co-recipient of the 2012 CAV Award and the recipient of the 2022 Herbrand Award.

Host Faculty: Deepak DSouza