Leveraging compiler intermediate representation for multi- and cross-language verification

DOI10.1007/978-3-030-39322-9_5zbMath1451.68071OpenAlexW3000442391MaRDI QIDQ784116

Jack J. Garzella, Zvonimir Rakamarić, Marek Baranowski, Shaobo He

Publication date: 5 August 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-39322-9_5

zbMATH Keywords

verificationcompiler intermediate representationcross-languagemulti-language

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Haskell
• DiVinE
• Frama-C
• z3
• LLVM
• KLEE
• Scala
• VCC
• Predator
• SMTInterpol
• CPAchecker
• UFO
• SatAbs
• Joogie
• Julia
• Viper
• SeaHorn
• BoogiePL
• SMACK
• Rust
• Swift
• Kotlin
• Calysto
• GraVy
• Rust2Viper
• Pyston
• Crust
• Cascade
• CIVL

This page was built for publication: Leveraging compiler intermediate representation for multi- and cross-language verification