Automatic bit- and memory-precise verification of eBPF code

DOI10.29007/SJ4LMaRDI QIDQ7025187zbMATH OpenFDO

Authors Martin Bromberger, Simon Schwarz, Christoph Weidenbach

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/SJ4L

zbMATH Keywords

constrained Horn clauseseBPFprogram verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Computer aided verification. 34th international conference, CAV 2022, Haifa, Israel, August 7--10, 2022. Proceedings. Part II
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Efficient CTL verification via Horn constraints solving
• Faster, higher, stronger: E 2.3
• Handbook of satisfiability. In 2 parts
• Horn clause solvers for program verification
• Horn clauses for communicating timed systems
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 1341618 (Why is no real title available?)
• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Polite theories revisited
• Proving Termination of C Programs with Lists
• Refutational theorem proving for hierarchic first-order theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
• Seventeen provers under the hammer
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Superposition for higher-order logic
• Symbolic Model Construction for Saturated Constrained Horn Clauses
• The MathSAT5 SMT solver
• Why3 -- where programs meet provers

This page was built for publication: Automatic bit- and memory-precise verification of eBPF code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7025187)