research-article

Lifting abstract interpreters to quantified logical domains

Authors:

Bill McCloskey,

Ashish TiwariAuthors Info & Claims

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 235 - 246

https://doi.org/10.1145/1328438.1328468

Published: 07 January 2008 Publication History

Abstract

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤ i < n ⇒ α[i] = 0). The principal challenge in this effort is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation. We present an automatic technique to convert the standard over-approximation operations provided with all domains into sound under-approximations. We establish the correctness of our abstract interpreters by identifying two lattices---one that establishes the soundness of the abstract interpreter and another that defines its precision, or completeness. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.

References

[1]

Dirk Beyer, Tom Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path invariants. In PLDI, 2007.

Digital Library

[2]

Jesse D. Bingham and Zvonimir Rakamaric. A logic and decision procedure for predicate abstraction of heap-manipulating programs. In VMCAI, pages 207--221, 2006.

Digital Library

[3]

A.R. Bradley, Z. Manna, and H. Sipma. What's decidable about arrays? In VMCAI, volume 3855 of LNCS, pages 427--442. Springer, 2006.

Digital Library

[4]

P. Cerny. Verification par interpretation abstraite de predicats parametriques. Master's thesis, Univ. Paris VII & Ecole normale superieure, Paris 20, 2003.

[5]

Patrick Cousot. Verification by abstract interpretation. In Verification: Theory and Practice, volume 2772 of LNCS, pages 243--268, 2003.

[6]

Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 234--252, 1977.

Digital Library

[7]

Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL, pages 84--97, 1978.

Digital Library

[8]

Cormac Flanagan and Shaz Qadeer. Predicate abstraction for software verification. In POPL, pages 191--202, 2002.

Digital Library

[9]

Denis Gopan, Thomas~W. Reps, and Shmuel Sagiv. A framework for numeric analysis of array operations. In POPL, pages 338--350, 2005.

Digital Library

[10]

Sumit Gulwani and Ashish Tiwari. Combining abstract interpreters. In PLDI, pages 376--386, June 2006.

Digital Library

[11]

Sumit Gulwani and Ashish Tiwari. Static analysis of heap manipulating low-level software. In CAV, LNCS, 2007.

[12]

Sumit Gulwani, Bill McCloskey, and Ashish Tiwari. Lifting abstract interpreters to quantified logical domains. Technical Report MSR-TR-2007-87, Microsoft Research, July 2007.

[13]

Ranjit Jhala and Ken McMillan. Array abstractions from proofs. In CAV, 2007.

Digital Library

[14]

Michael Karr. Affine relationships among variables of a program. In Acta Informatica, pages 133--151. Springer, 1976.

[15]

Shuvendu K. Lahiri and Randal E. Bryant. Indexed predicate discovery for unbounded system verification. In CAV, pages 135--147, 2004.

[16]

Matthew Might. Logic-flow analysis of higher-order programs. In POPL, pages 185--198, 2007.

Digital Library

Cited By

Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Sumanth Prabhu SFedyukovich GD’Souza D(2024)Maximal Quantified Precondition Synthesis for Linear Array LoopsProgramming Languages and Systems10.1007/978-3-031-57267-8_10(245-274)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_10
Sumanth Prabhu SD’Souza DChakraborty SVenkatesh RFedyukovich G(2024)Weakest Precondition Inference for Non-Deterministic Linear Array ProgramsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_9(175-195)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_9
Show More Cited By

Index Terms

Lifting abstract interpreters to quantified logical domains

Recommendations

Lifting abstract interpreters to quantified logical domains
POPL '08

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains. Our quantified abstract domain can represent universally quantified facts like ∀i(0 ≤...
Combining abstract interpreters
Proceedings of the 2006 PLDI Conference

We present a methodology for automatically combining abstract interpreters over given lattices to construct an abstract interpreter for the combination of those lattices. This lends modularity to the process of design and implementation of abstract ...
Combining abstract interpreters
PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present a methodology for automatically combining abstract interpreters over given lattices to construct an abstract interpreter for the combination of those lattices. This lends modularity to the process of design and implementation of abstract ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2008

448 pages

ISBN:9781595936899

DOI:10.1145/1328438

General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

ACM SIGPLAN Notices Volume 43, Issue 1
POPL '08
January 2008
420 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1328897
Issue’s Table of Contents

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL08

Sponsor:

POPL08: The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 7 - 12, 2008

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

142
Total Citations
View Citations
530
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Sumanth Prabhu SFedyukovich GD’Souza D(2024)Maximal Quantified Precondition Synthesis for Linear Array LoopsProgramming Languages and Systems10.1007/978-3-031-57267-8_10(245-274)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57267-8_10
Sumanth Prabhu SD’Souza DChakraborty SVenkatesh RFedyukovich G(2024)Weakest Precondition Inference for Non-Deterministic Linear Array ProgramsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_9(175-195)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_9
Malík VSchrammel PVojnar T(2024)Template-Based Verification of Array-Manipulating ProgramsTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_12(206-224)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_12
Giet JRidoux FRival X(2023)A Product of Shape and Sequence AbstractionsStatic Analysis10.1007/978-3-031-44245-2_15(310-342)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_15
Bruni RGiacobazzi RGori RRanzato FJhala RDillig I(2022)Abstract interpretation repairProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523453(426-441)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523453
Feldman YSagiv MShoham SWilcox J(2022)Property-directed reachability as abstract interpretation in the monotone theoryProceedings of the ACM on Programming Languages10.1145/34986766:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498676
Wang ZAlbarghouthi APrakriya GJha S(2022)Interval universal approximation for neural networksProceedings of the ACM on Programming Languages10.1145/34986756:POPL(1-29)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498675
Castagna GLaurent MNguyễn KLutze M(2022)On type-cases, union elimination, and occurrence typingProceedings of the ACM on Programming Languages10.1145/34986746:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498674
Zhao HYao QSong YKwok JLee D(2021)Side Information Fusion for Recommender Systems over Heterogeneous Information NetworkACM Transactions on Knowledge Discovery from Data10.1145/344144615:4(1-32)Online publication date: 10-Jun-2021
https://dl.acm.org/doi/10.1145/3441446
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.

Figures

Tables

Media

View Table of Conten