[4-21]A Brief Tutorial on the Prototype Verification System (PVS)----中國科學院軟件研究所

[4-21]A Brief Tutorial on the Prototype Verification System (PVS)

文章來源： | 發布時間：2017-04-18 | 【打印】【關閉】

Title: A Brief Tutorial on the Prototype Verification System (PVS)

Speaker: Natarajan Shankar, SRI International Computer Science Laboratory

Time: 10:00am-12:30am (2 hours on lecturing + 0.5 hour on discussion), Apr. 21, Friday, 2017

Venue: Room 334, Building 5, State Key Lab. of Computer Science, Institute of Software

Abstract:

The Prototype Verification System (PVS) is an interactive proof assistant with a wide-spectrum specification language. PVS is used to formalize mathematical knowledge, including the syntax and semantics of other formalisms. The interactive proof assistant blends automation (including SAT/SMT solving, model checking) with interaction.

Short bio of the speaker:

?Dr. Natarajan Shankar is a Principal Scientist at SRI International. He has worked there since 1989 and was made an SRI Fellow in 2009. He has a Ph.D. in Computer Science from the University of Texas at Austin. His research interests include automated reasoning, formal methods, computational logic, programming language theory, and artificial intelligence.

He, along with his SRI colleagues, has developed of a number of logic-based tools, including the PVS interactive proof assistant, the SAL model checker, the Yices SMT solver, the PCE probabilistic inference engine, and the Radler architecture definition language for cyber-physical systems.