Title: A Tutorial on Theorem Proving in the Prototype Verification System (PVS)
Abstract: This tutorial will be offered for faculty members and graduate students whose research involves any sort of logical reasoning that can be expressed in predicate logic. The Prototype Verification System (PVS) is one of the premier theorem provers developed at the Stanford Research Institute (SRI). This tutorial provides a basic understanding of PBS along with the elementary techniques for formal specification and mechanical verification. PVS has been used in the verification of numerous real-world applications such as mission-critical systems, air traffic management systems, fault-tolerant distributed systems, security protocols, spacecraft autonomy and AI planning.
Organizers: Mr. Amer Tahat (CS), Dr. Ali Ebnenasir (CS), and Dr. Ossama Abdelkhalik (ME-EM).
Time: 4:00 – 5:00 p.m., Dec. 3rd, 4th and 5th
Place: Rekhi 112
Registration: Please send an email to Mr. Amer Tahat at atahat@mtu.edu. Space is limited, so register early please.
Acknowledgement: The organizers extend their gratitude to the Formal Methods group at NASA Langley for providing technical support. Prerequisites include preliminary knowledge of propositional and predicate logic.