A new talk: Beyond Hoare Logic Assertions: Advanced Specification and Verification with JML and ESC/Java2, presented at Formal Methods for Components and Object (FMCO) 2005 on 4 November, 2005.
ESC/Java 2.0a9 released. This is the tenth (alpha) release of ESC/Java2.
Joe Kiniry gave a talk on Supporting Multiple Theories and Provers in ESC and VC at the Grand Challenge 6 Workshop on Dependable System Evolution at FM 2005 in Newcastle.
Joe Kiniry helped give the popular tutorial "Design by Contract and Automatic Verification for Java with JML and ESC/Java2" at several recent conferences: Formal Methods in Newcastle, England on 19 July and ECOOP in Glasgow, Scotland on 25 July. The previously announced tutorial at ESEC/FSE in Lisbon, Portugal on 6 September has been cancelled, like nearly all the other tutorials at ESEC/FSE due to lack of registrations.
Joe Kiniry gave a talk on the calculi and logics of ESC/Java2 at the Department of Computer and Information Science at Kansas State University and participated in an all-day site visit with the SAnToS Lab folks on the 23rd of June.
Joe Kiniry is on a research sabbatical from the end of April until late July 2005. He is visiting several collaborators during this trip including Cesare Tinelli at the University of Iowa, Gary Leavens at Iowa State, Theo de Raadt at the OpenBSD Hackathon (Slashdot stories I and II) in Calgary, Canada, Patrice Chalin at Concordia University in Montreal, Canada, two conferences in Chicago, PLDI and LICS, John Hatcliff at Kansas State University, and two conferences in the UK: FM in Newcastle and ECOOP in Glasgow.
We have posted a number of internship, final year thesis, and M.S. thesis proposals. If you are interested in a specific proposal, please contact the appropriate lecturer. One of these projects is supported by the School of Computer Science and Informatics, University College Dublin.
We are hiring Ph.D. and Postdoc positions in Integrated Development Environments supporting Logic-based Verification of Sequential and Concurrent Java programs with Proof-Carrying Code!
A new alpha release of OBJ3 2.10 is available. OBJ3 now runs in GNU Common Lisp, CLISP, Steel Bank Common Lisp, and CMU Common Lisp on Linux/x86 and Mac OS X/PPC. See our OBJ3 page for more information.
We gave a tutorial Design by Contract and Automatic Verification for Java with JML and ESC/Java2 at ETAPS 2005.
ESC/Java 2.0a8 released. This is the ninth (alpha) release of ESC/Java2.
A new alpha release of OBJ3 2.10 is soon available! OBJ3 now runs in GNU Common Lisp, CLISP, Steel Bank Common Lisp, and CMU Common Lisp on Linux/x86 and Mac OS X/PPC. See our OBJ3 page for more information.