Write a Blog >>
Mon 10 Oct 2022 14:15 - 14:30 at Room 129 - Session 3

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 Oct

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:00
13:30
45m
Talk
Invited talk: "Virtual threads: scalable, harmonious concurrency"
[Workshop] JPF '22
14:15
15m
Talk
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
15m
Talk
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
15m
Talk
Gradle support for Symbolic PathFinder
[Workshop] JPF '22
Gaurang Kudale University of Pune