The ME-EM Graduate Seminar speaker on Thursday, November 20th at 4:00 in 103 EERC will be Amer Tahat, PhD Student, Computational Sciences and Engineering, Department of Computer Science, Michigan Tech University,
The title of his presentation will be ‘Prototype Verification System PVS: Cutting Edges Human-Machine Interactive Verification, Modeling and Analysis Software’.
PVS is an interactive prototype verification system developed by SRI (Stanford Research Institute) with collaboration of NASA. PVS has been widely used by NASA to verify the correctness of their designs under extreme safety measures e.g Next Generation Air Traffic System (NextGen) and Scalable Processor-Independent Design for Extended Reliability (SPIDER). It has very powerful and ultra-reliable specification and semi-automatic verification language which can capture wide range of real world applications like complicated critical and autonomous control systems in: Aerodynamics, Robotics, Security and Communication Protocols. It also has been used for the design and the verifications of hardware and software of parametric critical systems, mathematical theories, and it was used even in modeling and analyzing meta-physical arguments! In this seminar we would like to introduce the revolutionary features of interactive analysis and verification system PVS. We will provide some examples of its applications in solving real life problems. Dr. Ossama Abdelkhalik (ME-EM department) and Amer Tahat PhD student (CSE) are planning to conduct a tutorial about this tool here at MTU with a generous collaboration of NASA Langley.
PVS received CAV award in 2012 ( 2012 CAV (Computer-Aided Verification) Award). PVS is an open source since 1994 and is known for its user friendliness. It has been used in industry as well as in academic research. For more information about related research fields please visit NASA formal methods group (http://shemesh.larc.nasa.gov/fm/fm-pvs.html), and PVS SRI website (http://pvs.csl.sri.com/index.shtml).
Amer Tahat is a Computational Sciences and Engineering PhD student, computer science department, at Michigan Tech University. I joined my PhD program in Sept 2012. In Oct 2012 I attended NASA Langley and National Institute of Aeronautics PVS (Prototype Verification System) class, in Hampton Virginia. Between Oct 2012 and March 2013 I was involved in a short project using PVS with the collaboration of NASA Langley. Since then I have been a member of Software Design Laboratory at Michigan Tech university and have been part of two projects under supervision of Dr. Ali Ebnenasir funded by National Science Foundation in which I study the applications of mechanical verifications using theorem prover PVS. Between 2012 and 2014, I attended and participated in several international conferences in formal and automatic verification techniques. In particular NASA Formal Methods Symposiums of Automatic Reasoning (NFM) NFM13, Moffett Field, Silicon Valley, CA and NFM14 in Johns Space Center, Huston, TX. Also in Sept 2014 I participated by a paper in LOPSTR 14 (24th International Conference of logic-Based Program Synthesis and Transformation) in UK.
In last summer 19-26 May 2014 I attended the Stanford Research International (SRI) forth summer school in formal techniques, Menlo College, Stanford, CA, in which assisted in organizing the student presentation secession. In the school I presented a PVS based analysis of a 1000 year metaphysical controversy http://fm.csl.sri.com/SSFT14/. I received an NSF generous award to attend this school.
Lately the work has been submitted to FSEN International Conference in Foundations of Software Engineering FSEN 15. Currently I am exploring more applications of PVS with the collaboration of Dr. Ossama Abedlkhalik ME-EM department on some other fields in Orbital Mechanics.