Introduction:
Symbolic GameChecker is a prototype tool developed in Java for checking safety properties of open programs. The tool compiles an open program with infinite integers into a symbolic automaton, which represents the game semantics of the program. The main feature of symbolic automata is that the data is not represented explicitly in it, but symbolically. Along with the tool we have also implemented in Java our own library of classes for working with symbolic automata.
The symbolic automata generated by the tool is checked for safety, i.e. for reachability of a specified move abort.run. We use the breadth-first search algorithm to find the shortest unsafe play (trace) in the model, which contains the unsafe move. Then an external SMT solver Yices is called to determine consistency of its condition. If the condition is found to be consistent (satisfiable), the unsafe play is feasible, i.e. there is an assignment of concrete values to symbols which makes the condition true. This unsafe trace is reported as a genuine counter-example. Otherwise we search for another unsafe trace in the automaton. If no unsafe trace is discovered or all unsafe traces are found to be inconsistent, then the term is deemed safe.
The tool comes in two versions: for single programs, and for annotative family programs implemented with #ifdef preprocessor statements.
Download and Installation:
The tool can be downloaded as an executable jar file from the web page. It needs JDK 1.8 version. Enter the home directory and run the tool.
java -jar symbolicGC-single.jar prog*.ia
or
java -jar symbolicGC-family.jar prog*.ia
The tool also requires the Yices SMT solver to operate correctly. It can be downloaded from: http://yices.csl.sri.com
The tool takes an program "prog*.ia" as input and returns as output "prog*-Output.txt" which contains the resulting symbolic automata for "prog*.ia" and the found (consistent) counter-example if any. Also all shorter inconsistent counter-examples in the automata are reported.
|
