Aleksandar S. Dimovski

Office: 4D04

Email: adim@itu.dk

Phone: +45 7652 2412

 

 

 

Symbolic GAMECHECKER

 

 

 

 


  Home

  Research

  Publications

  CV





 

Tool:

Version Installation File Examples Documentation
Single programs symbolicGC-single.jar Examples-SGC-Single.zip symbolGC.pdf
Family programs symbolicGC-family.jar Examples-SGC-Family.zip  
Probabilistic analysis symbolicGC-Prob.jar symbolicGC-Prob-Linux.jar Examples-SGC-Prob.zip HowToUse.pdf

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.