article

Open access

Polymorphic predicate abstraction

Authors:

Todd Millstein,

Sriram K. RajamaniAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 27, Issue 2

Pages 314 - 343

https://doi.org/10.1145/1057387.1057391

Published: 01 March 2005 Publication History

Abstract

Predicate abstraction is a technique for creating abstract models of software that are amenable to model checking algorithms. We show how polymorphism, a well-known concept in programming languages and program analysis, can be incorporated in a predicate abstraction algorithm for C programs. The use of polymorphism in predicates, via the introduction of symbolic names for values, allows us to model the effect of a procedure independent of its calling contexts. Therefore, we can safely and precisely abstract a procedure once and then reuse this abstraction across multiple calls and multiple applications containing the procedure. Polymorphism also enables us to handle programs that need to be analyzed in an open environment, for all possible callers. We have proved that our algorithm is sound and have implemented it in the C2BP tool as part of the SLAM software model checking toolkit.

References

[1]

Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. K. 2001a. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation. ACM, New York, pp. 203--213.]]

[2]

Ball, T., Podelski, A., and Rajamani, S. K. 2001b. Boolean and Cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, New York, pp. 268--283.]]

[3]

Ball, T. and Rajamani, S. K. 2000. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop. Lecture Notes in Computer Science, vol. 1885. Springer-Verlag, New York, pp. 113--130.]]

[4]

Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In SPIN 01: SPIN Workshop. Lecture Notes in Computer Science, vol. 2057. Springer-Verlag, New York, pp. 103--122.]]

[5]

Ball, T. and Rajamani, S. K. 2002a. Generating abstract explanations of spurious counterexamples in C programs. Tech. Rep. MSR-TR-2002-09. Microsoft Research, Jan.]]

[6]

Ball, T. and Rajamani, S. K. 2002b. The SLAM project: Debugging system software via static analysis. In POPL 02: Principles of Programming Languages. ACM, New York, pp. 1--3.]]

[7]

Cardelli, L. and Wegner, P. 1985. On understanding types, data abstraction, and polymorphism. Comput. Surv. 17, 4, 471--522.]]

[8]

Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, New York, pp. 154--169.]]

[9]

Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In ICSE 2000: International Conference on Software Engineering. ACM, New York, pp. 439--448.]]

[10]

Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In POPL 77: Principles of Programming Languages. ACM, New York, pp. 238--252.]]

[11]

Das, M. 2000. Unification-based pointer analysis with directional assignments. In PLDI 00: Programming Language Design and Implementation. ACM, New York, pp. 35--46.]]

[12]

Das, S., Dill, D. L., and Park, S. 1999. Experience with predicate abstraction. In CAV 00: Computer-Aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, New York, pp. 160--171.]]

[13]

Detlefs, D., Nelson, G., and Saxe, J. B. 2003. Simplify: A theorem prover for program checking. HP Labs Technical Report HPL-2003-148.]]

[14]

Dijkstra, E. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J.]]

[15]

Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Robby, Visser, W., and Zheng, H. 2001. Tool-supported program abstraction for finite-state verification. In ICSE 01: International Conference on Software Engineering. ACM, New York, pp. 177--187.]]

[16]

Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association.]]

[17]

Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for java. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. ACM, New York, pp. 234--245.]]

[18]

Flanagan, C. and Qadeer, S. 2002. Predicate abstraction for software verification. In POPL '02: Principles of Programming Languages. ACM, New York, 191--202.]]

[19]

Foster, J. S., Fahndrich, M., and Aiken, A. 2000. Polymorphic versus monomorphic flow-insensitive points-to analysis for C. In SAS 00: Static Analysis. Lecture Notes in Computer Science, vol. 1824. Springer-Verlag, New York, pp. 175--198.]]

[20]

Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In CAV 97: Computer-aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 72--83.]]

[21]

Gries, D. 1981. The Science of Programming. Springer-Verlag, New York.]]

[22]

