Extending string analysis in symbolic JPF


This project revolves around symbolic execution over strings and symbolic execution over the integers that result from the given string constraints.


student: Gideon Redelinghuys <email> <GR>

mentor: Willem Visser <email> <WV>

co-mentor: Corina Pasareanu

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


The implementation, so far, makes use of the dk.brics Automaton package and the JSA extensions to represent each symbolic string and constraint as some automata. Automata operations found in the named two packages are capable of emulating most string operations, except for operations such as substring and equality, which had to be added to the implementation on top of the two automata packages.

The forward solving and backward solving of the string operations: equals, startswith, endswith, trim and substring is currently supported. The extension as is, can determine if all paths in a program (with the above operations) are reachable (forward solving) and what values results in the execution of those paths (backward solving).

Currently, the support for the string operations valueOf, concat and contains are being added (due for 11 June). Other string operations such as charAt and length still need some planning before implementation, due their dependency on integer constraint solving.

A second implementation of the problem is planned in which automata's will be replaced with bit-vectors and a SMT-Solver (for research purposes). Integration between string solving and integer solving needs to be added.

Project Blog

(most recent on top)

2010-06-07 (NR) - project details and progress

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

Last modified 8 years ago Last modified on 06/07/2010 05:52:19 PM