LTL verification in JPF


This project is a collaboration with “Construction of linear temporal property verification extension” project, by Dinh-Phuc Nguyen, mentored by Hoang Truong. The aim of this project is to enable the verification of LTL formulae in jpf. To this end, we have implemented the standard DDFS algorithm for the verification of LTL formulae as a new search strategy for infinite traces, and a listener for finite traces. This project also allows the verification of LTL formulae over symbolic executions.


student: Ewgenij Starostin <estar@…> <ES>

mentor: Franco Raimondi <f.raimondi@…> <FR>


Please see these slides for additional details

Program & Timeline

This project is funded by the Google Summer of Code (GSoC) program. It follows the GSoC timeline (start 05/24, finish 08/16).


The sources for this project are available from a Mercurial repository on

Project Blog

(most recent on top)

2010-08-12 (FR) - Content updated

2010-05-30 (FR) - added a few details

2010-05-07 (NR) - project page created

Last modified 8 years ago Last modified on 08/12/2010 03:10:18 PM