《 即时编译的正式验证 》
- 即时编译形式化验证编译器动态优化推测优化逆向优化解释执行机器代码生成CompCertCoq
- #技术专著 #编译器正确性 #方法论指南 #研究受众 #创新解决方案 #机械化验证 #学术著作
- 选题分类：计算机理论 软件工程
- 原版语种：英语（可提供图书翻译服务）
- 出版日期：2025年02月
- 页数：176页
- 图书定价：（不详）
- 开本：195mm×234mm
- 原出版地：美国
- 字数：（不详）
- 作品星级：
- 内文印刷：单色
申请样书样章
您正在通过本网站在线提交出版评估申请。
若您的申请获得通过，您将可以在线对本作品的电子样书进行查看。
特别提示：
1、一旦提交本申请，则表示您承诺自愿通过成都锐拓传媒广告有限公司申请上述图书的中文版权，并承诺在申请日起18个月内，不会向任何第三方（包括但不限于图书作者、出版方及其他代理商等）申请或联系上述图书的中文简体版权。否则，我公司有权关闭您在本网站的使用权限，且不再与您进行任何业务合作，并有权要求您支付不低于人民币5000元/本的违约金，或将上述违约金直接从您的账户余额中予以扣除。
2、您通过本功能在线申请样书样章而支付的费用仅为样书样章在线查阅的费用，不代表我公司对上述图书的中文版权授权事宜向您作出任何承诺。除非发生我公司无法向您提交样书或样章的情况，否则无论最终是否与您达成中文版权的交易合作，该费用概不退还。
申请翻译样章
您正在通过本网站在线提交翻译样章申请。
若您的申请获得通过，您将可以在线对本作品的翻译样章进行查看。
特别提示：
1、一旦提交本申请，则表示您承诺自愿通过成都锐拓传媒广告有限公司申请上述图书的中文版权，并承诺在申请日起18个月内，不会向任何第三方（包括但不限于图书作者、出版方及其他代理商等）申请或联系上述图书的中文简体版权。否则，我公司有权关闭您在本网站的使用权限，且不再与您进行任何业务合作，并有权要求您支付不低于人民币5000元/本的违约金，或将上述违约金直接从您的账户余额中予以扣除。
2、您通过本功能在线申请样书样章而支付的费用仅为样书样章在线查阅的费用，不代表我公司对上述图书的中文版权授权事宜向您作出任何承诺。除非发生我公司无法向您提交样书或样章的情况，否则无论最终是否与您达成中文版权的交易合作，该费用概不退还。
内容简介
然而，即时编译器采用的技术可能尤为复杂，这种复杂性往往成为程序缺陷和安全漏洞的根源。如何确保即时编译器不存在错误？针对传统提前编译器，业界已开发出多种预防编译错误的技术，其中形式化验证编译就是典型代表——通过数学证明确保编译后程序的语义与源代码语义保持一致。但即时编译器出现时间较晚，认知程度较低，且受到的验证研究关注远少于传统编译器。
为将形式化验证引入即时编译领域，本书系统性地识别了一系列特定验证挑战，并针对每个挑战提出了创新解决方案。这些挑战包括动态优化、推测优化、逆向优化以及解释执行与机器代码生成的交错处理。作者创新性地重用了CompCert等形式化验证提前编译器的证明技术，通过该方法论，读者可以开发即时编译器并形式化证明其行为符合所执行程序的语义规范。书中所有证明均在Coq证明助手中完成机械化验证。
作者介绍
洛桑联邦理工学院（EPFL）SYSTEMF实验室博士后，现任洛桑联邦理工学院SYSTEMF实验室博士后研究员，与克莱门特·皮特-克劳德尔共事。研究方向聚焦编程语言实现的形式化验证，特别是现代正则表达式引擎与即时编译器。
当前项目致力于现代正则表达式的形式化研究，致力于开发具有线性时间复杂度的实用正则表达式匹配新算法。部分算法已应用于V8 JavaScript引擎的线性正则表达式引擎。同时研究现代正则表达式语义的机械化实现及其引擎的形式化验证。
博士阶段在桑德琳·布拉兹与大卫·皮夏尔迪指导下从事即时编译（JIT）的形式化验证研究，论文获EAPLS最佳博士论文奖。该项目中设计了基于Coq证明助手的即时编译器正确性验证方法论。相较于传统提前编译器，即时编译器具备动态程序优化、代码行为推测以及本地代码与解释代码交错执行等特性。该研究攻克了这些新型验证挑战，并在Coq中开发了经形式化验证的原型即时编译器。
相关推荐
然而，即时编译器采用的技术可能尤为复杂，这种复杂性往往成为程序缺陷和安全漏洞的根源。如何确保即时编译器不存在错误？针对传统提前编译器，业界已开发出多种预防编译错误的技术，其中形式化验证编译就是典型代表——通过数学证明确保编译后程序的语义与源代码语义保持一致。但即时编译器出现时间较晚，认知程度较低，且受到...
请输入分享的Email地址：
