Abstract Interpretation as Automated Deduction

DOI10.1007/978-3-319-21401-6_31MaRDI QIDQ3454115zbMATH OpenFDO

Authors Vijay D'Silva, C. Urban

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Abstract interpretation as automated deduction
• Automating abstract interpretation
• scientific article; zbMATH DE number 1953018
• scientific article; zbMATH DE number 1949621
• scientific article; zbMATH DE number 1696591
• Abstract interpretation from a denotational-semantics perspective
• Abstract interpretation and application to logic programs
• Abstract interpretation from Büchi automata
• Automatic construction of Hoare proofs from abstract interpretation results.
• Automatically Refining Abstract Interpretations

Cites work

• scientific article; zbMATH DE number 5872401 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• scientific article; zbMATH DE number 3198011 (Why is no real title available?)
• Abstract conflict driven learning
• Abstract satisfaction
• Automatically Refining Abstract Interpretations
• Deciding floating-point logic with abstract conflict driven clause learning
• Internal and External Logics of Abstract Interpretations
• Introduction to set constraint-based program analysis
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Numeric bounds analysis with conflict-driven learning
• Program analysis via satisfiability modulo path programs
• Systematic design of program transformation frameworks by abstract interpretation
• Theories, solvers and static analysis by abstract interpretation

Cited in

(8)

• Verification, Model Checking, and Abstract Interpretation
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Conjunctive abstract interpretation using paramodulation
• scientific article; zbMATH DE number 1953018 (Why is no real title available?)
• Automating abstract interpretation
• Abstract interpretation from Büchi automata
• Abstract interpretation as automated deduction
• Internal and External Logics of Abstract Interpretations

Describes a project that uses

Uses Software

• Dagger

This page was built for publication: Abstract Interpretation as Automated Deduction

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