Article

Combining abstract interpreters

Authors:

Ashish TiwariAuthors Info & Claims

PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 376 - 386

https://doi.org/10.1145/1133981.1134026

Published: 11 June 2006 Publication History

Abstract

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 interpreters.We define the notion of logical product of lattices. This kind of combination is more precise than the reduced product combination. We give algorithms to obtain the join operator and the existential quantification operator for the combined lattice from the corresponding operators of the individual lattices. We also give a bound on the number of steps required to reach a fixed point across loops during analysis over the combined lattice in terms of the corresponding bounds for the individual lattices. We prove that our combination methodology yields the most precise abstract interpretation operators over the logical product of lattices when the individual lattices are over theories that are convex, stably infinite, and disjoint.We also present an interesting application of logical product wherein some lattices can be reduced to combination of other (unrelated) lattices with known abstract interpreters.

References

[1]

E. Chang and R. Leino. Abstract interpretation with alien expressions and heap structures. In VMCAI, volume 3385 of LNCS, pages 147--163. Springer, 2005.

Digital Library

[2]

M. Codish, A. Mulkers, M. Bruynooghe, M. G. de la Banda, and M. Hermenegildo. Improving abstract interpretations by combining domains. ACM Transactions on Programming Languages and Systems, 17(1):28--44, 1995.

Digital Library

[3]

A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Trans. Program. Lang. Syst., 19(1):7--47, 1997.

Digital Library

[4]

P. Cousot. Iterative reduced product, Lecture Notes on Abstract Interpretation, Available at http://web.mit.edu/16.399/www/. 2005.

[5]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on POPL, pages 234--252, 1977.

Digital Library

[6]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th ACM Symp. on POPL, pages 269--282, 1979.

Digital Library

[7]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on POPL, pages 84--97, 1978.

Digital Library

[8]

R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Proc. 24th ICALP, volume 1256 of LNCS, pages 771--781, 1997.

Digital Library

[9]

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

Digital Library

[10]

S. Gulwani and G. C. Necula. Discovering affine equalities using random interpretation. In 30th ACM Symposium on POPL, pages 74--84. ACM, Jan. 2003.

Digital Library

[11]

S. Gulwani and G. C. Necula. Global value numbering using random interpretation. In 31st ACM Symposium on POPL, pages 342--352, Jan. 2004.

Digital Library

[12]

S. Gulwani and G. C. Necula. A polynomial-time algorithm for global value numbering. In 11th Static Analysis Symposium, volume 3148 of LNCS, pages 212--227. Springer-Verlag, Aug. 2004.

[13]

S. Gulwani and A. Tiwari. Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In 15th European Symposium on Programming, volume 3924 of LNCS. Springer, Mar. 2006.

Digital Library

[14]

S. Gulwani and A. Tiwari. Combining abstract interpreters. Technical Report MSR-TR-2006-25, Microsoft Research, Mar. 2006.

Digital Library

[15]

S. Gulwani, A. Tiwari, and G. C. Necula. Join algorithms for the theory of uninterpreted symbols. In Conf. on Foundations of Software Tech. and Theor. Comp. Sci., FST&TCS '2004, volume 3328 of LNCS, pages 311--323, 2004.

Digital Library

[16]

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

[17]

S. Lerner, D. Grove, and C. Chambers. Composing dataflow analyses and transformations. In 29th ACM Symposium in POPL, pages 270--282, 2002.

Digital Library

[18]

M. Müller-Olm and H. Seidl. A note on Karr's algorithm. In ICALP, pages 1016--1028, 2004.

[19]

G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245--257, Oct. 1979.

Digital Library

[20]

F. Nielson, H. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 2005.

Digital Library

[21]

T. W. Reps, S. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In VMCAI, volume 2937 of LNCS, pages 252--266. Springer, 2004.

Cited By

