Stratified Datalog and Program Analysis

In this entry we formalize stratified Datalog, the first such formalization in Isabelle to the best of our knowledge. Next we formally establish the existence of least solutions for any stratified Datalog program, essential for reasoning about negations in clauses. Lastly we illustrate the usefulness of our Datalog formalization by further formalizing the general Bit-Vector Framework and formalize and prove correct five analyses in this framework namely liveness, reaching definitions, available expressions, very busy expressions and reachability. Many of our definitions follow Nielson and Nielson’s textbook [NN20]. The formalization is described in our SAC 2024 paper [SHN24].

[NN20] Flemming Nielson and Hanne Riis Nielson. Program analysis (an appetizer). CoRR, abs/2012.10086, 2020. https://arxiv.org/abs/2012.10086
[SHN24] Anders Schlichtkrull, René Rydhof Hansen, and Flemming Nielson. Isabelle-verified correctness of Datalog programs for program analysis. In Jiman Hong and Juw Won Park, editors, Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024, Avila, Spain, April 8-12, 2024, pages 1731–1734. ACM, 2024.