More Web Proxy on the site http://driver.im/

research-article

Certified Abstract Interpretation with Pretty-Big-Step Semantics

Authors:

Alan SchmittAuthors Info & Claims

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

Pages 29 - 40

https://doi.org/10.1145/2676724.2693174

Published: 13 January 2015 Publication History

Abstract

This paper describes an investigation into developing certified abstract interpreters from big-step semantics using the Coq proof assistant. We base our approach on Schmidt's abstract interpretation principles for natural semantics, and use a pretty-big-step (PBS) semantics, a semantic format proposed by Charguéraud. We propose a systematic representation of the PBS format and implement it in Coq. We then show how the semantic rules can be abstracted in a methodical fashion, independently of the chosen abstract domain, to produce a set of abstract inference rules that specify an abstract interpreter. We prove the correctness of the abstract interpreter in Coq once and for all, under the assumption that abstract operations faithfully respect the concrete ones. We finally show how to define correct-by-construction analyses: their correction amounts to proving they belong to the abstract semantics.

References

[1]

R. Bagnara, P. M. Hill, A. Pescetti, and E. Zaffanella. Verification of C programs via natural semantics and abstract interpretation. In Proc. of the IFM 2007 C/C

[2]

Verification Workshop, Technical Report ICIS-R07015, Institute for Computing and Information Sciences (iCIS), pages 75--80. Radboud University Nijmegen, The Netherlands, 2007.

[3]

M. Bodin, T. Jensen, and A. Schmitt. Pretty-big-step-semantics-based certified abstract interpretation (preliminary version). In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday,rm Manhattan, Kansas, USA, 19--20th September 2013, volume 129 of Electronic Proceedings in Theoretical Computer Science, pages 360--383. Open Publishing Association, 2013.

[4]

M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A trusted mechanised javascript specification. In POPL, pages 87--100. ACM, 2014.

Digital Library

[5]

M. Bodin, T. Jensen, and A. Schmitt. Certified abstract interpretation with pretty big-step semantics: Coq development files and analyzers results. http://ajacs.inria.fr/coq/cpp2015/, 2015.

Digital Library

[6]

D. Cachera and D. Pichardie. A certified denotational abstract interpreter. In ITP, pages 9--24, 2010.

Digital Library

[7]

D. Cachera, T. P. Jensen, D. Pichardie, and V. Rusu. Extracting a data flow analyser in constructive logic. Theor. Comput. Sci., pages 56--78, 2005.

Digital Library

[8]

A. Charguéraud. Pretty-big-step semantics. In ESOP, pages 41--60. Springer, 2013. 10.1007/978-3-642-37036-6_3.

Digital Library

[9]

P. Cousot. The calculational design of a generic abstract interpreter. In Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.

[10]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252. ACM, 1977.

Digital Library

[11]

V. Gouranton and D. L. Métayer. Dynamic slicing: a generic analysis based on a natural semantics format. Journal of Logic and Computation, 9 (6), 1999. 10.1093/logcom/9.6.835.

[12]

G. Klein and T. Nipkow. Verified bytecode verifiers. Theor. Comput. Sci., pages 583--626, 2003.

Digital Library

[13]

X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52 (7): 107--115, 2009. URL http://gallium.inria.fr/xleroy/publi/compcert-CACM.pdf.

Digital Library

[14]

X. Leroy and H. Grall. Coinductive big-step operational semantics. Information and Computation, 207: 284--304, 2009.

Digital Library

[15]

C. McBride. Elimination with a motive. In Types for proofs and programs, pages 197--216. Springer, 2002.

[16]

J. Midtgaard and T. Jensen. A calculational approach to control-flow analysis by abstract interpretation. In SAS, volume 5079 of LNCS, pages 347--362. Springer Verlag, 2008. 10.1007/978--3--540--69166--2_23.

Digital Library

[17]

J. Midtgaard and T. Jensen. Control-flow analysis of function calls and returns by abstract interpretation. In ICFP, pages 287--298. ACM, 2009. 10.1145/1596550.1596592.

Digital Library

[18]

D. Park. Fixpoint induction and proofs of program properties. In Machine Intelligence 5, pages 59--78. Edinburgh University Press, 1969.

[19]

D. Pichardie. Building certified static analysers by modular construction of well-founded lattices. In FICS, volume 212 of ENTCS, pages 225--239, 2008. 10.1016/j.entcs.2008.04.064.

Digital Library

[20]

C. B. Poulsen and P. D. Mosses. Deriving pretty-big-step semantics from small-step semantics. In Programming Languages and Systems, pages 270--289. Springer, 2014.

Digital Library

[21]

D. A. Schmidt. Natural-semantics-based abstract interpretation (preliminary version). In SAS, pages 1--18. Springer LNCS vol. 983, 1995. 10.1007/3-540-60360-3_28.