Olliaro MArceri VCortesi AFerrara P(2023)Lifting String Analysis DomainsChallenges of Software Verification10.1007/978-981-19-9601-6_7(109-143)Online publication date: 22-Jul-2023
https://doi.org/10.1007/978-981-19-9601-6_7
Arceri VOlliaro MCortesi AFerrara P(2022)Relational String Abstract DomainsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_2(20-42)Online publication date: 14-Jan-2022
https://doi.org/10.1007/978-3-030-94583-1_2
Avanzini MMoser GSchaper M(2020)A modular cost analysis for probabilistic programsProceedings of the ACM on Programming Languages10.1145/34282404:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428240
Show More Cited By

Index Terms

Combining abstract interpreters

Recommendations

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 ...
Lifting abstract interpreters to quantified logical domains
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 Semilattices and Semimodules
Foundations of Software Science and Computation Structures
Abstract
We describe the canonical weak distributive law $δ : S P \to P S$ of the powerset monad $P$ over the S-left-semimodule monad $S$ , for a class of semirings S. We show that the composition of $P$ with $S$ by means of such $δ$ yields almost the monad of convex subsets ... $_{}$

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2006

438 pages

ISBN:1595933204

DOI:10.1145/1133981

General Chair:
Michael Schwartzbach
University of Aarhus, Denmark
,
Program Chair:
Thomas Ball
Microsoft Research

ACM SIGPLAN Notices Volume 41, Issue 6
Proceedings of the 2006 PLDI Conference
June 2006
426 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1133255
Issue’s Table of Contents

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

In-Cooperation

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI06

Sponsor:

PLDI06: ACM SIGPLAN Conference on Programming Language Design and Implementation 2006

June 11 - 14, 2006

Ontario, Ottawa, Canada

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

75
Total Citations
View Citations
686
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Olliaro MArceri VCortesi AFerrara P(2023)Lifting String Analysis DomainsChallenges of Software Verification10.1007/978-981-19-9601-6_7(109-143)Online publication date: 22-Jul-2023
https://doi.org/10.1007/978-981-19-9601-6_7
Arceri VOlliaro MCortesi AFerrara P(2022)Relational String Abstract DomainsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-94583-1_2(20-42)Online publication date: 14-Jan-2022
https://doi.org/10.1007/978-3-030-94583-1_2
Avanzini MMoser GSchaper M(2020)A modular cost analysis for probabilistic programsProceedings of the ACM on Programming Languages10.1145/34282404:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428240
Beyer DWehrheim H(2020)Verification Artifacts in Cooperative Verification: Survey and Unifying Component FrameworkLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_8(143-167)Online publication date: 29-Oct-2020
https://doi.org/10.1007/978-3-030-61362-4_8
Lucas SGutiérrez R(2018)Automatic Synthesis of Logical Models for Order-Sorted First-Order TheoriesJournal of Automated Reasoning10.1007/s10817-017-9419-360:4(465-501)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9419-3
D'silva VUrban C(2017)Abstract Interpretation as Automated DeductionJournal of Automated Reasoning10.1007/s10817-016-9382-458:3(363-390)Online publication date: 1-Mar-2017
https://dl.acm.org/doi/10.1007/s10817-016-9382-4
Dillig IDillig TLi BMcmillan KSagiv M(2017)Synthesis of circular compositional program proofs via abductionInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0397-719:5(535-547)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-015-0397-7
Madsen MYee MLhoták O(2016)From Datalog to flix: a declarative language for fixed points on latticesACM SIGPLAN Notices10.1145/2980983.290809651:6(194-208)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908096
Madsen MYee MLhoták OKrintz CBerger E(2016)From Datalog to flix: a declarative language for fixed points on latticesProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908096(194-208)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908096
Ferrara P(2016)A generic framework for heap and value analyses of object-oriented programming languagesTheoretical Computer Science10.1016/j.tcs.2016.04.001631:C(43-72)Online publication date: 6-Jun-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.001
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