0
喜欢
0
书签
声明论文
Type-based data structure verification   
摘  要:   We present a refinement type-based approach for the static verifica- tion of complex data structure invariants. Our approach is based on the observation that complex data structures are typically fashioned from two elements: recursion (e.g., lists and trees), and maps (e.g., arrays and hash tables). We introduce two novel type-based mecha- nisms targeted towards these elements: recursive refinements and polymorphic refinements. These mechanisms automate the chal- lenging work of generalizing and instantiating rich universal invari- ants by piggybacking simple refinement predicates on top of types, and carefully dividing the labor of analysis between the type system and an SMT solver (6). Further, the mechanisms permit the use of the abstract interpretation framework of liquid type inference (22) to automatically synthesize complex invariants from simple logi- cal qualifiers, thereby almost completely automating the verifica- tion. We have implemented our approach in DSOLVE, which uses liquid types to verify OCAML programs. We present experiments that show that our type-based approach reduces the manual anno- tation required to verify complex properties like sortedness, bal- ancedness, binary-search-ordering, and acyclicity by more than an order of magnitude. cally reason about data structures severely limits the kinds of prop- erties they can verify. The challenge of automating data structure verification stems from the need to reason about relationships between the unbounded number of values comprising the structure. In SMT and theorem proving based approaches, manual effort is needed to help the prover to generalize relationships over specific values into universal facts that hold over the structure, and dually, to instantiate quanti- fied facts to obtain relationships over particular values. In model checking and abstract interpretation based approaches, manual ef- fort is needed to design, for each data structure, an abstract domain that is capable of generalizing and instantiating relevant relation- ships. Types provide a robust means for reasoning about coarse- grained properties of an unbounded number of values. For exam- ple, if a variable x is of the type int list, then we are guaranteed that every value in the list is an integer. Similarly, if a variable g is of the type (int;int) Map:t, then we are guaranteed that g is a hash-map where every key is an integer that is mapped to another integer. Modern type systems automatically generalize such global properties from local properties of the individual values added to the structure, and dually, automatically instantiate the properties when the structures are accessed.
发  表:   SIGPLAN Conference on Programming Language Design and Implementation  2009

论文统计图
共享有7个版本
 [展开全部版本] 

Bibtex
创新指数 
阅读指数 
重现指数 
论文点评
还没有人点评哦

Feedback
Feedback
Feedback
我想反馈:
排行榜