Java Pathfinder is the annual workshop on technologies related to Java Pathfinder and similar program analyis tools and approaches.
Invited talk: Elena Sherman.Abstract: In evidence-based program analysis research benchmarks play an important role. The more realistic programs contained in a benchmark, the stronger conclusions researchers can make. The researchers who drive the development of benchmarks might include programs relevant to their program analysis research agenda. Then it is unclear whether it is appropriate to reuse those benchmarks for a different program analysis. Thus, the problem that we would like to present in this talk is how to characterize a suitable benchmark for a given analysis. Moreover, what does “a suitable benchmark” even mean?
|10:05||–||10:30|| Dinh Xuan Bach Le, Corina Pasareanu, Rohan Padhye, Willem Visser, Koushik Sen and David Lo.|
SAFFRON: Adaptive Grammar-based Fuzzing for Worst-Case Analysis
|11:00||–||11:25|| Alyas Almaawi, Hayes Converse, Milos Gligoric, Sasa Misailovic and Sarfraz Khurshid.|
Quantifying the Exploration of an Imperative Constraint Solver
|11:25||–||11:50|| Kyle Storey, Eric Mercer and Pavel Parizek.|
A Sound Dynamic Partial Order Reduction Engine for Java Path Finder
|11:50||–||12:10|| Zhenbang Chen, Hengbiao Yu, Ji Wang and Wei Dong.|
Symbolic Verification of Regular Properties for Java Programs (fast abstract)
|12:10||–||12:30|| Egor Namakonov, Eric Mercer, Pavel Parizek and Kyle Storey.|
Symbolic data race detection for Habanero programs (fast abstract)
Keynote: Simon Goldsmith.Abstract: Building a commercial grade static analysis presents a lot of interesting problems. Everything not forbidden is compulsory: language specifications are wonderful documents, but in reality anything the user’s compiler and runtime accepts is fair game. Analysis abstractions that scale “except in pathological cases” don’t scale: analyzing tens of thousands of code bases that routinely exceed millions of lines of code means that those pathological cases inevitably arise. Build a good analysis that runs overnight, and users will ask you to run it in their IDE for near-immediate feedback. A bug finding tool needs a low false positive rate, but a tool aimed at finding security vulnerabilities needs a low false negative rate. Only analyzing “source” code and only starting from main() is insufficient for understanding modern web and mobile applications: frameworks imply a different programming model with a lot of auto-magical program behavior, often including idiosyncratic configuration regimes and various template languages. We’ll talk about these problems and how we tackle them.
|15:00||–||15:25|| Yannic Noller, Hoang Lam Nguyen, Minxing Tang, Timo Kehrer and Lars Grunske.|
Complete Shadow Symbolic Execution with Java PathFinder
|16:00||–||16:25|| Seemanta Saha, William Eiers, Ismet Burak Kadron, Lucas Bang and Tevfik Bultan.|
Incremental Attack Synthesis
|16:25||–||16:50|| Lasse Berglund, Cyrille Artho.|
Method summaries for JPF
|16:50||–||17:10|| Joshua Hooker, Peter Aldous, Eric Mercer, Benjamin Ogles, Kyle Storey and S. Jacob Powell.|
JPF-HJ: A Tool for Task Parallel Program Analysis (fast abstract)
|17:10||–||17:25||Overview of GSoC projects; closing.|
Mon 11 Nov Times are displayed in time zone: Tijuana, Baja California change
Call for Papers (now closed)
Java Pathfinder is the annual workshop on technologies related to Java Pathfinder and similar program analysis tools and approaches.
We solicit regular paper submissions on existing research and applications related to Java Pathfinder (JPF) or its extensions. If the underlying research idea has been published in another venue, the paper needs to clarify the novel aspects that are being presented in the paper. We also solicit extended abstracts and position paper submissions on recent work or work in progress. We welcome comparative analysis papers that evaluate algorithms in JPF or its extensions with other relevant tools. The goal of the workshop is to encourage the flow of ideas relevant to JPF and Java/Android program analysis in general.
Topics of interest include the following:
- JPF extensions or tools
- JPF case studies
- Position papers on JPF, such as future directions
- Java program analysis or verification
- Android program analysis or verification
- General software verification and symbolic execution techniques or tools
Submissions are single-blind: author names will be visible to the reviewers in the PDF. Reviewers will not be disclosed to the authors.
We solicit two types of submissions to be uploaded on EasyChair/JPF2019:
- Regular papers (submissions closed): At most 5-page long papers (incl. references) in the ACM SEN Proceedings format will be reviewed by the organizing committee. Accepted regular papers will be presented at the workshop and published in the ACM SIGSOFT Software Engineering Notes and the ACM Digital Library, as in previous years.
- Extended (“fast”) abstracts: At most 2-page long abstracts will be selected by the organizing committee. Accepted abstracts will be presented at the workshop but NOT published.