BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//project/author//NONSGML v1.0//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTEND:20230214T120000Z
UID:ced05f90bcf82077d626d66af1578153-412
DTSTAMP:19700101T120011Z
DESCRIPTION:Proving and Programming with PVS
URL;VALUE=URI:https://www.csa.iisc.ac.in/newweb/event/412/proving-and-programming-with-pvs/
SUMMARY: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.
DTSTART:20230214T120000Z
END:VEVENT
END:VCALENDAR