Abstract interpretation as automated deduction

DOI10.1007/S10817-016-9382-4zbMATH Open1410.68222OpenAlexW1424885608MaRDI QIDQ2360874FDOQ2360874

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

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

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)

Cites Work

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

Cited In (11)

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

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)