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

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

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

• 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?)
• Abstract Interpretation as Automated Deduction
• Abstract conflict driven learning
• 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
• 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)

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

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)