research-article

Open access

Abstract interpretation repair

Authors:

Roberto Giacobazzi,

Francesco RanzatoAuthors Info & Claims

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 426 - 441

https://doi.org/10.1145/3519939.3523453

Published: 09 June 2022 Publication History

Abstract

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.

References

[1]

Aws Albarghouthi and Kenneth L. McMillan. 2013. Beautiful Interpolants. In Proceedings of CAV 2013, 25th International Conference on Computer Aided Verification (Lecture Notes in Computer Science, Vol. 8044). Springer, 313–329. https://doi.org/10.1007/978-3-642-39799-8_22

[2]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press.

Digital Library

[3]

Thomas Ball, Todd D. Millstein, and Sriram K. Rajamani. 2005. Polymorphic predicate abstraction. ACM Trans. Program. Lang. Syst., 27, 2 (2005), 314–343. https://doi.org/10.1145/1057387.1057391

Digital Library

[4]

Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. 2001. Boolean and Cartesian Abstraction for Model Checking C Programs. In Proceedings of TACAS 2001, 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 2031). Springer, 268–283. https://doi.org/10.1007/3-540-45319-9_19

[5]

Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. 2003. Boolean and Cartesian abstraction for model checking C programs. Int. J. Softw. Tools Technol. Transf., 5, 1 (2003), 49–58. https://doi.org/10.1007/s10009-002-0095-0

Digital Library

[6]

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A Static Analyzer for Large Safety-Critical Software. In Proceedings of PLDI 2003, ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, NY, USA. 196–207. isbn:1581136625 https://doi.org/10.1145/781131.781153

Digital Library

[7]

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic. 2020. Abstract extensionality: on the properties of incomplete abstract interpretations. Proc. ACM Program. Lang., 4, POPL (2020), 28:1–28:28. https://doi.org/10.1145/3371096

Digital Library

[8]

Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. In Proceedings of LICS 2021, 36th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 1–13. https://doi.org/10.1109/LICS52264.2021.9470608 Distinguished paper.

Digital Library

[9]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In Proceedings of CAV 2000, 12th International Conference on Computer Aided Verification (Lecture Notes in Computer Science, Vol. 1855). Springer-Verlag, 154–169. https://doi.org/10.1007/10722167_15

[10]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2001. Progress on the State Explosion Problem in Model Checking. In Informatics - 10 Years Back. 10 Years Ahead (Lecture Notes in Computer Science, Vol. 2000). Springer, 176–194. https://doi.org/10.1007/3-540-44577-3_12

[11]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50, 5 (2003), 752–794. https://doi.org/10.1145/876638.876643

Digital Library

[12]

Edmund M. Clarke, Orna Grumberg, and David E. Long. 1994. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16, 5 (1994), 1512–1542. https://doi.org/10.1145/186025.186051

Digital Library

[13]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. The MIT Press.

Digital Library

[14]

Patrick Cousot. 2007. Proving the absence of run-time errors in safety-critical avionics code. In Proceedings of EMSOFT 2007, 7th ACM & IEEE International conference on Embedded software. ACM, 7–9. https://doi.org/10.1145/1289927.1289932

Digital Library

[15]

Patrick Cousot. 2015. Abstracting Induction by Extrapolation and Interpolation. In Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, Deepak D’Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 8931). Springer, 19–42. https://doi.org/10.1007/978-3-662-46081-8_2

Digital Library

[16]

Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press. isbn:9780262044905

[17]

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of ACM POPL’77. ACM, 238–252. https://doi.org/10.1145/512950.512973

Digital Library

[18]

Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of ACM POPL’79. ACM, 269–282. https://doi.org/10.1145/567752.567778

Digital Library

[19]

Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2005. The ASTRÉE Analyzer. In Proceedings of ESOP 2005, 14th European Symposium on Programming (Lecture Notes in Computer Science, Vol. 3444). Springer, 21–30. https://doi.org/10.1007/978-3-540-31987-0_3

Digital Library

[20]

Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. 2012. Theories, solvers and static analysis by abstract interpretation. J. ACM, 59, 6 (2012), 31:1–31:56. https://doi.org/10.1145/2395116.2395120

Digital Library

[21]

Patrick Cousot and Nicolas Halbwachs. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of POPL’78, the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM Press, 84–96. https://doi.org/10.1145/512760.512770

Digital Library

[22]

Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis. 1979. Social Processes and Proofs of Theorems and Programs. Commun. ACM, 22, 5 (1979), 271–280. https://doi.org/10.1145/359104.359106

Digital Library

[23]

Edsger W. Dijkstra. 1972. The Humble Programmer. Commun. ACM, 15, 10 (1972), 859–866. https://doi.org/10.1145/355604.361591

Digital Library

[24]

Edsger W. Dijkstra. 1976. A discipline of programming. Prentice-Hall.

Digital Library

[25]

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019. Scaling static analyses at Facebook. Commun. ACM, 62, 8 (2019), 62–70. https://doi.org/10.1145/3338112

Digital Library

[26]

Gilberto Filé, Roberto Giacobazzi, and Francesco Ranzato. 1996. A unifying view of abstract domain design. ACM Comput. Surv., 28, 2 (1996), 333–336. https://doi.org/10.1145/234528.234742

