Viper: A Verification Infrastructure for Permission-Based Reasoning
Müller Peter, Malte Schwerhoff, Alexander J. Summers · NATO science for peace and security series. D, Information and communication security · 2017
The automation of verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools: in particular, verification condition generators.