本教程参考自 Verification glasses 链接
1、Install Java 8
2、安装ant和mercurial
sudo apt install ant
sudo apt install mercurial
3、下载 junit.jar和hamcrest.jar (假设它们被下载到 “junit-dir”这个 directory 里面)
4、执行以下步骤
cd ~/Documents
mkdir junit
mv junit-dir/junit*.jar ~/Documents/junit
mv junit-dir/hamcrest*.jar ~/Documents/junit
mkdir jpf
cd jpf
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc
5、 创建一个新的文件~/.jpf/site.properties
cd
mkdir .jpf
cd .jpf
printf " " > site.properties
gedit site.properties
在打开的文件中粘贴（并编辑）以下文本
jpf-core = ${user.home}/Documents/jpf/jpf-core
jpf-symbc = ${user.home}/Documents/jpf/jpf-symbc
extensions=${jpf-core},${jpf-symbc}
6、build and test jpf-core
cd ~/Documents/jpf/jpf-core
ant test
遇到 error:
not found ${env.JUNIT_HOME}，那就编辑build.xml这个文件，把里面的${env.JUNIT_HOME}替换为${user.home}/Documents/junit
7、build and test jpf-symbc
cd ~/Documents/jpf/jpf-symbc
ant test
遇到 error:
not found ${env.JUNIT_HOME}，那就编辑build.xml这个文件，把里面的${env.JUNIT_HOME}替换为${user.home}/Documents/junit，并且把上面的3行对unless="env.JUNIT_HOME"的检查注释掉
至此，JPF基本就安装好了。下面运行示例程序。
8、示例程序
cd ~/Documents/jpf/jpf-symbc/src/examples
~/Documents/jpf/jpf-core/bin/jpf TestPaths.jpf
正常运行，但是输出的结果里面并没有对各个路径进行探索，内容如下
====================================================== Method Summaries
Inputs: x,b
No path conditions for TestPaths.testMe2(0,false)
debug了一段时间，在 Google Groups 找到了一个解决方法，那就是把 ~/Documents/jpf/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java这个文件替换为 这个 文件
再次运行，成功，以下为结果
====================================================== Method Summaries
Inputs: x,b
TestPaths.testMe2(1200,true) --> Return Value: --
TestPaths.testMe2(-2147483648,true) --> Return Value: --
TestPaths.testMe2(1201,true) --> Return Value: --
TestPaths.testMe2(0(don't care),false) --> Return Value: --