Digital Library

[22]

D. A. Schmidt. Abstract interpretation of small-step semantics. In Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, Springer LNCS vol. 1192, pages 76--99, 1997.

Digital Library

[23]

D. Van Horn and M. Might. Abstracting abstract machines. In ICFP, pages 51--62. ACM, 2010. 10.1145/1995376.1995399.

Digital Library

Cited By

Voogd EJohnsen EKløvstad ÅRot JSilva A(2024)Correct and Complete Symbolic Execution for FreeIntegrated Formal Methods10.1007/978-3-031-76554-4_13(237-255)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-76554-4_13
Khayam ANoizet LSchmitt A(2022)A Faithful Description of ECMAScript AlgorithmsProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551381(1-14)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551381
Bock ABøgholm TSestoft PThomsen BThomsen L(2022)On the cost semantics for spreadsheets with sheet-defined functionsJournal of Computer Languages10.1016/j.cola.2022.10110369(101103)Online publication date: Apr-2022
https://doi.org/10.1016/j.cola.2022.101103
Show More Cited By

Index Terms

Certified Abstract Interpretation with Pretty-Big-Step Semantics
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Abstract interpretation of resolution-based semantics

We extend the abstract interpretation point of view on context-free grammars by Cousot and Cousot to resolution-based logic programs and proof systems. Starting from a transition-based small-step operational semantics of Prolog programs (akin to the ...
Deriving Pretty-Big-Step Semantics from Small-Step Semantics
Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410

Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel 'pretty-big-step' style presented by Charguéraud at ESOP'13. Such rules are less concise than corresponding ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs

January 2015

192 pages

ISBN:9781450332965

DOI:10.1145/2676724

Program Chairs:
Xavier Leroy
Inria Paris-Rocquencourt, France
,
Alwen Tiu
Nanyang Technological University, Singapore

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

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 January 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

INRIA

Conference

POPL '15

Sponsor:

SIGPLAN

POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 13 - 14, 2015

Mumbai, India

Acceptance Rates

CPP '15 Paper Acceptance Rate 18 of 26 submissions, 69%;

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
157
Total Downloads

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

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Voogd EJohnsen EKløvstad ÅRot JSilva A(2024)Correct and Complete Symbolic Execution for FreeIntegrated Formal Methods10.1007/978-3-031-76554-4_13(237-255)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-76554-4_13
Khayam ANoizet LSchmitt A(2022)A Faithful Description of ECMAScript AlgorithmsProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551381(1-14)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551381
Bock ABøgholm TSestoft PThomsen BThomsen L(2022)On the cost semantics for spreadsheets with sheet-defined functionsJournal of Computer Languages10.1016/j.cola.2022.10110369(101103)Online publication date: Apr-2022
https://doi.org/10.1016/j.cola.2022.101103
Al-Sibahi AJensen TDimovski AWąsowski A(2021)Verification of Program Transformations with Inductive Refinement TypesACM Transactions on Software Engineering and Methodology10.1145/340980530:1(1-33)Online publication date: 20-Jan-2021
https://dl.acm.org/doi/10.1145/3409805
Li XZhang QWang GShi ZGuan Y(2021)Reasoning About Iteration and Recursion Uniformly Based on Big-Step SemanticsDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-030-91265-9_4(61-80)Online publication date: 18-Nov-2021
https://doi.org/10.1007/978-3-030-91265-9_4
Al-Sibahi AJensen TDimovski AWąsowski A(2020)Verification of high-level transformations with inductive refinement typesACM SIGPLAN Notices10.1145/3393934.327812553:9(147-160)Online publication date: 7-Apr-2020
https://dl.acm.org/doi/10.1145/3393934.3278125
Dagnino FBono VZucca EDezani-Ciancaglini M(2020)Soundness Conditions for Big-Step SemanticsProgramming Languages and Systems10.1007/978-3-030-44914-8_7(169-196)Online publication date: 27-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-44914-8_7
Bodin MGardner PJensen TSchmitt A(2019)Skeletal semantics and their interpretationsProceedings of the ACM on Programming Languages10.1145/32903573:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290357
Al-Sibahi AJensen TDimovski AWąsowski AVan Wyk ERompf T(2018)Verification of high-level transformations with inductive refinement typesProceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3278122.3278125(147-160)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1145/3278122.3278125
Ströder TGiesl JBrockschmidt MFrohn FFuhs CHensel JSchneider-Kamp PAschermann C(2017)Automatically Proving Termination and Memory Safety for Programs with Pointer ArithmeticJournal of Automated Reasoning10.1007/s10817-016-9389-x58:1(33-65)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1007/s10817-016-9389-x

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.

Media

Figures

Other

Tables

View Table of Contents