Abstract interpretation as automated deduction

DOI10.1007/S10817-016-9382-4MaRDI QIDQ2360874zbMATH OpenOpenAlexFDO

Authors Vijay D'Silva, C. Urban

Publication date 29 June 2017

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-016-9382-4

zbMATH Keywords

abstract interpretationdeductionLindenbaum-Tarski construction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstract Interpretation as Automated Deduction
• scientific article; zbMATH DE number 1953018
• Verification by abstract interpretation
• Abstract interpretation based verification of logic programs
• Abstract interpretation

Cites work

• Abstract conflict driven learning
• Abstract Interpretation as Automated Deduction
• Abstract satisfaction
• Abstract symbolic automata: mixed syntactic/semantic similarity analysis of executables
• Automatic generation of propagation complete SAT encodings
• Automatically Refining Abstract Interpretations
• Conflict-driven conditional termination
• Deciding floating-point logic with abstract conflict driven clause learning
• Extended symbolic finite automata and transducers
• scientific article; zbMATH DE number 3829860 (Why is no real title available?)
• scientific article; zbMATH DE number 5872401 (Why is no real title available?)
• scientific article; zbMATH DE number 3940199 (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?)
• Internal and External Logics of Abstract Interpretations
• Introduction to set constraint-based program analysis
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Program analysis via satisfiability modulo path programs
• Reasoning about infinite computations
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Systematic design of program transformation frameworks by abstract interpretation
• Theories, solvers and static analysis by abstract interpretation

Cited in

(11)

• Verified functional programming of an abstract interpreter
• Contradiction separation based dynamic multi-clause synergized automated deduction
• Automating abstract interpretation
• Conjunctive abstract interpretation using paramodulation
• Abstract Interpretation as Automated Deduction
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• scientific article; zbMATH DE number 3947598 (Why is no real title available?)
• scientific article; zbMATH DE number 1765701 (Why is no real title available?)
• Abstract interpretation from Büchi automata
• Sweeping in Abstract Interpretation
• Automating the functional correspondence between higher-order evaluators and abstract machines

Describes a project that uses

Uses Software

• Dagger
• Verasco

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 Q2360874)