Havelund, K. and Pressburger, T. 1998. Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Tech. Trans. 2, 4 (Apr.).]]

[23]

Henzinger, T. A., Jhala, R., Majumdar, R., and McMillan, K. L. 2004. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York, pp. 232--244.]]

[24]

Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In POPL '02: Principles of Programming Languages (Jan.). ACM, New York, pp. 58--70.]]

[25]

Holzmann, G. 1997. The Spin model checker. IEEE Trans. Softw. Eng. 23, 5 (May), 279--295.]]

[26]

Holzmann, G. 2000. Logic verification of ANSI-C code with Spin. In SPIN 00: SPIN Workshop. Lecture Notes in Computer Science, vol. 1885. Springer-Verlag, New York, pp. 131--147.]]

[27]

Landi, W. and Ryder, B. G. 1992. A safe approximate algorithm for interprocedural pointer aliasing. SIGPLAN Notices 27, 7, 235--248.]]

[28]

Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.]]

[29]

Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML (Revised). The MIT Press, Cambridge, Mass.]]

[30]

Morris, J. M. 1982. A general axiom of assignment. In Theoretical Foundations of Programming Methodology. Lecture Notes of an International Summer School, Reidel, pp. 25--34.]]

[31]

Nelson, G. 1981. Techniques for program verification. Tech. Rep. CSL81-10. Xerox Palo Alto Research Center, Palo Alto, Calif.]]

[32]

Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Principles of Programming Languages. ACM, New York, pp. 49--61.]]

[33]

Saïdi, H. and Shankar, N. 1999. Abstract and model check while you prove. In CAV 99: Computer-aided Verification. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, New York, pp. 443--454.]]

[34]

Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall, New York, pp. 189--233.]]

[35]

Visser, W., Park, S., and Penix, J. 2000. Using predicate abstraction to reduce object-oriented programs for model checking. In FMSP 00: Formal Methods in Software Practice. ACM, New York, pp. 3--12.]]

[36]

Wilson, R. P. and Lam, M. S. 1995. Efficient context-sensitive pointer analysis for C programs. In Proceedings of the ACM SIGPLAN 1995 conference on Programming Language Design and Implementation. ACM, New York, pp. 1--12.]]

Cited By

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 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
Ferles KStephens JDillig I(2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434298
Show More Cited By

Index Terms

Polymorphic predicate abstraction

Recommendations

Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Special issue on POPL 2005

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 27, Issue 2

March 2005

198 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1057387

Issue’s Table of Contents

Copyright © 2005 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2005

Published in TOPLAS Volume 27, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

44
Total Citations
View Citations
1,415
Total Downloads

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

Reflects downloads up to 02 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

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 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
Ferles KStephens JDillig I(2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434298
Wang YDillig ILahiri SCook W(2017)Verifying equivalence of database-driven applicationsProceedings of the ACM on Programming Languages10.1145/31581442:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158144
Larsen KLegay A(2016)Statistical Model Checking: Past, Present, and FutureLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_1(3-15)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_1
Legay AViswanathan M(2015)Statistical model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0384-z17:4(369-376)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.1007/s10009-015-0384-z
Henzinger TJhala RMajumdar RMcMillan K(2014)Abstractions from proofsACM SIGPLAN Notices10.1145/2641638.264165549:4S(79-91)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2641638.2641655
Nikolić ĐSpoto F(2014)Reachability analysis of program variablesACM Transactions on Programming Languages and Systems10.1145/252999035:4(1-68)Online publication date: 3-Jan-2014
https://dl.acm.org/doi/10.1145/2529990
Köpf BRybalchenko A(2013)Automation of Quantitative Information-Flow AnalysisFormal Methods for Dynamical Systems10.1007/978-3-642-38874-3_1(1-28)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38874-3_1
Nikolić ĐSpoto F(2012)Reachability analysis of program variablesProceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_33(423-438)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_33
Show More Cited By

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 Article

Figures

Tables

Media

View Issue’s Table of Contents