research-article

Open access

Formally Verifying Optimizations with Block Simulations

Authors:

Benjamin Bonneau,

Sylvain Boulmé,

David Monniaux,

Alexandre BérardAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2

Article No.: 224, Pages 59 - 88

https://doi.org/10.1145/3622799

Published: 16 October 2023 Publication History

Abstract

CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing C compiler. Indeed, some optimizations of “gcc ‍-O1” such as Lazy Code Motion (LCM) or Strength Reduction (SR) were still missing: developing these efficient optimizations together with their formal proofs remained a challenge.

Cyril Six et al. have developed efficient formally verified translation validators for certifying the results of superblock schedulers and peephole optimizations. We revisit and generalize their approach into a framework (integrated into CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also Dead Code Elimination (DCE), Constant Propagation (CP), and more noticeably, LCM and SR. In contrast to other approaches to translation validation, we co-design our untrusted optimizations and their validators. Our optimizations provide hints, in the forms of invariants or CFG morphisms, that help keep the formally verified validators both simple and efficient. Such designs seem applicable beyond CompCert.

References

[1]

9899:1999. International standard—Programming languages—C. ISO/IEC.

[2]

Martín Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci., 82, 2 (1991), 253–284. https://doi.org/10.1016/0304-3975(91)90224-P

Digital Library

[3]

Jean-Raymond Abrial. 1996. The B-book - assigning programs to meanings. Cambridge University Press. isbn:978-0-521-02175-3 https://doi.org/10.1017/CBO9780511624162

[4]

Andrew W. Appel. 1998. SSA is Functional Programming. SIGPLAN Not., 33, 4 (1998), apr, 17–20. issn:0362-1340 https://doi.org/10.1145/278283.278285

Digital Library

[5]

Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04). Association for Computing Machinery, New York, NY, USA. 14–25. isbn:158113729X https://doi.org/10.1145/964001.964003

Digital Library

[6]

Frédéric Besson, Sandrine Blazy, and Pierre Wilke. 2019. CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. J. Autom. Reason., 63, 2 (2019), 369–392. https://doi.org/10.1007/s10817-018-9496-y

Digital Library

[7]

Rastislav Bodík, Rajiv Gupta, and Mary Lou Soffa. 1998. Complete Removal of Redundant Expressions. In Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI ’98). Association for Computing Machinery, New York, NY, USA. 1–14. isbn:0897919874 https://doi.org/10.1145/277650.277653

Digital Library

[8]

Sylvain Boulmé. 2021. Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). Université Grenoble Alpes. https://hal.archives-ouvertes.fr/tel-03356701

[9]

Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. 2019. Semantic Program Alignment for Equivalence Checking. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 1027–1040. isbn:9781450367127 https://doi.org/10.1145/3314221.3314596

Digital Library

[10]

Basile Clément and Albert Cohen. 2022. End-to-End Translation Validation for the Halide Language. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), Article 84, apr, 30 pages. https://doi.org/10.1145/3527328

Digital Library

[11]

Basile Clément. 2022. Translation Validation of Tensor Compilers. Ph. D. Dissertation. École Normale Supérieure, Paris, France. https://basile.clement.pm/papers/phd.pdf

[12]

Charlie Curtsinger and Emery D Berger. 2013. STABILIZER: Statistically Sound Performance Evaluation. In ASPLOS’2013. ACM, 219–228. https://doi.org/10.1145/2451116.2451141

Digital Library

[13]

Delphine Demange. 2012. Semantic Foundations of Intermediate Program Representations. Ph. D. Dissertation. École Normale Supérieure de Cachan, France. http://people.irisa.fr/Delphine.Demange/papers/DemangePhD.pdf EAPLS Best PhD Dissertation Award 2012. Gilles Kahn PhD Thesis Award 2013

[14]

Delphine Demange and Yon Fernandez de Retana. 2016. Mechanizing conventional SSA for a verified destruction with coalescing. In 25th International Conference on Compiler Construction. Barcelona, Spain. https://doi.org/10.1145/2892208.2892222

Digital Library

[15]

Delphine Demange, David Pichardie, and Léo Stefanesco. 2015. Verifying Fast and Sparse SSA-based Optimizations in Coq. In 24th International Conference on Compiler Construction, CC 2015. London, United Kingdom. https://doi.org/10.1007/978-3-662-46663-6_12

[16]

Heiko Falk, Sebastian Altmeyer, Peter Hellinckx, Björn Lisper, Wolfgang Puffitsch, Christine Rochange, Martin Schoeberl, Rasmus Bo Sørensen, Peter Wägemann, and Simon Wegener. 2016. TACLeBench: A Benchmark Collection to Support Worst-Case Execution Time Research. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016), Martin Schoeberl (Ed.) (OpenAccess Series in Informatics (OASIcs), Vol. 55). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 2:1–2:10.

