Towards a verified range analysis for JavaScript JITs
Towards a verified range analysis for JavaScript JITs
复制标题
针对 JavaScript JIT 进行经过验证的范围分析
DOI：
10.1145/3385412.3385968
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Stefan, Deian
中科院分区：
文献类型：
--
作者：
Brown, Fraser;Renner, John;Nötzli, Andres;Lerner, Sorin;Shacham, Hovav;Stefan, Deian
我们提出了一个用于验证浏览器JIT编译器中的范围分析的系统VeRA。浏览器开发人员用C++的一个子集编写范围分析例程，验证开发人员编写基础结构来验证自定义分析属性。然后，VeRA自动验证范围分析例程，浏览器开发人员可以直接将其集成到JIT中。我们使用VeRA来翻译和验证Firefox范围分析例程，它检测到一个新的，已确认的错误，已经存在于浏览器中六年。
We present VeRA, a system for verifying therange analysispass in browser just-in-time (JIT) compilers. Browser developers write range analysis routines in a subset of C++, and verification developers write infrastructure to verify custom analysis properties. Then, VeRA automatically verifies the range analysis routines, which browser developers can integrate directly into the JIT. We use VeRA to translate and verify Firefox range analysis routines, and it detects a new, confirmed bug that has existed in the browser for six years.
登录
查看更多内容
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
JavaScript 的操作语义
DOI：
--
发表时间：
2008
期刊：
Asian Symposium on Programming Languages and Systems
影响因子：
--
作者：
S. Maffeis;John C. Mitchell;Ankur Taly
通讯作者：
Ankur Taly
使用 CLP 模糊 Rust 类型检查器
DOI：
--
发表时间：
2015
期刊：
影响因子：
--
作者：
Kyle Dewey;Jared Roesch;B. Hardekopf
通讯作者：
B. Hardekopf
JavaScript 的快速、精确的混合类型推理
DOI：
10.1145/2254064.2254094
发表时间：
2012
期刊：
Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Brian Hackett;Shu
通讯作者：
Shu
Alive-FP：LLVM 中基于浮点的窥孔优化的自动验证
DOI：
--
发表时间：
2016
期刊：
Sensors Applications Symposium
影响因子：
--
作者：
David Menendez;Santosh Nagarakatte;Aarti Gupta
通讯作者：
Aarti Gupta