THOR: A tool for reasoning about shape and arithmetic - Tool paper
Journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Journal Volume
5123 LNCS
Pages
428-432
Date Issued
2008
Author(s)
Abstract
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. © 2008 Springer-Verlag.
Type
book