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

DOI10.1007/978-3-030-39322-9_5zbMATH Open1451.68071OpenAlexW3000442391MaRDI QIDQ784116FDOQ784116

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

Recommendations

• A polymorphic intermediate verification language: design and logical encoding
• Verifying an Open Compiler Using Multi-language Semantics
• Formalizing the LLVM intermediate representation for verified program transformations
• Verifying Whiley programs with Boogie
• Relational program reasoning using compiler IR

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)

Cited In (1)

• Verifying an Open Compiler Using Multi-language Semantics

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q784116)