Paper Info
Title
Automated Specification Discovery via User-Defined Predicates.
Abstract
Automated discovery of specifications for heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures. This task is further complicated by an expressive domain that combines shape, numerical and bag information. In this paper, we propose a compositional analysis framework in the presence of user-defined predicates, which would derive the summary for each method in the expressive abstract domain, independently from its callers. We propose a novel abstraction method with a bi-abduction technique in the combined domain to discover pre-/post-conditions that could not be automatically inferred before. The analysis does not only prove the memory safety properties, but also finds relationships between pure and shape domains towards full functional correctness of programs. A prototype of the framework has been implemented and initial experiments have shown that our approach can discover interesting properties for non-trivial programs.
Year
DOI
Venue
2013
10.1007/978-3-642-41202-8_26
Lecture Notes in Computer Science
Field
DocType
Volume
Data structure,Memory safety,Separation logic,Abstraction,Computer science,Correctness,Theoretical computer science,Aliasing,Symbolic execution,Binary search tree
Conference
8144
Issue
ISSN
Citations 
null
0302-9743
3
PageRank 
References 
Authors
0.39
21
4
Name
Order
Citations
PageRank
Guanhua He1687.50
Shengchao Qin271162.81
Wei-Ngan Chin386863.37
Florin Craciun4408.19