![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > A tutorial introduction to the PVS proof assistant
![]() A tutorial introduction to the PVS proof assistantAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact INI IT. BPR - Big proof The Prototype Verification System (PVS) is an interactive proof assistant developed at SRI International. The PVS specification language extends higher-order logic with predicate subtypes, dependent types, inductive datatypes, and parametric theories. These features make typechecking undecidable, or more accurately, decidable modulo proof obligations. The interactive proof assistant includes automated support for contextual simplification, rewriting, and SAT /SMT solving. PVS has been used to formalize large libraries (see, for example, https://github.com/nasa/pvslib). The tutorial gives a brief overview of the language, logic, and proof infrastructure of PVS . This talk is part of the Isaac Newton Institute Seminar Series series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listscms-all@maths.cam.ac.uk Natural History Cabinet, Cambridge University Department of History and Philosophy of Science Talk about Jean Paul Sartre Business Briefing Series, Cambridge Judge Business School Babbage Seminar Series Numerical AnalysisOther talksWhat is the Market Potential of Multilingualism? Constructing datasets for multi-hop reading comprehension across documents Neurological Problems Light Scattering techniques Lunchtime Talk: Helen's Bedroom Architecture and the English economy, 1200-1500: a new history of the parish church over the longue durée |