Digital Library

[27]

Luca Gazzola, Daniela Micucci, and Leonardo Mariani. 2019. Automatic Software Repair: A Survey. IEEE Trans. Software Eng., 45, 1 (2019), 34–67. https://doi.org/10.1109/TSE.2017.2755013

Digital Library

[28]

Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. 2015. Analyzing Program Analyses. In Proceedings of POPL 2015, 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 261–273. https://doi.org/10.1145/2676726.2676987

Digital Library

[29]

Roberto Giacobazzi and Elisa Quintarelli. 2001. Incompleteness, counterexamples and refinements in abstract model-checking. In Proceedings of SAS 2001, 8th International Static Analysis Symposium (Lecture Notes in Computer Science, Vol. 2126). Springer, 356–373. https://doi.org/10.1007/3-540-47764-0_20

[30]

Roberto Giacobazzi and Francesco Ranzato. 2002. States vs. Traces in Model Checking by Abstract Interpretation. In Proceedings of the 9th International Static Analysis Symposium, SAS 2002 (Lecture Notes in Computer Science, Vol. 2477). Springer, 461–476. https://doi.org/10.1007/3-540-45789-5_32

[31]

Roberto Giacobazzi and Francesco Ranzato. 2006. Incompleteness of states w.r.t. traces in model checking. Inf. Comput., 204, 3 (2006), 376–407. https://doi.org/10.1016/j.ic.2006.01.001

[32]

Roberto Giacobazzi and Franceso Ranzato. 2022. History of Abstract Interpretation. IEEE Annals of the History of Computing, 44 (2022), 13 pages. issn:1934-1547 https://doi.org/10.1109/MAHC.2021.3133136

[33]

Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. 2000. Making Abstract Interpretation Complete. Journal of the ACM, 47, 2 (2000), March, 361–416. https://doi.org/10.1145/333979.333989

Digital Library

[34]

Sumit Gulwani, Bill McCloskey, and Ashish Tiwari. 2008. Lifting Abstract Interpreters to Quantified Logical Domains. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). Association for Computing Machinery, 235–246. isbn:9781595936899 https://doi.org/10.1145/1328438.1328468

Digital Library

[35]

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In Proceedings of POPL 2004, 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 232–244. https://doi.org/10.1145/964001.964021

Digital Library

[36]

Krystof Hoder, Laura Kovács, and Andrei Voronkov. 2012. Playing in the grey area of proofs. In Proceedings of POPL 2012, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 259–272. https://doi.org/10.1145/2103656.2103689

Digital Library

[37]

Ranjit Jhala and Rupak Majumdar. 2009. Software Model Checking. ACM Comput. Surv., 41, 4 (2009), Article 21, Oct., 54 pages. issn:0360-0300 https://doi.org/10.1145/1592434.1592438

Digital Library

[38]

Ranjit Jhala and Kenneth L. McMillan. 2006. A Practical and Complete Approach to Predicate Refinement. In Proceedings of TACAS 2006, 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 3920). Springer, 459–473. https://doi.org/10.1007/11691372_33

Digital Library

[39]

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A Formally-Verified C Static Analyzer. In Proceedings of POPL 2015, 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 247–259. https://doi.org/10.1145/2676726.2676966

Digital Library

[40]

Dexter Kozen. 1997. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19, 3 (1997), May, 427–443. issn:0164-0925 https://doi.org/10.1145/256167.256195

Digital Library

[41]

Dexter Kozen. 2000. On Hoare Logic and Kleene Algebra with Tests. ACM Trans. Comput. Logic, 1, 1 (2000), July, 60–76. issn:1529-3785 https://doi.org/10.1145/343369.343378

Digital Library

[42]

Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proceedings of POPL 2006, 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 42–54. isbn:1-59593-027-2 https://doi.org/10.1145/1111037.1111042

Digital Library

[43]

Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. 1995. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6 (1995), 11–44. https://doi.org/10.1007/BF01384313

Digital Library

[44]

Antoine Miné. 2006. The octagon abstract domain. High. Order Symb. Comput., 19, 1 (2006), 31–100. https://doi.org/10.1007/s10990-006-8609-1

Digital Library

[45]

Antoine Miné. 2017. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Foundations and Trends in Programming Languages, 4, 3-4 (2017), 120–372. https://doi.org/10.1561/2500000034

Digital Library

[46]

David Monniaux and Julien Le Guen. 2012. Stratified Static Analysis Based on Variable Dependencies. Electron. Notes Theor. Comput. Sci., 288 (2012), 61–74. https://doi.org/10.1016/j.entcs.2012.10.008

Digital Library

[47]

Martin Monperrus. 2018. Automatic Software Repair: A Bibliography. ACM Comput. Surv., 51, 1 (2018), 17:1–17:24. https://doi.org/10.1145/3105906

Digital Library

[48]

Peter W. O’Hearn. 2020. Incorrectness logic. Proc. ACM Program. Lang., 4, POPL (2020), 10:1–10:32. https://doi.org/10.1145/3371078

