no description available

Ron Pressler

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

In this work, we conduct a study about SPF’s existing string support by running tests on a version of SPF with the latest string support. Base on the results, we then analyze each string method and identify the major challenges in supporting them. We categorize string API functions by type of the challenge, propose several solutions to each of the challenges, and discuss the feasibility and disadvantages of different approaches. We implement support in the case of three string methods according to the proposed solution, leaving other methods as future work.

Qiuchen Yan

University of Minnesota

Cyrille Artho

KTH Royal Institute of Technology, Sweden

Pavel Parizek

Charles University

no description available

Gaurang Kudale

University of Pune

India