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.
Notes related to Intermediate verification language
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]