research-article

Verification modulo versions: towards usable verification

Authors:

Francesco Logozzo,

Shuvendu K. Lahiri,

Manuel Fähndrich,

Sam BlackshearAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 6

Pages 294 - 304

https://doi.org/10.1145/2666356.2594326

Published: 09 June 2014 Publication History

Abstract

We introduce Verification Modulo Versions (VMV), a new static analysis technique for reducing the number of alarms reported by static verifiers while providing sound semantic guarantees. First, VMV extracts semantic environment conditions from a base program P. Environmental conditions can either be sufficient conditions (implying the safety of P) or necessary conditions (implied by the safety of P). Then, VMV instruments a new version of the program, P', with the inferred conditions. We prove that we can use (i) sufficient conditions to identify abstract regressions of P' w.r.t. P; and (ii) necessary conditions to prove the relative correctness of P' w.r.t. P. We show that the extraction of environmental conditions can be performed at a hierarchy of abstraction levels (history, state, or call conditions) with each subsequent level requiring a less sophisticated matching of the syntactic changes between P' and P. Call conditions are particularly useful because they only require the syntactic matching of entry points and callee names across program versions. We have implemented VMV in a widely used static analysis and verification tool. We report our experience on two large code bases and demonstrate a substantial reduction in alarms while additionally providing relative correctness guarantees.

References

[1]

R. Alur, P. Černý, P. Madhusudan, and W. Nam. Synthesis of interface specifications for java classes. In POPL, 2005.

Digital Library

[2]

G. Ammons, R. Bodík, and J. R. Larus. Mining specifications. In POPL, 2002.

Digital Library

[3]

G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In FM, 2011.

Digital Library

[4]

A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. R. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM, 53(2), 2010.

Digital Library

[5]

S. Blackshear and S. K. Lahiri. Almost-correct specifications: a modular semantic framework for assigning confidence to warnings. In PLDI, 2013.

Digital Library

[6]

M. Bouaziz, F. Logozzo, and M. Fähndrich. Inference of necessary field conditions with abstract interpretation. In APLAS, 2012.

[7]

P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci., 277(1-2), 2002.

Digital Library

[8]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.

Digital Library

[9]

P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Log. Comput., 2(4):511--547, 1992.

[10]

P. Cousot, R. Cousot, M. Fähndrich, and F. Logozzo. Automatic inference of necessary preconditions. In VMCAI, 2013.

Digital Library

[11]

P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In POPL, 2011.

Digital Library

[12]

P. Cousot, R. Cousot, and F. Logozzo. Precondition inference from intermittent assertions and application to contracts on collections. In VMCAI, 2011.

Digital Library

[13]

P. Cousot, R. Cousot, F. Logozzo, and M. Barnett. An abstract interpretation framework for refactoring with application to extract methods with contracts. In OOPSLA, 2012.

Digital Library

[14]

Coverity. Coverity static analysis verification engine. http://www.coverity.com/products/coverity-save.html.

[15]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8), 1975.

Digital Library

[16]

M. Fähndrich, M. Barnett, and F. Logozzo. Embedded contract languages. In ACM SAC, 2010.

Digital Library

[17]

M. Fähndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS, 2010.

[18]

R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361--416, 2000.

Digital Library

[19]

GrammaTech. CodeSonar. http://www.grammatech.com/ codesonar.

[20]

T. A. Henzinger, R. Jhala, and R. Majumdar. Permissive interfaces. In ESEC/FSE-13, 2005.

Digital Library

[21]

D. Hovemeyer and W. Pugh. Finding bugs is easy. SIGPLAN Not., 39(12), 2004.

Digital Library

[22]

S. Joshi, S. K. Lahiri, and A. Lal. Underspecified harnesses and interleaved bugs. In POPL, 2012.

Digital Library

[23]

Klocwork. Klocwork inspect. http://www.klocwork.com/products.

[24]

S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In FSE, 2013.

Digital Library

[25]

S. K. Lahiri, K. Vaswani, and C. A. R. Hoare. Differential static analysis: opportunities, applications, and challenges. In FoSER, 2010.

Digital Library

[26]

V. Laviron and F. Logozzo. Subpolyhedra: A (more) scalable approach to infer linear inequalities. In VMCAI, 2009.

Digital Library

[27]

W. Lee, W. Lee, and K. Yi. Sound non-statistical clustering of static analysis alarms. In VMCAI, 2012.

Digital Library

[28]

F. Logozzo. Automatic inference of class invariants. In VMCAI, 2004.

