wiki:summer-projects/2010-ltl-1

LTL verification in JPF

Abstract

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.

Contact

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

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

Description

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).

Repository

The sources for this project are available from a Mercurial repository on http://bitbucket.org/francoraimondi/jpf-ltl

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