SMACK verifier

[Google Scholar] [Website]

Notes: LLVM compiler, Boogie verifier, intermediate verification language
Papers: baranowski:atva:2018, rakamaric:cav:2014

SMACK is verifier based on translating LLVM bitcode to Boogie (an intermediate verification language).

Extended static checking (ESC), Rust language, Software Verification Competition (SV-COMP)

Verifying constant-time implementations [almeida:security:2016]
Verifying Rust programs with SMACK [baranowski:atva:2018]
Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]

The opinions expressed are my own views and not my employer’s.