Isabelle-verified correctness of Datalog programs for program analysis

被引：0

作者：

Schlichtkrull, Anders ^{[1
]}

Hansen, Rene Rydhof ^{[2
]}

Nielson, Flemming ^{[3
]}

机构：

[1] Aalborg Univ, Copenhagen, Denmark

[2] Aalborg Univ, Aalborg, Denmark

[3] Tech Univ Denmark, Lyngby, Denmark

来源：

39TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2024 | 2024年

关键词：

Datalog; static analysis; formal methods; Isabelle;

D O I：

10.1145/3605098.3636091

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

Static program analysis has become an essential tool for developers to find and avoid bugs as well as security vulnerabilities. This is particularly important for applications requiring formal verification, e.g., safety- or security-critical applications. We formalize and prove correct all the components needed to specify and perform static analysis based on the Datalog logic programming language, including the first known Isabelle formalization of stratified Datalog. In addition the existence of least solutions for any stratified Datalog program is established and proven. We demonstrate the usefulness of our formalization by further formalizing the general Bit-Vector Framework and prove correct four classic analyses in this framework.

引用

页码：1731 / 1732

页数：2

共 13 条

[1] Certifying Standard and Stratified Datalog Inference Engines in SSReflect [J].

Benzaken, Veronique ;

Contejean, Evelyne ;

Dumbrava, Stefania .

INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 :171-188

[2]

Ceri S., 1989, IEEE Transactions on Knowledge and Data Engineering, V1, P146, DOI 10.1109/69.43410

[3] MONOTONE DATA FLOW ANALYSIS FRAMEWORKS [J].

KAM, JB ;

ULLMAN, JD .

ACTA INFORMATICA, 1977, 7 (03) :305-317

[4]

Kildall Gary A., 1973, Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. POPL'73, P194, DOI DOI 10.1145/512927.512945

[5]

Madsen M, 2016, ACM SIGPLAN NOTICES, V51, P194, DOI [10.1145/2908080.2908096, 10.1145/2980983.2908096]

[6]

Nielson Flemming, 2020, arXiv

[7]

Nipkow T., 2002, LECT NOTES COMPUTER, V2283, DOI [10.1007/3-540-45949-9, DOI 10.1007/3-540-45949-9]

[8]

Nipkow Tobias, 2014, Concrete Semantics-With Isabelle/HOL, DOI [DOI 10.1007/978-3-319-10542-0, 10.1007/978-3-319-10542-0]

[9]

Przymusinski Teodor C., 1988, Foundations of Deductive Databases and Logic Programming, P193, DOI DOI 10.1016/B978-0-934613-40-8.50009-9

[10]

Schlichtkrull Anders, 2023, Formal proof development for the present paper

← 1 2 →