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

  • Jack J. Garzella
  • Marek Baranowski
  • Shaobo HeEmail author
  • Zvonimir Rakamarić
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11990)


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.


Verification Multi-language Cross-language Compiler intermediate representation 


  1. 1.
    Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: a framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012). Scholar
  2. 2.
    Arlt, S., Rubio-González, C., Rümmer, P., Schäf, M., Shankar, N.: The gradual verifier. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 313–327. Springer, Cham (2014). Scholar
  3. 3.
    Arlt, S., Rümmer, P., Schäf, M.: Joogie: from java through jimple to boogie. In: ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis (SOAP), pp. 3–8 (2013).
  4. 4.
    Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3(OOPSLA), 147:1–147:30 (2019). Scholar
  5. 5.
    Babić, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: International Conference on Software Engineering (ICSE), pp. 211–220 (2008).
  6. 6.
    Baranová, Z., et al.: Model checking of C and C++ with DIVINE 4. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 201–207. Springer, Cham (2017). Scholar
  7. 7.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). Scholar
  8. 8.
    Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: USENIX Conference on Operating Systems Design and Implementation (OSDI), pp. 209–224 (2008)Google Scholar
  9. 9.
    Carter, M., He, S., Whitaker, J., Rakamarić, Z., Emmi, M.: SMACK software verification toolchain. In: International Conference on Software Engineering (ICSE), pp. 589–592 (2016).
  10. 10.
    Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007). Scholar
  11. 11.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005). Scholar
  12. 12.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). Scholar
  13. 13.
    Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). Scholar
  14. 14.
    Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 137–148 (2009).
  15. 15.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). Scholar
  16. 16.
    The D programming language.
  17. 17.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). Scholar
  18. 18.
    DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005). Scholar
  19. 19.
    Stack overflow developer survey (2018).
  20. 20.
    Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing Semantic models of programs with the software analysis workbench. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 56–72. Springer, Cham (2016). Scholar
  21. 21.
    Dudka, K., Peringer, P., Vojnar, T.: Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 372–378. Springer, Heidelberg (2011). Scholar
  22. 22.
  23. 23.
    Filliâtre, J.-C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004). Scholar
  24. 24.
    The Flang Fortran compiler.
  25. 25.
    The Go programming language.
  26. 26.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). Scholar
  27. 27.
    Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 424–440. Springer, Heidelberg (2011). Scholar
  28. 28.
    Hahn, F.: Rust2Viper: Building a Static Verifier for Rust. Master’s thesis, ETH (2016)Google Scholar
  29. 29.
    The Haskell programming language.
  30. 30.
    Heizmann, M., et al.: Ultimate automizer with SMTInterpol. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 641–643. Springer, Heidelberg (2013). Scholar
  31. 31.
    Bezanson, J., Edelman, A., Karpinski, S., Shah, V.B.: Julia: a fresh approach to numerical computing. SIAM Rev. 59, 65–98 (2017). Scholar
  32. 32.
  33. 33.
    Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012). Scholar
  34. 34.
    Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization (CGO), pp. 75–86 (2004)Google Scholar
  35. 35.
    The LLVM compiler infrastructure.
  36. 36.
    LLVM language reference manual.
  37. 37.
    Merz, F., Falke, S., Sinz, C.: Bounded model checking of C and C++ programs using a compiler IR. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 146–161. Springer, Heidelberg (2012). Scholar
  38. 38.
    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). Scholar
  39. 39.
    Pǎsǎreanu, C.S., et al.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 15–26 (2008).
  40. 40.
  41. 41.
    Rakamarić, Z., Emmi, M.: SMACK: Decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106–113. Springer, Cham (2014). Scholar
  42. 42.
    Rakamarić, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 290–304. Springer, Heidelberg (2008). Scholar
  43. 43.
  44. 44.
    half: f16 type for Rust.
  45. 45.
    The Rust programming language.
  46. 46.
  47. 47.
    Siegel, S.F., et al.: CIVL: the concurrency intermediate verification language. In: International Conference for High Performance Computing, Networking, Storage and Analysis (SC), pp. 61:1–61:12 (2015).
  48. 48.
    SMACK software verifier and verification toolchain.
  49. 49.
    The Swift programming language.
  50. 50.
    Toman, J., Pernsteiner, S., Torlak, E.: CRUST: a bounded verifier for rust. In: IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 75–80 (2015).
  51. 51.
    Wang, W., Barrett, C., Wies, T.: Cascade 2.0. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 142–160. Springer, Heidelberg (2014). Scholar
  52. 52.
    Woodward, M.: Announcing LLILC – a new LLVM-based compiler for.NET (2015).

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Jack J. Garzella
    • 1
  • Marek Baranowski
    • 1
  • Shaobo He
    • 1
    Email author
  • Zvonimir Rakamarić
    • 1
  1. 1.School of ComputingUniversity of UtahSalt Lake CityUSA

Personalised recommendations