当前位置:网站首页>how to prove compiler‘s correctness
how to prove compiler‘s correctness
2022-07-07 17:09:00 【大魔法师云中君】
Formal verification
Compiler correctness for all input programs
since the tool to find the proof (theorem prover) is implemented in software and is complex,
there is a high probability it will contain errors.
One approach has been to use a tool that verifies the proof (a proof checker) which,
because it is much simpler than a proof-finder, is less likely to contain errors.
A prominent example of this approach is CompCert,
which is a formally verified optimizing compiler of a large subset of C99.
Translation validation: compiler correctness on a given program
In contrast to attempting to prove that a compiler is correct for all valid input programs
translation validation aims to automatically establish that a given input program is compiled correctly
compares the intermediate form of the program before and after each compiler pass and verifies the preservation of semantics.
Testing
generates random programs to try to find bugs in a compiler
minimize a found test case to make it easier to understand
边栏推荐
- 数据验证框架 Apache BVal 再使用
- Micro service remote debug, nocalhost + rainbow micro service development second bullet
- 2022.07.02
- Initial experience of cache and ehcache "suggestions collection"
- L1-025 positive integer a+b (Lua)
- State mode - Unity (finite state machine)
- AI来搞财富分配比人更公平?来自DeepMind的多人博弈游戏研究
- Interview vipshop internship testing post, Tiktok internship testing post [true submission]
- Review of network attack and defense
- Solve the error reporting problem of rosdep
猜你喜欢
Multimodal point cloud fusion and visual location based on image and laser
2022.07.05
2022.07.02
How to choose the appropriate automated testing tools?
[Blue Bridge Cup training 100 questions] sort scratch from small to large. Blue Bridge Cup scratch competition special prediction programming question centralized training simulation exercise question
ES6笔记一
链式二叉树的基本操作(C语言实现)
Numpy——2. Shape of array
2022上半年朋友圈都在传的10本书,找到了
In the first half of 2022, I found 10 books that have been passed around by my circle of friends
随机推荐
Numpy——axis
国内首次!这家中国企业的语言AI实力被公认全球No.2!仅次于谷歌
Responsibility chain model - unity
Redis
How much does it cost to develop a small program mall?
RISCV64
Uvalive – 4621 CAV greed + analysis "suggestions collection"
虚拟数字人里的生意经
unity2d的Rigidbody2D的MovePosition函数移动时人物或屏幕抖动问题解决
Realize payment function in applet
完整的电商系统
2022.07.05
6. About JWT
多个kubernetes集群如何实现共享同一个存储
Wechat web debugging 8.0.19 replace the X5 kernel with xweb, so the X5 debugging method can no longer be used. Now there is a solution
如何选择合适的自动化测试工具?
SlashData开发者工具榜首等你而定!!!
[Blue Bridge Cup training 100 questions] sort scratch from small to large. Blue Bridge Cup scratch competition special prediction programming question centralized training simulation exercise question
博睿数据入选《2022爱分析 · IT运维厂商全景报告》
Policy mode - unity