Intra-module Inference

Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti, Jan W. Voung, Thomas Wies

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

Abstract

Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program modules because they require programmers to provide detailed contracts, including an interface specification, module invariants, and internal specifications. We argue that given a suitably rich assertion language, modest effort suffices to document the interface specification and the module invariants. However, the burden of providing internal specifications is still significant and remains a deterrent to the use of contract-based checkers. Therefore, we consider the problem of intra-module inference, which aims to infer annotations for internal procedures and loops, given the interface specification and the module invariants. We provide simple and scalable techniques to search for a broad class of desired internal annotations, comprising quantifiers and Boolean connectives, guided by the module specification. We have validated our ideas by building a prototype verifier and using it to verify several properties on Windows device drivers with zero false alarms and small annotation overhead. These drivers are complex; they contain thousands of lines and use dynamic data structures such as linked lists and arrays. Our technique significantly improves the soundness, precision, and coverage of verification of these programs compared to earlier techniques.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Pages493-508
Number of pages16
Volume5643 LNCS
DOIs
StatePublished - 2009
Event21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France
Duration: Jun 26 2009Jul 2 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5643 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other21st International Conference on Computer Aided Verification, CAV 2009
CountryFrance
CityGrenoble
Period6/26/097/2/09

Fingerprint

Specification
Specifications
Module
Internal
Annotation
Invariant
Driver
Dynamic Data Structures
False Alarm
Quantifiers
Soundness
Assertion
Data structures
Coverage
Reasoning
Prototype
Verify
Line
Zero

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Lahiri, S. K., Qadeer, S., Galeotti, J. P., Voung, J. W., & Wies, T. (2009). Intra-module Inference. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings (Vol. 5643 LNCS, pp. 493-508). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS). https://doi.org/10.1007/978-3-642-02658-4_37

Intra-module Inference. / Lahiri, Shuvendu K.; Qadeer, Shaz; Galeotti, Juan P.; Voung, Jan W.; Wies, Thomas.

Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Vol. 5643 LNCS 2009. p. 493-508 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS).

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

Lahiri, SK, Qadeer, S, Galeotti, JP, Voung, JW & Wies, T 2009, Intra-module Inference. in Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. vol. 5643 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5643 LNCS, pp. 493-508, 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France, 6/26/09. https://doi.org/10.1007/978-3-642-02658-4_37
Lahiri SK, Qadeer S, Galeotti JP, Voung JW, Wies T. Intra-module Inference. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Vol. 5643 LNCS. 2009. p. 493-508. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02658-4_37
Lahiri, Shuvendu K. ; Qadeer, Shaz ; Galeotti, Juan P. ; Voung, Jan W. ; Wies, Thomas. / Intra-module Inference. Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Vol. 5643 LNCS 2009. pp. 493-508 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{b5e54b4ee1764dfa87e2a76ca9c45bd8,
title = "Intra-module Inference",
abstract = "Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program modules because they require programmers to provide detailed contracts, including an interface specification, module invariants, and internal specifications. We argue that given a suitably rich assertion language, modest effort suffices to document the interface specification and the module invariants. However, the burden of providing internal specifications is still significant and remains a deterrent to the use of contract-based checkers. Therefore, we consider the problem of intra-module inference, which aims to infer annotations for internal procedures and loops, given the interface specification and the module invariants. We provide simple and scalable techniques to search for a broad class of desired internal annotations, comprising quantifiers and Boolean connectives, guided by the module specification. We have validated our ideas by building a prototype verifier and using it to verify several properties on Windows device drivers with zero false alarms and small annotation overhead. These drivers are complex; they contain thousands of lines and use dynamic data structures such as linked lists and arrays. Our technique significantly improves the soundness, precision, and coverage of verification of these programs compared to earlier techniques.",
author = "Lahiri, {Shuvendu K.} and Shaz Qadeer and Galeotti, {Juan P.} and Voung, {Jan W.} and Thomas Wies",
year = "2009",
doi = "10.1007/978-3-642-02658-4_37",
language = "English (US)",
isbn = "3642026575",
volume = "5643 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "493--508",
booktitle = "Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings",

}

TY - GEN

T1 - Intra-module Inference

AU - Lahiri, Shuvendu K.

AU - Qadeer, Shaz

AU - Galeotti, Juan P.

AU - Voung, Jan W.

AU - Wies, Thomas

PY - 2009

Y1 - 2009

N2 - Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program modules because they require programmers to provide detailed contracts, including an interface specification, module invariants, and internal specifications. We argue that given a suitably rich assertion language, modest effort suffices to document the interface specification and the module invariants. However, the burden of providing internal specifications is still significant and remains a deterrent to the use of contract-based checkers. Therefore, we consider the problem of intra-module inference, which aims to infer annotations for internal procedures and loops, given the interface specification and the module invariants. We provide simple and scalable techniques to search for a broad class of desired internal annotations, comprising quantifiers and Boolean connectives, guided by the module specification. We have validated our ideas by building a prototype verifier and using it to verify several properties on Windows device drivers with zero false alarms and small annotation overhead. These drivers are complex; they contain thousands of lines and use dynamic data structures such as linked lists and arrays. Our technique significantly improves the soundness, precision, and coverage of verification of these programs compared to earlier techniques.

AB - Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program modules because they require programmers to provide detailed contracts, including an interface specification, module invariants, and internal specifications. We argue that given a suitably rich assertion language, modest effort suffices to document the interface specification and the module invariants. However, the burden of providing internal specifications is still significant and remains a deterrent to the use of contract-based checkers. Therefore, we consider the problem of intra-module inference, which aims to infer annotations for internal procedures and loops, given the interface specification and the module invariants. We provide simple and scalable techniques to search for a broad class of desired internal annotations, comprising quantifiers and Boolean connectives, guided by the module specification. We have validated our ideas by building a prototype verifier and using it to verify several properties on Windows device drivers with zero false alarms and small annotation overhead. These drivers are complex; they contain thousands of lines and use dynamic data structures such as linked lists and arrays. Our technique significantly improves the soundness, precision, and coverage of verification of these programs compared to earlier techniques.

UR - http://www.scopus.com/inward/record.url?scp=70350220887&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350220887&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02658-4_37

DO - 10.1007/978-3-642-02658-4_37

M3 - Conference contribution

SN - 3642026575

SN - 9783642026577

VL - 5643 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 493

EP - 508

BT - Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings

ER -