jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code
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.
Mon 10 OctDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 15:00 | |||
13:30 45mTalk | Invited talk: "Virtual threads: scalable, harmonious concurrency" [Workshop] JPF '22 | ||
14:15 15mTalk | jpf-logic: a Framework for Checking Temporal Logic Properties of Java Code [Workshop] JPF '22 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 | ||
14:30 15mTalk | Towards Wider Support for Java String Functions [Workshop] JPF '22 Qiuchen Yan University of Minnesota, Cyrille Artho KTH Royal Institute of Technology, Sweden, Pavel Parizek Charles University | ||
14:45 15mTalk | Gradle support for Symbolic PathFinder [Workshop] JPF '22 Gaurang Kudale University of Pune |