Abstract interpretation of recursive logic definitions for efficient runtime assertion checking

DOI10.1007/978-3-031-38828-6_10MaRDI QIDQ6535334zbMATH OpenFDO

Authors Thibaut Benajmin, Julien Signoles

Publication date 12 December 2023

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 1497823
• Abstract interpretation based verification of logic programs
• Runtime verification logics. A language design perspective
• scientific article; zbMATH DE number 1975609
• Model Checking Recursive Programs with Exact Predicate Abstraction
• scientific article; zbMATH DE number 1953018
• scientific article; zbMATH DE number 1696591
• Predicate abstraction for program verification

Cites work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Principles of abstract interpretation
• Verified runtime assertion checking for memory properties

Cited in

(1)

• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Abstract interpretation of recursive logic definitions for efficient runtime assertion checking

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