A PVS Eclipse Plug-in
Note: Some initial work on this project was done as a 2005-2006 Final Year Project by Robert Finlay (report).
- Supervisor Dr. Joseph Kiniry
- Subject Area Software Engineering
- Pre-requisite Strong knowledge of Java and basic software engineering principles
- Co-requisite (things you must learn along the way) Eclipse use and plug-in development
- Subject Coverage Integrated Development Environments, Higher-order Theorem Provers
- Project Type Design and Implementation
- Hardware/Software: Any machine running x86/Linux or Mac OS X
Description
PVS is a higher-order theorem prover that uses Emacs as a front-end, much like nearly all other higher-order theorem provers.
Many other provers like Isabelle, HOL, and Coq used the same Emacs-based front-end, called Proof General. Proof General is somewhat inappropriate for PVS, as the former's interactive style is semi-incompatible with the latter.
PVS's front-end, on the other hand, is highly tuned for the kinds of specifications and proofs accomplished in PVS. Additionally, that interface has been significantly enriched by other projects mentioned on this web site.
A new Eclipse-based Proof General is now in development. The purpose of this project is to evaluate this new interface and the general possibility of using an Eclipse plugin framework for the development of a new PVS front-end.
Mandatory
- Show expertise with the Eclipse Platform, particularly the plug-ins architecture.
- Specify a JML-annotated Java interface for the I/O interface and proof interface of PVS.
- Design, implement, and test a PVS plugin for the Eclipse Platform supporting PVS specification authoring and proof interaction.
- Release the plugin to the world under an appropriate FLOSS license.
Discretionary
- Support plug-in indefinitely and help kickstart a community focused on the evolution and maintenance of the plug-in.
- Coauthor, submit, and publish a paper on this work.