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 an industrial-grade IDE -- Sireum IVE. Logika can: (1) be used without up-front specification costs to verify Slang programs interprocedurally, (2) leverage behavioral contracts for compositional verification of Slang programs at scale, or (3) employ hybrid interprocedural/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]