 |
 |
 |
 |
 |
ThorThis page holds the latest version of the Thor program verification tool. Thor stands for Tool for Heap-Oriented Reasoning, as the tool's goal is to prove properties of programs that manipulate heap-based data structures. The tool currently supports proving memory safety of programs that manipulate doubly-linked lists and also supports arithmetic reasoning via the approach described in our SAS 2007 paper. In this case "arithmetic reasoning" refers to the ability to prove properties involving arithmetic inequalities over integer program variables, integers stored in the heap, and list lengths. The tool outputs "arithmetic abstractions," which are purely stack-based programs with the property that unreachability of the error state in the arithmetic program implies memory safety of the original program. Such programs provide an interesting source of examples for tools targeting arithmetic reasoning. Thor is under active development and new features will be periodically added. The main goal of the tool is to support the proving of strong invariants. As such, scalability is not currently a focus. For an example of some very promising work on scalability of a similar shape analysis, see the work of Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano, and Peter O'Hearn available from Hongseok's web page and some of the other work listed on O'Hearn's local reasoning page. An example of Thor's output is given here. This shows the result of running Thor on a program that partitions a list. Clicking on the blue invariants will replace them with graphical depictions of the pointer state at that program location. An alternate version of the output is given here. This version presents the execution tree that was built by Thor and gives more insight into how the state space was explored during the proving process. Thor is provided solely for non-commercial, academic use. Any other use requires the authors' express permission. Requirements: The Thor programming team: |
||
 |
 |
 |