LARA

We need to fix representation exposure checking. Two things:

• in short term, we can just fix problem with 'hidden' set and private methods
• in medium term, we implement analysis Karen and Viktor talked about

This is one of the priorities. We need to create a nice colleciton of verified benchmarks and tell to people about it. Currently, the strength of the system is not clearly demonstrated. Especially interesting are benchmarks that can be related to real-world code in some way.

Among the main priorities are:

• Java library
• Jame

Jahob does 3 things currently:

• from Java to ast
• from ast to formulas
• from formulas to the truth (which is out there, in the external theorem provers)

While formDecider successfully separates the last step from the others, the first two are not sufficiently separated, and they should be.

One reason is that we may want to write, for example, front-end for Java or bytecodes in Java and keep the rest of the system in Ocaml.

This is tricky because intermediate language should be simpler, but at the same time, information should not be lost. One question for example, is how to encode generics. We talked about this with Ersoy.

One thing to handle here is BoogiePL front end, because Spec# is already using it and ESC/Java2 is looking into using it.

Given separation of components, we should perhaps take Soot as the Java front end.

Karen said: “Here's a partial list of things I've so far discovered that we could stand to support:

• the Math library (this has come up before) and other libraries
• String's
• double's
• inheritance (not likely, I know, and would require a major change in semantics)”

Ruzica is working on new decision procedures and large-scale reasoning.

Irina Rychkova is connecting SEAM tools to Jahob.

• generalize abstract domain (quantification over more than one variable of arbitrary type)

We should use specification variables as a vehicle to enable user-defined analyses in Jahob, with optional checking of transfer functions.

This is also related to user-defined simulations.

• iprover integration: I tried it succesfully from the web:
  • modified path to caml/mlvalues.h in Makefile
  • added path to eprover (with trailing “/” sign)
  • it worked on generated tptp file
  • ISSUE: it still needs eprover on the path
• Piere Geneve's decision procedure
• poll Sava Krstic on ocaml smt procedure

We want easy to install Linux, Windows and Mac distributions.

Windows issues: getting at least some SMT provers run (get new version of CVC3 to work)

Mac issues: some dynamic library problem on Intel Mac

General questions:

• can we pack prover binaries somehow to avoid all path issues? Search for all of them in jahob/bin as well.
• make path search work on all platforms (do we use “/” right now?)