research-article

Public Access

Inferring annotations for device drivers from verification histories

Authors:

Zvonimir Pavlinovic,

Rahul SharmaAuthors Info & Claims

ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

Pages 450 - 460

https://doi.org/10.1145/2970276.2970305

Published: 25 August 2016 Publication History

Abstract

This paper studies and optimizes automated program verification. Detailed reasoning about software behavior is often facilitated by program invariants that hold across all program executions. Finding program invariants is in fact an essential step in automated program verification. Automatic discovery of precise invariants, however, can be very difficult in practice. The problem can be simplified if one has access to a candidate set of assertions (or annotations) and the search for invariants is limited over the space defined by these annotations. Then, the main challenge is to automatically generate quality program annotations. We present an approach that infers program annotations automatically by leveraging the history of verifying related programs. Our algorithm extracts high-quality annotations from previous verification attempts, and then applies them for verifying new programs. We present a case study where we applied our algorithm to Microsoft’s Static Driver Verifier (SDV). SDV is an industrial-strength tool for verification of Windows device drivers that uses manually-tuned heuristics for obtaining a set of annotations. Our technique inferred program annotations comparable in performance to the existing annotations used in SDV that were devised manually by human experts over years. Additionally, the inferred annotations together with the existing ones improved the performance of SDV overall, proving correct 47% of drivers more while running 22% faster in our experiments.

References

[1]

A. Albarghouthi, A. Gurfinkel, Y. Li, S. Chaki, and M. Chechik. Ufo: Verification with interpolants and abstract interpretation. In Tools and Algorithms for the Construction and Analysis of Systems, pages 637–640. Springer, 2013.

Digital Library

[2]

T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, 54(7):68–76, 2011.

Digital Library

[3]

T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pages 203–213, 2001.

Digital Library

[4]

N. E. Beckman, A. V. Nori, S. K. Rajamani, R. J. Simmons, S. Tetali, and A. V. Thakur. Proofs from tests. IEEE Trans. Software Eng., 36(4):495–508, 2010.

Digital Library

[5]

D. Beyer, S. Löwe, E. Novikov, A. Stahlbauer, and P. Wendler. Precision reuse for efficient regression verification. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 389–399, 2013.

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238–252, 1977.

Digital Library

[7]

A. M. Dan, Y. Meshman, M. T. Vechev, and E. Yahav. Predicate abstraction for relaxed memory models. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, pages 84–104, 2013.

[8]

G. Fedyukovich, A. Gurfinkel, and N. Sharygina. Incremental verification of compiler optimizations. In NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pages 300–306, 2014.

Digital Library

[9]

C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for esc/java. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings, pages 500–517, 2001.

Digital Library

[10]

P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: A robust framework for learning invariants. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 69–87, 2014.

Digital Library

[11]

P. Godefroid, S. K. Lahiri, and C. Rubio-González. Statically validating must summaries for incremental compositional dynamic test generation. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, pages 112–128, 2011.

Digital Library

[12]

B. Godlin and O. Strichman. Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3):241–258, 2013.

[13]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 232–244, 2004.

Digital Library

[14]

S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26, 2013, pages 345–355, 2013.

Digital Library

[15]

A. Lal and S. Qadeer. Powering the static driver verifier using corral. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 202–212, 2014.

Digital Library

[16]

A. Lal and S. Qadeer. A program transformation for faster goal-directed search. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pages 147–154, 2014.

Digital Library

[17]

A. Lal and S. Qadeer. DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 280–290, 2015.

Digital Library

[18]

A. Lal, S. Qadeer, and S. K. Lahiri. A solver for reachability modulo theories. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pages 427–443, 2012.

Digital Library

[19]

K. R. M. Leino. This is boogie 2. Manuscript KRML, 178:131, 2008. http://https://github.com/boogie-org/boogie.

[20]

K. L. McMillan and A. Rybalchenko. Computing relational fixed points using interpolation. Technical report, Technical report, 2012. available from authors, 2013.

[21]

Microsoft. The Static Driver Verifier. http://msdn.microsoft.com/en-us/library/windows/ hardware/ff552808(v=vs.85).aspx.

[22]

A. Mishne, S. Shoham, and E. Yahav. Typestate-based semantic code search over partial programs. In Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 997–1016, 2012.

Digital Library

[23]

H. Oh, H. Yang, and K. Yi. Learning a strategy for adapting a program analysis via bayesian optimisation. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 572–588, 2015.

