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

DOI10.1007/978-3-030-39322-9_5MaRDI QIDQ784116zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(2)

• A polymorphic intermediate verification language: design and logical encoding
• Verifying an Open Compiler Using Multi-language Semantics

Describes a project that uses

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)