A New Object Logic and an SMT-LIB Backend for ESC/Java3

Supervisor:       Dr. Joseph Kiniry
Subject Area: 	  Software Engineering
Pre-requisite: 	  Good knowledge of Java and Logic
Co-requisite: 	  Knowledge of predicate calculus, wp calculus, and
                  program verification will be obtained during the
                  course of this project
Subject Coverage: Formal Specifications, Extended Static Checking,
                  Verification, Logic, Algebraic Frameworks, First-order
                  Theorem Provers
Project Type: 	  Design & Implementation
Hardware: 	  PC or workstation (almost any operating system)

Description:
ESC/Java, and existing versions of ESC/Java2, use an unsorted object
logic that describes "interesting" aspect of Java's semantics. This
logic is expressed in the syntax of a popular-but-antique first-order
theorem prover called "Simplify". While Simplify represented a radical
advance in the field of automated first-order provers when it was
written, it is no longer seriously supported, nor does it see any new
features, and is considered in many respect obsolete.

Many new automated first-order provers are under development
today. Nearly all of the researchers related to these provers are
represented in the SMT-LIB initiative. SMT-LIB stands for
"Satisfiability Modulo Theories Library". Essentially, everyone doing
first-order provers for verification wants a common syntax and
semantics for their provers.  Perhaps when we have such a syntax, all
tools that use these provers can choose to use the best prover for
their particular problem, since they all support the same language.
Moreover, then there is a reasonable way to compare different provers'
correctness, completeness, capabilities, performance, etc.

A new many-sorted object logic for ESC/Java2 has recently been written
in the SMT-LIB language. Thus, we have already taken the first
theoretical steps for supporting a new (more capable, comprehensible,
and complete) logic.

This project is to add this logic to ESC/Java3 and work out the kinks
in the logic. This work entails modifying the verification condition
generator so that it "understands" SMT-LIB and refactoring some of the
internal reasoning of ESC/Java2 so that is is more generic (thus, it
no longer depends upon the quirks of Simplify).

Mandatory

1) Gain familiarity with JML, ESC/Java2, and Maude.
2) Input the new logic into the Maude algebraic framework.
3) Sort-check the logic and generate an unsorted version to compare to
the original unsorted logic.
4) Design and implement modifications to ESC/Java3 to support SMT-LIB.
5) Implement an SMT-LIB benchmarks generator in ESC/Java3.
6) Test new ESC/Java3 against old example code bases that have
verification results.
7) Release to the world a new version of ESC/Java3. Fame and fortune
follows.

Discretionary

Other collaborators are also encoding this logic in higher-order
logical frameworks, including Coq and PVS. If the student has an
interest in theorem proving, he or she can become involved in this
work as well.  Writing, submiting, and publishing a paper on the
results is also a possibility.

Exceptional

Proving the soundness and measuring the completeness of the logic in
some fashion means you earn an M.S. :)

Sources of information and preparatory reading

0) The SMT-LIB web site https://goedel.cs.uiowa.edu/smtlib/
1) The JML web site https://www.jmlspecs.org/
2) The ESC/Java2 web site /products/opensource/ESCJava2/
3) Read the two recent papers available via the JML web page: "An
overview of JML tools and applications" and "JML: notations and tools
supporting detailed design in Java".
4) Read "ESC/Java2: Uniting ESC/Java and JML: Progress and issues in
building and using ESC/Java2" available via Google Scholar.
5) Download, install, and play around with the JML tool suite and
ESC/Java2 to get a feel for the technology.
6) Download, install, and play around with Maude. https://maude.cs.uiuc.edu/