An intermediate verification language is a simple verification language that more complex languages can be converted down to.

A critical feature in IVLs is that any error messages can be converted back to the source language as in the Boogie verification debugger.

Examples include the Boogie verifier and the Viper verifier.

Notes related to Intermediate verification language

Boogie verifier, CIVL verifier, Prusti verifier, SMACK verifier, Viper verifier

Papers related to Intermediate verification language

• Verifying Rust programs with SMACK [baranowski:atva:2018]
• Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
• A polymorphic intermediate verification language: Design and logical encoding [leino:tacas:2010]
• Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]
• SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]
• CIVL: the concurrency intermediate verification language [siegel:sc:2015]