End-of-Year Update on ESC/Java2

One of the tools that we work hard on here at UCD is ESC/Java2. This post is to provide an end-of-year update on this popular tool. First, I plan on working on the first version of the ESC/Java2 User's Guide during the holiday break. Mikolas Janota and Radu Grigore, two of my PhD students, are continuing to work on their new specification-aware dead-code/assertion identification subsystem. We'll be writing a paper about this next quarter. Many people outside of UCD contribute to ESC/Java2 as well. We are excited to see collaborators Patrice Chalin and Perry James's work on the IDC subsystem continue to come in. We look forward to trying it out! My PhD student Alan Morkan is very unfortunately leaving us for greener pastures, as he has decided that doing a PhD is not in the cards right now. He and I are in the middle of writing a paper on the specification consistency checker, and I am trying to inspire him to help finish up the first version of the soundness and completeness warning system, which has been on hold while he has figured out his future. If anyone else would like to help finish up that subsystem, please drop me a line. I hope to have PhD student Michal Moskal visiting next semester for some time to work on ESC/Java2's prover backend and his theorem prover. We are very much looking forward to having him around for a few months. I have also been working with Clark Barrett CVC3 (the upcoming new version of CVC Lite) again lately, helping ensure it builds and runs well on OS X. Consequently, we hope to see the CVC3 and SMT-LIB backends move forward again next quarter. We are expecting some commits from MSc graduate Ke Sun in Eindhoven (supervised by Kuiper and Huizing and advised by Erik Poll). He has improved the PVS backend considerably and has some patches to the logic and the code as a result. His work is detailed in his thesis entitled "Verifying Java Programs by Integrating ESC/Java2 and PVS." Finally, I would like to put out a new beta release for the New Year, right after I have a first draft of the User's Guide. Coincident with this release will be a public announcement of the new version of the ESC/Java2 plugin that Aleksy Schubert has helped out with. I want to express my gratitude to all ESC/Java2 contributors and collaborators. Without you all this effort simply would not succeed. Happy holidays all. --Joe

powered by performancing firefox