Posts for the month of May 2011

Slides for Summer School on Formal Techniques

I just uploaded the slides for the JPF talks and lab given at the First Summer School on Formal Techniques (05/22-05/27/2011 Menlo College, Atherton CA) to the presentations page. You can find PowerPoint, Keynote and PDF versions in the attachments section of this page. Especially the lab is a good basis for a first hands-on course of about 2h.

JPF Workshop 2011

We have a JPF Workshop 2011 co-located with ASE 2011 in Oread, Lawrence, Kansas on Nov 12.

Call for Contributions:

We welcome contributions on all topics related to JPF or one of its extensions. In addition to research papers, we also solicit comparative analysis papers that evaluate algorithms in JPF or its extensions with relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF. We solicit two kinds of papers:

  1. Full Papers: The full papers should be at most 12 pages long in the IEEE trans format. The paper should describe a fully matured research topic that has been implemented within JPF core or one of its extensions. The papers can be previously published at other peer-reviewed venues or be original research papers not been published before. In previously published work we highly encourage addition of new material that provides new insights about either the implementation, engineering, or evaluation with respect to JPF.
  1. Short Papers: The short papers should be at most 5 pages long in the IEEE trans format. Short papers can describe an extension of JPF as a tool paper. Work in progress descriptions can also be submitted as short papers.

The best papers in the workshop will be invited to be included in a special STTT issue on Java Pathfinder.

Important Dates and Deadlines:

  • Paper Submission Deadline: August 29, 2011
  • Notification of acceptance/rejection: September 30, 2011
  • Deadline for Final Version: October 15, 2011

different Instruction class hierachies

jpf-core r474 aims at making gov.nasa.jpf.jvm agnostic to specific Instruction class hierarchies. This mostly works by relaxing the gov.nasa.jpf.jvm.InstructionFactory interface to return abstract Instruction types, and should be transparent to most InstructionFactory implementors.

However, if you use your own TABLESWITCH, LOOKUPSWITCH or xRETURN classes that are not derived from their jpf-core counterparts, you have to make them implement the corresponding

  • TableSwitchInstruction
  • LookupSwitchInstruction
  • ReturnInstruction

interfaces from gov.nasa.jpf.jvm. This should not require any new methods, just add the respective implements spec to your instruction class.