soc logo

"No bird soars too high, if he soars with his own wings."   W. Blake

Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification

VMCAI 2020 screenshot

Abstract

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.

Citation

Jack Garzella, Marek Baranowski, Shaobo He, Zvonimir Rakamaric
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 11990: 90--111, doi:10.1007/978-3-030-39322-9_5, 2020.

BibTeX

@inproceedings{2020_vmcai_gbhr,
  title = {Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification},
  author = {Jack Garzella and Marek Baranowski and Shaobo He and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  series = {Lecture Notes in Computer Science},
  volume = {11990},
  publisher = {Springer},
  editor = {Dirk Beyer and Damien Zufferey},
  pages = {90--111},
  doi = {10.1007/978-3-030-39322-9_5},
  year = {2020}
}

Acknowledgements

Supported by funding from the Undergraduate Research Opportunities Program at the University of Utah awarded to Jack J. Garzella, the National Science Foundation awards CNS 1527526 and CCF 1837051, and a gift from the VMware’s University Research Fund.