We present jpf-logic. It is an extension of Java PathFinder (JPF), a model checker for Java apps. Our extension jpf-logic provides a framework to check properties expressed in temporal logics such a linear temporal logic (LTL) and computation tree logic (CTL). To support a logic in our framework, one has to implement a parser for the logic, one has to develop a hierarchy of classes that represent the abstract syntax of the logic and implement a transformation from parse trees of formulas to the corresponding abstract syntax trees, and one has to implement a model checking algorithm that takes as input an abstract syntax tree of a formula and a partial transition system. The latter represents a model of the Java app. All three components have been implemented for CTL. The first two have been implemented for LTL.

Matt Walker

York University, Canada

Parssa Khazra

York University, Canada

Anto Nanah Ji

York University, Canada

Hongru Wang

York University, Canada

Franck van Breugel

York University, Toronto

Canada