and another one on verification condition generation (VCG). Based on the Viper infrastructure, several frontends for various programming languages have emerged: Gobra for Go, Nagini for Python, Prusti for Rust, and VerCors for C, Java, OpenCL, and OpenMP. These frontends translate the frontend programming language into Viper to then use a Viper verification backend for proving the input program's correctness. The Mezzo Programming Language and Asynchronous Liquid Separation Types include ideas related to CSL in the type system for a programming language. The idea to include separation in a type system has earlier examples in Alias Types and Syntactic Control of Interference. The distinction between interactive and in-between verifiers is not a sharp one. For example, Bedrock strives for a high degree of automation, in what it terms mostly-automatic verification, where Verifast sometimes requires annotations that resemble the tactics (little programs) used in interactive verifiers. References 2002 introductions Program logic Substructural logic Logic in computer science