[29]

F. Logozzo and M. Fähndrich. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In SAC, 2008.

Digital Library

[30]

F. Logozzo and M. Fähndrich. Checking compatibility of bit sizes in floating point comparison operations. In 3rd workshop on Numerical and Symbolic Abstract Domains, ENTCS, 2011.

[31]

Mathworks. Polyspace verifier. http://www.mathworks.com/products/polyspace/.

[32]

Y. Moy. Sufficient preconditions for modular assertion checking. In VMCAI, 2008.

Digital Library

[33]

Y. Wei, C. A. Furia, N. Kazmin, and B. Meyer. Inferring better contracts. In ICSE, 2011.

Digital Library

Cited By

Dunlap TThorn SEnck WReaves B(2023)Finding Fixed Vulnerabilities with Off-the-Shelf Static Analysis2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP57164.2023.00036(489-505)Online publication date: Jul-2023
https://doi.org/10.1109/EuroSP57164.2023.00036
Choi YNam J(2023)WINEInformation and Software Technology10.1016/j.infsof.2022.107109155:COnline publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1016/j.infsof.2022.107109
Jana AKhadsare AChimdyalwar BKumar SGhime VVenkatesh R(2021)Fast Change-Based Alarm Reporting for Evolving Software Systems2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00062(546-556)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00062
Show More Cited By

Index Terms

Verification modulo versions: towards usable verification

Recommendations

Verification modulo versions: towards usable verification
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

We introduce Verification Modulo Versions (VMV), a new static analysis technique for reducing the number of alarms reported by static verifiers while providing sound semantic guarantees. First, VMV extracts semantic environment conditions from a base ...
Verifying dereference safety via expanding-scope analysis
ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis

This paper addresses the challenging problem of verifying the safety of pointer dereferences in real Java programs. We provide an automatic approach to this problem based on a sound interprocedural analysis. We present a staged expanding-scope algorithm ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 6

PLDI '14

June 2014

598 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2666356

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2014
619 pages
ISBN:9781450327848
DOI:10.1145/2594291
General Chair:
Michael O'Boyle
University of Edinburgh
,
Program Chair:
Keshav Pingali
University of Texas, Austin

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2014

Published in SIGPLAN Volume 49, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

52
Total Citations
View Citations
386
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)7

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Dunlap TThorn SEnck WReaves B(2023)Finding Fixed Vulnerabilities with Off-the-Shelf Static Analysis2023 IEEE 8th European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP57164.2023.00036(489-505)Online publication date: Jul-2023
https://doi.org/10.1109/EuroSP57164.2023.00036
Choi YNam J(2023)WINEInformation and Software Technology10.1016/j.infsof.2022.107109155:COnline publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1016/j.infsof.2022.107109
Jana AKhadsare AChimdyalwar BKumar SGhime VVenkatesh R(2021)Fast Change-Based Alarm Reporting for Evolving Software Systems2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00062(546-556)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00062
Nichols LEmre MHardekopf BGrech NLavoie T(2019)Fixpoint reuse for incremental JavaScript analysisProceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis10.1145/3315568.3329964(2-7)Online publication date: 22-Jun-2019
https://dl.acm.org/doi/10.1145/3315568.3329964
Legunsen OZhang YHadzi-Tanovic MRosu GMarinov D(2019)Techniques for Evolution-Aware Runtime Verification2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST.2019.00037(300-311)Online publication date: Apr-2019
https://doi.org/10.1109/ICST.2019.00037
Bouajjani AEnea CLahiri S(2018)Abstract semantic diffing of evolving concurrent programsFormal Methods in System Design10.1007/s10703-018-0322-2Online publication date: 21-Aug-2018
https://doi.org/10.1007/s10703-018-0322-2
Pick LFedyukovich GGupta A(2018)Exploiting Synchrony and Symmetry in Relational VerificationComputer Aided Verification10.1007/978-3-319-96145-3_9(164-182)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96145-3_9
Ferles KWüstholz VChristakis MDillig IBodden ESchäfer WDeursen AZisman A(2017)Failure-directed program trimmingProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106249(174-185)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106249
Çiçek EBarthe GGaboardi MGarg DHoffmann JCastagna GGordon A(2017)Relational cost analysisProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009858(316-329)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009858
Barthe GBlazy SLaporte VPichardie DTrieu A(2017)Verified Translation Validation of Static Analyses2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.16(405-419)Online publication date: Aug-2017
https://doi.org/10.1109/CSF.2017.16
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents