Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
复制标题
利用编译器中间表示进行多语言和跨语言验证
DOI：
10.1007/978-3-030-39322-9_5
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Rakamaric, Zvonimir
中科院分区：
文献类型：
--
作者：
Garzella, Jack;Baranowski, Marek;He, Shaobo;Rakamaric, Zvonimir
如今，开发人员经常使用具有不同特性和权衡的许多编程语言。不幸的是，从头开始实现一个新语言的软件验证器是一个庞大而繁琐的任务，需要多个领域的专家知识，如编译器，验证和约束求解。因此，只有一小部分使用的语言有现成的软件验证器，以帮助开发正确的程序。在过去的十年中，在实现软件验证器时，有一种利用流行的编译器中间表示（IR）的趋势，例如LLVM IR。处理IR承诺开箱即用的多语言和跨语言验证，因为至少在理论上，验证器应该能够处理可以编译成IR的任何编程语言（及其组合）的程序。在本文中，我们提供了一个过程中添加到一个基于IR的验证工具流支持一种新的语言。使用我们的过程中，我们扩展的SMACK验证与原型支持6个额外的语言。我们通过几个案例研究来评估我们的扩展的质量，我们详细描述了我们的经验，以指导未来在这方面的努力。
Developers nowadays regularly use numerous programming languages with different characteristics and trade-offs. Unfortunately, implementing a software verifier for a new language from scratch is a large and tedious undertaking, requiring expert knowledge in multiple domains, such as compilers, verification, and constraint solving. Hence, only a tiny fraction of the used languages has readily available software verifiers to aid in the development of correct programs. In the past decade, there has been a trend of leveraging popular compiler intermediate representations (IRs), such as LLVM IR, when implementing software verifiers. Processing IR promises out-of-the-box multi- and cross-language verification since, at least in theory, a verifier ought to be able to handle a program in any programming language (and their combination) that can be compiled into the IR. In practice though, to the best of our knowledge, nobody has explored the feasibility and ease of such integration of new languages. In this paper, we provide a procedure for adding support for a new language into an IR-based verification toolflow. Using our procedure, we extend the SMACK verifier with prototypical support for 6 additional languages. We assess the quality of our extensions through several case studies, and we describe our experience in detail to guide future efforts in this area.
登录
查看更多内容
用于验证堆操作的森林自动机
影响因子：
0.8
作者：
P. Habermehl;L. Holík;Adam Rogalewicz;Jirí Simácek;Tomáš Vojnar
通讯作者：
Tomáš Vojnar
本国的
DOI：
--
发表时间：
1996
期刊：
Encyclopedic Dictionary of Archaeology
影响因子：
--
作者：
Jay Williams
通讯作者：
Jay Williams
Joogie：从 Java 到 Jimple 到 Boogie
DOI：
--
发表时间：
2013
期刊：
State Of the Art in Java Program Analysis
影响因子：
--
作者：
Stephan Arlt;P. Rümmer;Martin Schäf
通讯作者：
Martin Schäf
级联2.0
DOI：
--
发表时间：
2014
期刊：
International Conference on Verification, Model Checking and Abstract Interpretation
影响因子：
--
作者：
Wen Wang;Clark W. Barrett;Thomas Wies
通讯作者：
Thomas Wies
渐进验证者
DOI：
--
发表时间：
2014
期刊：
NASA Formal Methods
影响因子：
--
作者：
Stephan Arlt;Cindy Rubio;P. Rümmer;Martin Schäf;N. Shankar
通讯作者：
N. Shankar