README

README.txt

SOURCE FILES

package gov.nasa.jpf.symbc, /extensions/symbc/src/gov/nasa/jpf/symbc/

Debug.java
DebugV1.java
JPF_gov_nasa_jpf_symbc_Debug.java
JPF_gov_nasa_jpf_symbc_DebugV1.java
SymbolicListener.java
SymbolicListenerClean.java

package gov.nasa.jpf.symbc.sequences, /extensions/symbc/src/gov/nasa/jpf/symbc/sequences

SeqListenerSkeleton.java
SequenceChoiceGenerator.java
SequenceChoiceGeneratorV1.java
SymbolicSequenceListener.java
SymbolicSequenceListenerV1.java
SymbolicSequenceListenerV2.java
SymbolicSequenceListenerV3.java
SymbolicSequenceListenerV4.java
SymbolicSequenceListenerV4_9.java
SymbolicSequenceListenerV5.java
SymbolicSequenceListenerV6.java
SymbolicSequenceListenerV7.java
SymbolicSequenceListenerV8.java

package gov.nasa.jpf.symbc.abstraction, /extensions/symbc/src/gov/nasa/jpf/symbc/abstraction

OSM.java
SymbolicAbstractionListener.java
SymbolicAbstractionListenerV1.java
SymbolicAbstractionListenerV2.java
SymbolicAbstractionListenerV3.java
SymbolicAbstractionListenerV4.java
SymbolicAbstractionListenerV5.java
SymbolicAbstractionListenerV6.java

EXAMPLES

BST.java
BSTDriverAbstraction.java
BSTDriverSequences.java
BankAccount.java
BankAccountDriverSequences.java
BinTree.java
IncDec.java
IncDecDriverAbstraction.java
IncDecDriverSequences.java
LinkedList.java
MethodSequenceGeneratorTao.java
MySymbolicDriverForBST.java
Stack.java
StackDriverAbstraction.java
StackDriverSequences.java
TaoSymbolicDriverForBST.java
TestBinTree.java

LAUNCH CONFIGURATIONS

BSTDriverAbstraction.launch
BSTDriverSymbolic.launch
BSTDriverSymbolicHeuristic.launch
BankAccountDriverSymbolic.launch
IncDecDriverAbstraction.launch
IncDecDriverConcrete.launch
IncDecDriverStateSpaceDot.launch
IncDecDriverSymbolic.launch
IncDecDriverSymbolicHeuristic.launch
StackDriverAbstraction.launch
StackDriverSymbolic.launch
TaoSymbolicDriverForBST.launch

OTHERS

genHtml (script used to generate this page)

Symbolic Labels

BST-SeqLen2-AddOnly-MethodOSM-SymbolicLabels.jpg
BST-SeqLen2-AddOnly-SequenceOSM-SymbolicLabels.jpg
BST-SeqLen2-MethodOSM-SymbolicLabels.jpg
BST-SeqLen2-SequenceOSM-SymbolicLabels.jpg
BST-SeqLen3-AddOnly-MethodOSM-SymbolicLabels.jpg
IncDec-Field-SeqLen2-MethodOSM-SymbolicLabels.jpg
IncDec-Field-SeqLen2-SequenceOSM-SymbolicLabels.jpg
Stack-SeqLen2-MethodOSM-SymbolicLabels.jpg
Stack-SeqLen3-MethodOSM-SymbolicLabels.jpg

Concrete Labels

BST-SeqLen1-MethodOSM-ConcreteLabels.jpg
BST-SeqLen2-AddOnly-MethodOSM-ConcreteLabels.jpg
BST-SeqLen2-AddOnly-SequenceOSM-ConcreteLabels.jpg
BST-SeqLen2-MethodOSM-ConcreteLabels.jpg
BST-SeqLen2-MethodOSM-ConcreteLabelsNoPC.jpg
BST-SeqLen2-SequenceOSM-ConcreteLabels.jpg
IncDec-SeqLen1-Field-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen1-Observer-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen2-Field-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen2-Field-SequenceOSM-ConcreteLabels.jpg
IncDec-SeqLen2-HeapShape-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen2-HeapShape-SequenceOSM-ConcreteLabels.jpg
IncDec-SeqLen2-Observer-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen2-Observer-SequenceOSM-ConcreteLabels.jpg
IncDec-SeqLen3-Field-MethodOSM-ConcreteLabels.jpg
IncDec-SeqLen4-Field-MethodOSM-ConcreteLabels.jpg
Stack-SeqLen1-MethodOSM-ConcreteLabels.jpg
Stack-SeqLen2-SequenceOSM-ConcreteLabels.jpg
Stack-SeqLen3-SequenceOSM-ConcreteLabels.jpg
stack-SeqLen2-MethodOSM-ConcreteLabels.jpg
stack-SeqLen3-MethodOSM-ConcreteLabels.jpg