We describe THOR (Tool for Heap-Oriented Reasoning), a tool based on separation logic that is capable of reasoning automatically about heap-manipulating programs. There are several such systems in development now. However, THOR is unique in that it provides not only shape analysis, but also arithmetic reasoning via a novel combination procedure. Also, considerable effort has been put into making the output clear and easy to understand. THOR uses Javascript and HTML to produce an interactive representation of the analysis results.
展开▼