[17]

Léo Gourdin. 2023. Lazy Code Transformations in a Formally Verified Compiler. In ICOOOLPS ’23: 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems. ACM, Seattle WA USA, United States. 3–14. https://doi.org/10.1145/3605158.3605848 HAL:hal-04108775.

Digital Library

[18]

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, and Alexandre Bérard. 2023. Artifact of the "Formally Verifying Optimizations with Block Simulations" OOPSLA’23 paper. Proceedings of the ACM on Programming Languages, September, https://doi.org/10.5281/zenodo.8314677

Digital Library

[19]

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard, and all CompCert and Chamois CompCert authors. 2023. Chamois CompCert Software Heritage Archive. https://archive.softwareheritage.org/browse/origin/directory/?origin_url=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/Chamois-CompCert.git

[20]

M.R. Guthaus, J.S. Ringenberg, D. Ernst, T.M. Austin, T. Mudge, and R.B. Brown. 2001. MiBench: A free, commercially representative embedded benchmark suite. In Proceedings of the Fourth Annual IEEE International Workshop on Workload Characterization. WWC-4 (Cat. No.01EX538). IEEE, Austin, TX, USA. 3–14. isbn:978-0-7803-7315-0 https://doi.org/10.1109/WWC.2001.990739

[21]

Wen-mei Hwu, Scott Mahlke, William Chen, Pohua Chang, Nancy Warter, Roger Bringmann, Roland Ouellette, Richard Hank, Tokuzo Kiyohara, Grant Haab, John Holm, and Daniel Lavery. 1993. The Superblock: An Effective Technique for VLIW and Superscalar Compilation. The Journal of Supercomputing, 7 (1993), 05, 229–248. isbn:978-1-4613-6404-7 https://doi.org/10.1007/BF01205185

Digital Library

[22]

Justus Fasse. 2021. Code Transformations to Increase Prepass Scheduling Opportunities in CompCert. Université Grenoble Alpes. https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf

[23]

Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi. 2018. Crellvm: Verified Credible Compilation for LLVM. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). Association for Computing Machinery, New York, NY, USA. 631–645. isbn:9781450356985 https://doi.org/10.1145/3192366.3192377

Digital Library

[24]

Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, and Grigore Roşu. 2021. Language-Parametric Compiler Validation with Application to LLVM. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’21). Association for Computing Machinery, New York, NY, USA. 1004–1019. isbn:9781450383172 https://doi.org/10.1145/3445814.3446751

Digital Library

[25]

James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM, 19, 7 (1976), 385–394. https://doi.org/10.1145/360248.360252

Digital Library

[26]

Claude Kirchner and Hélène Kirchner. 2014. Equational logic and rewriting. In Handbook of the History of Logic, Dov M. Gabbay, Jörg H. Siekmann, and John Woods (Eds.) (History of Logic and Computation in the 20th Century, Vol. 9). Elsevier. https://hal.inria.fr/hal-01183817

[27]

Jens Knoop, Oliver Ruthing, and Bernhard Steffen. 1995. Optimal Code Motion: Theory and Practice. ACM Transactions on Programming Languages and Systems, 16 (1995), September, https://doi.org/10.1145/183432.183443

Digital Library

[28]

Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1992. Lazy code motion. In Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation - PLDI ’92. ACM Press, San Francisco, California, United States. 224–234. isbn:978-0-89791-475-8 https://doi.org/10.1145/143095.143136

Digital Library

[29]

Jens Knoop, Oliver Rüthing, and Bernhard Steffen. 1993. Lazy Strength Reduction. Journal of Programming Languages, 1 (1993), 71–91.

[30]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 179–191. isbn:9781450325448 https://doi.org/10.1145/2535838.2535841

Digital Library

[31]

Monica S. Lam. 1988. Software Pipelining: An Effective Scheduling Technique for VLIW Machines. In Programming Language Design and Implementation (PLDI). ACM Press.

[32]

Olivier Lebeltel, David Monniaux, Cyril Six, and Léo Gourdin. 2023. Chamois Benches Software Heritage Archive. https://archive.softwareheritage.org/browse/origin/directory/?origin_url=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/chamois-benchs.git

[33]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), https://doi.org/10.1145/1538788.1538814

Digital Library

[34]

Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning, 43, 4 (2009), 363–446. http://xavierleroy.org/publi/compcert-backend.pdf

[35]