Digital Library

[49]

Benjamin Pierce. 2002. Types and Programming Languages. MIT Press. isbn:9780262162098

[50]

Benjamin Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. isbn:0262162288

Digital Library

[51]

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Proc. CAV 2020 (LNCS, Vol. 12225). Springer, 225–252. https://doi.org/10.1007/978-3-030-53291-8_14

Digital Library

[52]

Francesco Ranzato and Francesco Tapparo. 2004. Strong Preservation as Completeness in Abstract Interpretation. In Proceedings of ESOP 2004, 13th European Symposium on Programming (Lecture Notes in Computer Science, Vol. 2986). Springer, 18–32. https://doi.org/10.1007/978-3-540-24725-8_3

[53]

Francesco Ranzato and Francesco Tapparo. 2007. Generalized Strong Preservation by Abstract Interpretation. J. Log. Comput., 17, 1 (2007), 157–197. https://doi.org/10.1093/logcom/exl035

[54]

Xavier Rival and Kwangkeun Yi. 2020. Introduction to Static Analysis – An Abstract Interpretation Perspective. MIT Press.

[55]

Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program., 64, 1 (2007), 54–75. https://doi.org/10.1016/j.scico.2006.03.003

Digital Library

[56]

Enric Rodríguez-Carbonell and Deepak Kapur. 2007. Generating all polynomial invariants in simple loops. J. Symb. Comput., 42, 4 (2007), 443–476. https://doi.org/10.1016/j.jsc.2007.01.002

Digital Library

[57]

Rahul Sharma, Aditya V. Nori, and Alex Aiken. 2012. Interpolants as Classifiers. In Proceedings of CAV 2012, 24th International Conference on Computer Aided Verification (Lecture Notes in Computer Science, Vol. 7358). Springer, 71–87. https://doi.org/10.1007/978-3-642-31424-7_11

Digital Library

[58]

Rahul Sharma, Aditya V. Nori, and Alex Aiken. 2014. Bias-variance tradeoffs in program analysis. In Proceedings of POPL 2014, 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 127–138. https://doi.org/10.1145/2535838.2535853

Digital Library

[59]

Tachio Terauchi and Hiroshi Unno. 2015. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. In Proceedings of ESOP 2015, 24th European Symposium on Programming (Lecture Notes in Computer Science, Vol. 9032). Springer, 610–633. https://doi.org/10.1007/978-3-662-46669-8_25

[60]

Hiroshi Unno and Tachio Terauchi. 2015. Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling. In Proceedings of TACAS 2015, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science, Vol. 9035). Springer, 149–163. https://doi.org/10.1007/978-3-662-46681-0_10

Digital Library

[61]

Moshe Y. Vardi. 2021. Program Verification: Vision and Reality. Commun. ACM, 64, 7 (2021), 5. https://doi.org/10.1145/3469113

Digital Library

[62]

Glynn Winskel. 1993. The Formal Semantics of Programming Languages: an Introduction. MIT press.

Digital Library

Cited By

Giacobazzi RMastroeni IPerantoni E(2024)Adversities in Abstract Interpretation - Accommodating Robustness by Abstract InterpretationACM Transactions on Programming Languages and Systems10.1145/364930946:2(1-31)Online publication date: 24-Feb-2024
https://dl.acm.org/doi/10.1145/3649309
Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Bruni RGiacobazzi RGori RRanzato F(2023)A Correctness and Incorrectness Program LogicJournal of the ACM10.1145/358226770:2(1-45)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582267
Show More Cited By

Index Terms

Abstract interpretation repair
1. Theory of computation
  1. Logic
    1. Abstraction
    2. Logic and verification
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

A Correctness and Incorrectness Program Logic
Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. ...
Refining Model Checking by Abstract Interpretation

Formal methods combining abstract interpretation and model-checking have been considered for automated analysis of software.
In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which ...
Finding feasible abstract counter-examples

A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2022

1038 pages

ISBN:9781450392655

DOI:10.1145/3519939

General Chair:
Ranjit Jhala
University of California at San Diego, USA
,
Program Chair:
Işil Dillig
University of Texas at Austin, USA

Copyright © 2022 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '22

Sponsor:

SIGPLAN

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 13 - 17, 2022

CA, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
785
Total Downloads

Downloads (Last 12 months)266
Downloads (Last 6 weeks)17

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Giacobazzi RMastroeni IPerantoni E(2024)Adversities in Abstract Interpretation - Accommodating Robustness by Abstract InterpretationACM Transactions on Programming Languages and Systems10.1145/364930946:2(1-31)Online publication date: 24-Feb-2024
https://dl.acm.org/doi/10.1145/3649309
Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Bruni RGiacobazzi RGori RRanzato F(2023)A Correctness and Incorrectness Program LogicJournal of the ACM10.1145/358226770:2(1-45)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582267
Bruni RGiacobazzi RGori RRanzato F(2023)Local Completeness in Abstract InterpretationChallenges of Software Verification10.1007/978-981-19-9601-6_8(145-156)Online publication date: 22-Jul-2023
https://doi.org/10.1007/978-981-19-9601-6_8

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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