Digital Library

[24]

V. Raychev, M. T. Vechev, and A. Krause. Predicting program properties from big code. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 111–124, 2015.

Digital Library

[25]

V. Raychev, M. T. Vechev, and E. Yahav. Code completion with statistical language models. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, page 44, 2014.

Digital Library

[26]

O. Sery, G. Fedyukovich, and N. Sharygina. Incremental upgrade checking by means of interpolation-based function summaries. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012, pages 114–121, 2012.

[27]

R. Sharma and A. Aiken. From invariant checking to invariant inference using randomized search. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 88–105, 2014.

Digital Library

[28]

R. S. Zvonimir Pavlinovic, Akash Lal. Inferring annotations for device drivers from verification histories. Technical report, Microsoft Research, April 2016.

Cited By

Neider DMadhusudan PSaha SGarg PPark D(2020)A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification EnginesJournal of Automated Reasoning10.1007/s10817-020-09570-z64:7(1523-1552)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09570-z
Zhang CSu TYan YZhang FPu GSu ZDumas MPfahl DApel SRusso A(2019)Finding and understanding bugs in software model checkersProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338932(763-773)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338932
Ezudheen PNeider DD'Souza DGarg PMadhusudan P(2018)Horn-ICE learning for synthesizing invariants and contractsProceedings of the ACM on Programming Languages10.1145/32765012:OOPSLA(1-25)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276501
Show More Cited By

Index Terms

Inferring annotations for device drivers from verification histories
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling
ASE '24: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering

We investigate a modification of the classical Bounded Model Checking (BMC) procedure that does not handle loops through unrolling but via modifications to the control flow graph (CFG). A portion of the CFG representing a loop is replaced by a node ...
An invariant-based approach to the verification of asynchronous parameterized networks

A uniform verification problem for parameterized systems is to determine whether a temporal property is satisfied for every instance of the system which is composed of an arbitrary number of homogeneous processes. To cope with this problem we combine an ...
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '16: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering

August 2016

899 pages

ISBN:9781450338455

DOI:10.1145/2970276

General Chair:
David Lo
Singapore Management University, Singapore
,
Program Chairs:
Sven Apel
University of Passau, Germany
,
Sarfraz Khurshid
University of Texas at Austin, USA

Copyright © 2016 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]

Sponsors

SIGAI: ACM Special Interest Group on Artificial Intelligence
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 August 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ASE'16

Sponsor:

SIGAI
SIGSOFT
IEEE-CS

ASE'16: ACM/IEEE International Conference on Automated Software Engineering

September 3 - 7, 2016

Singapore, Singapore

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
342
Total Downloads

Downloads (Last 12 months)56
Downloads (Last 6 weeks)16

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Neider DMadhusudan PSaha SGarg PPark D(2020)A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification EnginesJournal of Automated Reasoning10.1007/s10817-020-09570-z64:7(1523-1552)Online publication date: 1-Oct-2020
https://dl.acm.org/doi/10.1007/s10817-020-09570-z
Zhang CSu TYan YZhang FPu GSu ZDumas MPfahl DApel SRusso A(2019)Finding and understanding bugs in software model checkersProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338932(763-773)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338932
Ezudheen PNeider DD'Souza DGarg PMadhusudan P(2018)Horn-ICE learning for synthesizing invariants and contractsProceedings of the ACM on Programming Languages10.1145/32765012:OOPSLA(1-25)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276501
Zakharov INovikov E(2018)Compositional Environment Modelling for Verification of GNU C Programs2018 Ivannikov Ispras Open Conference (ISPRAS)10.1109/ISPRAS.2018.00013(39-44)Online publication date: Nov-2018
https://doi.org/10.1109/ISPRAS.2018.00013
Neider DGarg PMadhusudan PSaha SPark D(2018)Invariant Synthesis for Incomplete Verification EnginesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_13(232-250)Online publication date: 12-Apr-2018
https://doi.org/10.1007/978-3-319-89960-2_13
Beyer DLemberger T(2017)Software Verification: Testing vs. Model CheckingHardware and Software: Verification and Testing10.1007/978-3-319-70389-3_7(99-114)Online publication date: 12-Nov-2017
https://doi.org/10.1007/978-3-319-70389-3_7

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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

Media

Figures

Other

Tables

View Table of Contents