This is the online interface of our verification tool.
Please choose the file containing reachability formulas (the *.rl files) from the file tree in the left panel and then click the Verify button. Verification can take up to 30 seconds/file.
Formulas are verified one by one, in the same order they appear in the .rl file and for each formula the tool displays all the proof branches. Verification completes successfully when all the <k> cells are empty (i.e. contain .K). Path conditions produced during symbolic execution are collected in <path-condition> cell.
Curent folder Examples Cancel