Xavier Leroy. 2011. Verified squared: does critical software deserve verified tools? In POPL’11. ACM, Austin, TX, USA. 1–2. https://doi.org/10.1145/1926385.1926387

Digital Library

[36]

Vsevolod Livinskii, Dmitry Babokin, and John Regehr. 2020. Random testing for C and C++ compilers with YARPGen. Proc. ACM Program. Lang., 4, OOPSLA (2020), 196:1–196:25. https://doi.org/10.1145/3428264

Digital Library

[37]

David Monniaux and Sylvain Boulmé. 2022. The Trusted Computing Base of the CompCert Verified Compiler. In Programming Languages and Systems (ESOP 2022), Ilya Sergey (Ed.) (LNCS, Vol. 13240). Springer, Munich, Germany. 204–233. https://doi.org/10.1007/978-3-030-99336-8_8

Digital Library

[38]

David Monniaux, Léo Gourdin, Sylvain Boulmé, and Olivier Lebeltel. 2023. Testing a Formally Verified Compiler. In Tests and Proofs - 17th International Conference, TAP 2023, Held as Part of STAF 2023, July, 2023, Proceedings, Virgile Prevosto and Cristina Seceleanu (Eds.) (LNCS, Vol. 14066). Springer. isbn:978-3-031-38827-9 https://doi.org/10.1007/978-3-031-38828-6_3 HAL:hal-04096390.

Digital Library

[39]

David Monniaux and Cyril Six. 2021. Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. In LCTES ’21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021, Jörg Henkel and Xu Liu (Eds.). ACM, 85–96. https://doi.org/10.1145/3461648.3463850

Digital Library

[40]

David Monniaux and Cyril Six. 2022. Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. ACM Trans. Embed. Comput. Syst., mar, issn:1539-9087 https://doi.org/10.1145/3529507

Digital Library

[41]

Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman. 2016. Verified peephole optimizations for CompCert. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 448–461. https://doi.org/10.1145/2908080.2908109

Digital Library

[42]

Todd Mytkowicz, Amer Diwan, Matthias Hauswirth, and Peter F Sweeney. 2009. Producing Wrong Data Without Doing Anything Obviously Wrong!. In ASPLOS’2009. ACM, 265–276. https://doi.org/10.1145/1508244.1508275

Digital Library

[43]

George C. Necula. 2000. Translation validation for an optimizing compiler. In Programming Language Design and Implementation (PLDI). ACM Press, 83–94. https://doi.org/10.1145/349299.349314

Digital Library

[44]

Nicolas Nardino. 2021. Register-Pressure-Aware Prepass-Scheduling for CompCert. ENS de Lyon. https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf

[45]

Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Tools and Algorihtms for the Construction and Analysis of Systems (TACAS) (LNCS, Vol. 1384). Springer, 151–166. https://doi.org/10.1007/BFb0054170

[46]

Louis-Noël Pouchet. 2012. the Polyhedral Benchmark suite. http://web.cs.ucla.edu/~pouchet/software/polybench/

[47]

John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. 2012. Test-case reduction for C compiler bugs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012, Jan Vitek, Haibo Lin, and Frank Tip (Eds.). ACM, 335–346. https://doi.org/10.1145/2254064.2254104

Digital Library

[48]

Silvain Rideau and Xavier Leroy. 2010. Validating register allocation and spilling. In Compiler Construction (CC 2010) (LNCS, Vol. 6011). Springer, 224–243. http://gallium.inria.fr/~xleroy/publi/validation-regalloc.pdf

Digital Library

[49]

Martin C. Rinard and Darko Marino. 1999. Credible Compilation with Pointers. In Proceedings of the FLoC Workshop on Run-Time Result Verification. https://people.csail.mit.edu/rinard/paper/credibleCompilation.html

[50]

Hanan Samet. 1976. Compiler testing via symbolic interpretation. In Proceedings of the 1976 Annual Conference, Houston, Texas, USA, October 20-22, 1976, John A. Gosden and Olin G. Johnson (Eds.). ACM, 492–497. https://doi.org/10.1145/800191.805648

Digital Library

[51]

Thomas Arthur Leck Sewell, Magnus O. Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 471–482. https://doi.org/10.1145/2491956.2462183

Digital Library

[52]

Cyril Six. 2021. Optimized and formally-verified compilation for a VLIW processor. Ph. D. Dissertation. Université Grenoble Alpes. https://hal.archives-ouvertes.fr/tel-03326923

[53]

Cyril Six, Sylvain Boulmé, and David Monniaux. 2020. Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang., 4, OOPSLA (2020), 129:1–129:29. https://doi.org/10.1145/3428197 HAL:hal-02185883.

Digital Library

