Automatically refining partial specifications for Program Verification

Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He

Research output: Chapter in Book/Report/Conference proceedingConference contribution

142 Downloads (Pure)


Automatically verifying heap-manipulating programs is a challenging task, especially when dealing with complex data structures with strong invariants, such as sorted lists and AVL/red–black trees. The verification process can greatly benefit from human assistance through specification annotations, but this process requires intellectual effort from users and is error-prone. In this paper, we propose a new approach to program verification that allows users to provide only partial specification to methods. Our approach will then refine the given annotation into a more complete specification by discovering missing constraints. The discovered constraints may involve both numerical and multi-set properties that could be later confirmed or revised by users. We further augment our approach by requiring partial specification to be given only for primary methods. Specifications for loops and auxiliary methods can then be systematically discovered by our augmented mechanism, with the help of information propagated from the primary methods. Our work is aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties for pointer-based data structures. Initial experiments have confirmed that we can automatically refine partial specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer properties.
Original languageEnglish
Title of host publicationFM 2011: Formal Methods
Subtitle of host publicationLecture notes in computer science, 6664
EditorsMichael Butler, Wolfram Schulte
Place of PublicationBerlin
PublisherSpringer Berlin
Publication statusPublished - 2011
Event17th International Symposium on Formal Methods - Limerick, Ireland
Duration: 20 Jun 201124 Jun 2011
Conference number: 17

Publication series

Name Lecture Notes in Computer Science
PublisherSpringer Berlin


Conference17th International Symposium on Formal Methods
Abbreviated titleFM 2011

Bibliographical note

Author can archive post-print (ie final draft post-refereeing)


Dive into the research topics of 'Automatically refining partial specifications for Program Verification'. Together they form a unique fingerprint.

Cite this