The tool with the visualization is part of Java PathFinder. All of the source is in the jpf-guided-test repository. You will also need to install jpf-shell. Once jpf-shell is installed, modify its jpf.properties to add the tool to the shell panels:

#Shell Panels
...
shell.panels.guided-vis = edu.byu.cs.guided.search.visualize.TraceVisualizationPanel

You also need to update available panels as

#Available panels is here for when I one day add support to add panels at runtime to shells.
shell.available_panels = properties,config,site,report,test,verify,logging,guided-vis

Once that is complete, you are able to run the JPF files in the src-examples directory of jpf-guided-test. The shell is activated with the configuration line

# Needed when using jpf-shell
shell=edu.byu.cs.guided.search.visualize.TraceVisualizationPanelShell

Screen_Shots

Anything read from or written to in the concrete trace should be in the heap

<!--
   JPF Guided Search Visualization DTD
 
   A document type definition for the visualization XML generated by the JPF guided test
 
   Contributors: Saint Wesonga <developer@swesonga.org>
                 Steven Morley <morleys2@byu.net>
 
   Date: 2010/07/07
 
-->
 
<!ENTITY % Number "CDATA">
    <!-- one or more digits -->
 
<!ELEMENT graph (node|edge|subgraph|jpfstate|jpfedge)*>
<!ELEMENT jpfstate (node|edge|jpfstate)*>
<!ELEMENT subgraph (node|edge)*>
<!ELEMENT jpfedge EMPTY>
<!ELEMENT edge EMPTY>
<!ELEMENT node (variables*)>
<!ELEMENT variables (variable+)>
<!ELEMENT variable EMPTY>
 
<!ATTLIST graph
	id ID #IMPLIED>
 
<!ATTLIST jpfstate
	id ID #IMPLIED>
 
<!ATTLIST subgraph
	id ID #IMPLIED
	label CDATA #IMPLIED>
 
<!ATTLIST variable
	name CDATA #REQUIRED
	type CDATA #IMPLIED
	value CDATA #IMPLIED>
 
<!ATTLIST jpfedge
	srcnode IDREF #REQUIRED
	dstnode IDREF #REQUIRED>
 
<!ATTLIST edge
	srcnode IDREF #REQUIRED
	dstnode IDREF #REQUIRED>
 
<!ATTLIST node
	id ID #REQUIRED
	class CDATA #REQUIRED
	method CDATA #REQUIRED
	sourcecode CDATA #REQUIRED
	sourceline %Number; #REQUIRED
	srcpath CDATA #IMPLIED
	bytepath CDATA #IMPLIED
	bytecode CDATA #REQUIRED
	bytecodeline %Number; #REQUIRED
	executed (true|false) #REQUIRED
	type (conditionalbranch|callsite|synchpoint|startsite|regularstmt) #REQUIRED
	branchvalue (true|false) #IMPLIED
	threadnumber %Number; "-1">