Object Logic Interpretation and Translator (PVS to SMT-LIB)
Note: Initial work on this project was accomplished as a 2005 International Summer Internship by Clément Hurlin. His work is now part of ESC/Java2 (report).
- Supervisor Dr. Joseph Kiniry
- Subject Area Software Engineering with Applied Theoretical Computer Science
- Pre-requisites Strong mathematical background
- Co-requisites (things you must learn along the way) Knowledge of higher-order and first-order theorem provers, namely PVS and SMT-LIB provers like Sammy
- Other possible co-requisites Learning and programming in Lisp or a language good at doing gross parsing and translation (e.g., Ruby, Python, Perl, etc.)
- Subject Coverage Mathematical Specification Languages, Compilers/Translators, Object Logics
- Project Type Design and Implementation of a Mathematically Sound Translator
- Hardware/Software Machine running anything but Windows
Description
A new object logic for ESC/Java2 has been written in PVS. Because this logic was written in such a way that we intentionally avoided any higher-order constructs, we can translate it into a first-order form. The SMT-LIB language is one such first-order format. It is widely supported by new, powerful first-order provers.
The goal of this project is to specify and write a translator from the PVS object logic to an SMT-LIB object logic. The translation must be well-specified because we wish to reason about the translation (e.g., prove that the translation preserves certain properties of the logic). The translation must be automatic so that, as the PVS logic evolves, the SMT-LIB logic co-evolves.
Mandatory Goals
- Learn PVS.
- Understand the PVS object logic.
- Learn SMT-LIB.
- Understand the design of the SMT-LIB object logic sketch.
- Specify a translation from the PVS logic to an SMT-LIB logic.
- Design, implement, and test a translator from PVS to SMT-LIB.
Discretionary Goals
- Coauthor, submit, and publish a paper on this work.
Exceptional Goals
- Specify and prove some properties about the translation.