[54]

Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, and Nicolas Nardino. 2022. Formally Verified Superblock Scheduling. In Certified Programs and Proofs (CPP ’22). Philadelphia, United States. https://doi.org/10.1145/3497775.3503679

Digital Library

[55]

Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2011. Equality Saturation: A New Approach to Optimization. Log. Methods Comput. Sci., 7, 1 (2011), https://doi.org/10.2168/LMCS-7(1:10)2011

[56]

Zachary Tatlock and Sorin Lerner. 2010. Bringing Extensibility to Verified Compilers. SIGPLAN Not., 45, 6 (2010), jun, 111–121. issn:0362-1340 https://doi.org/10.1145/1809028.1806611

Digital Library

[57]

Jean-Baptiste Tristan, Paul Govereau, and Greg Morrisett. 2011. Evaluating value-graph translation validation for LLVM. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011. ACM, 295–305. https://doi.org/10.1145/1993498.1993533

Digital Library

[58]

Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: a Case Study on Instruction Scheduling Optimizations. In Principles of Programming Languages (POPL). ACM Press, 17–27. https://doi.org/10.1145/1328438.1328444

Digital Library

[59]

Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion. In Programming Language Design and Implementation (PLDI). ACM Press, 316–326. http://gallium.inria.fr/~xleroy/publi/validation-LCM.pdf

[60]

Jean-Baptiste Tristan and Xavier Leroy. 2010. A simple, verified validator for software pipelining. In Principles of Programming Languages (POPL). ACM Press, 83–92. http://gallium.inria.fr/~xleroy/publi/validation-softpipe.pdf

[61]

Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In Programming Language Design and Implementation (PLDI). ACM Press, 283–294. https://doi.org/10.1145/1993498.1993532

Digital Library

[62]

Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). Association for Computing Machinery, New York, NY, USA. 427–440. isbn:9781450310833 https://doi.org/10.1145/2103656.2103709

Digital Library

[63]

Zhide Zhou, Zhilei Ren, Guojun Gao, and He Jiang. 2021. An empirical study of optimization bugs in GCC and LLVM. Journal of Systems and Software, 174 (2021), 110884. issn:0164-1212 https://doi.org/10.1016/j.jss.2020.110884

Cited By

Yang ZShirako JSarkar V(2024)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689739
Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674629
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Show More Cited By

Index Terms

Formally Verifying Optimizations with Block Simulations

Recommendations

Formally verified superblock scheduling
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks ...
Certified and efficient instruction scheduling: application to interlocked VLIW processors

CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with ...
Formal verification of translation validators: a case study on instruction scheduling optimizations
POPL '08

Translation validation consists of transforming a program and a posteriori validating it in order to detect a modification of itssemantics. This approach can be used in a verified compiler, provided that validation is formally proved to be correct. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue OOPSLA2

October 2023

2250 pages

EISSN:2475-1421

DOI:10.1145/3554312

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 October 2023

Published in PACMPL Volume 7, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

LabEx PERSYVAL-Lab
IRT Nanoelec

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
358
Total Downloads

Downloads (Last 12 months)337
Downloads (Last 6 weeks)38

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yang ZShirako JSarkar V(2024)Fully Verified Instruction SchedulingProceedings of the ACM on Programming Languages10.1145/36897398:OOPSLA2(791-816)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689739
Melquiond GMoreau J(2024)A Safe Low-Level Language for Computer Algebra and Its Formally Verified CompilerProceedings of the ACM on Programming Languages10.1145/36746298:ICFP(121-146)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674629
Parthasarathy GDardinier TBonneau BMüller PSummers A(2024)Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification LanguageProceedings of the ACM on Programming Languages10.1145/36564388:PLDI(1510-1534)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656438
Monniaux DTimany ATraytel DPientka BBlazy S(2024)Memory Simulations, Security and Optimization in a Verified CompilerProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636952(103-117)Online publication date: 9-Jan-2024
https://doi.org/10.1145/3636501.3636952
Monniaux D(2024)Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-024-00760-326:4(463-477)Online publication date: 1-Aug-2024
https://dl.acm.org/doi/10.1007/s10009-024-00760-3
Li XLiang HFeng X(2024)Verified Validation for Affine Scheduling in Polyhedral CompilationTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_17(287-305)Online publication date: 29-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-64626-3_17
Gourdin LJul ERacordon D(2023)Lazy Code Transformations in a Formally Verified CompilerProceedings of the 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems10.1145/3605158.3605848(3-14)Online publication date: 17-Jul-2023
https://doi.org/10.1145/3605158.3605848

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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

Media

Figures

Other

Tables

View Issue’s Table of Contents