Facilitating verification in program loops by identification of static iteration patterns

Aditya Desai, Era Jain, Subhajit Roy

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

1 Scopus citations

Abstract

Generating invariants for loops is often a grueling obstacle in formal program verification. Researchers have employed methods from formal techniques based on abstract interpretation to test-driven dynamic analysis to tackle this problem. Even though powerful techniques for generating conjunctive invariants (invariants that employ only conjunction of terms) have been developed, disjunctive invariants have remained a sore thumb for formal techniques. In this paper, we propose a technique to transform certain category of loops, those that have a static iteration pattern, into loops that can be handled by conjunctive invariant generators. The key idea is to identify a static iteration pattern that distributes the disjunction in an invariant in a manner that can be captured by only conjunctive invariants. To broaden the scope of our algorithm, we also propose the idea of parametric verification, while attempting to verify specialized versions of the program where a subset of the input variables is instantiated with certain test-inputs. Note that parametric verification distinguishes it from program testing as testing requires all of its variables to be instantiated with test-inputs. We discuss our ideas on loops drawn from real programs to establish real-world applicability of our algorithms.

Original languageEnglish (US)
Title of host publicationAPSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference
EditorsPornsiri Muenchaisri, Gregg Rothermel
PublisherIEEE Computer Society
Pages83-90
Number of pages8
ISBN (Electronic)9781479921430
ISBN (Print)9780769549224
DOIs
StatePublished - Jan 1 2013
Externally publishedYes
Event20th Asia-Pacific Software Engineering Conference, APSEC 2013 - Bangkok, Thailand
Duration: Dec 2 2013Dec 5 2013

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
Volume1
ISSN (Print)1530-1362

Conference

Conference20th Asia-Pacific Software Engineering Conference, APSEC 2013
CountryThailand
CityBangkok
Period12/2/1312/5/13

Keywords

  • Control-flow refinement
  • Formal verification
  • Invariant generation

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Facilitating verification in program loops by identification of static iteration patterns'. Together they form a unique fingerprint.

  • Cite this

    Desai, A., Jain, E., & Roy, S. (2013). Facilitating verification in program loops by identification of static iteration patterns. In P. Muenchaisri, & G. Rothermel (Eds.), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference (pp. 83-90). [6805393] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC; Vol. 1). IEEE Computer Society. https://doi.org/10.1109/APSEC.2013.22