---

Sireum Logika is both a highly automated and interactive verification framework for Slang with strong scalability and usability emphases, offering incremental and (massively) parallel verification integrated in the Sireum IVE (Integrated Verification Environment), which is built on top of the widely-used IntelliJ IDE. Logika can: (1) be used without up-front specification costs to verify Slang programs inter-procedurally, (2) leverage behavioral contracts for compositional verification of Slang programs at scale, or (3) employ hybrid inter-procedural/compositional verification to accommodate different application workflows. Moreover, the extensible framework's plugin architecture eases customizations to target/optimize for different application domains (e.g., InfoFlow).

[Pending: see the Logika presentation at TCCOE'22]