JPF-static: Practical Verification Using Static Analysis and Java Pathfinder

The goal of this project is to design practical verification techniques for multi-threaded programs based on specific combinations of static and dynamic analyses. We implement all proposed techniques using WALA and Java Pathfinder, and evaluate them on Java bytecode programs.

Contact person: Pavel Parízek

Related Publications


 Date  Supported Features  Links
2015-12-15field access analysis, may-happen-before analysis, shared array elements analysis,
dynamic POR, heuristics based on hybrid analyses (transition reordering and pruning)
2014-08-26field access analysis, may-happen-before analysis, dynamic PORsources
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2016-02-11