Foreword


This webpage aims to present resources used for our tool presentation. To use those resources, first download Tinker from here. Once extracted, the example files will be available under:

$SOME_PATH/tinker/src/core/demo/TACAS16/

The example runs with Proof Power, to configure it, follow those steps :

Then open the following demo file in the pp to see if the tool can run correctly

$SOME_PATH/tinker/psgraph/src/core/demo/TACAS16/

The line

PPIntf.set_psg_goal

is to ask pp to connect gui for proofs. Note that to enable gui to accept the connection from pp, the following need to be clicked , once the connection is ready the icon will become . Details on how to start the GUI can be found in Tinker's user guide.

Proof recording


Tool demo