Static analysis you can trust, and why

介绍

A Generic, Executable, and Machine-Checked Framework for Interprocedural Abstract Interpretation in Isabelle/HOL

翻译准备中

取自仓库 README

README

正在加载完整 README。 以下为已保存的摘录。

A Verified Goblint-Style Static Analysis Pipeline in Isabelle/HOL Master's thesis. Manuel Lerchner, supervised by @AlexandraGrass Voblint is a machine-checked Isabelle/HOL framework for building, running and verifying interprocedural abstract interpreters, modelled on Goblint's D/G architecture. It chains verified CFG compilation, activation-local operational semantics, executable equation generation, and a vendored verified top-down solver into one soundness statement about the analyzer's own output.