Abstract interpretation with a theorem prover

DOI10.1007/3-540-36103-0_43MaRDI QIDQ4412528zbMATH OpenFDO

Authors Hugh Anderson

Publication date 15 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2495/24950411.htm

Mathematics Subject Classification ID

Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Structural Abstract Interpretation: A Formal Study Using Coq
• scientific article; zbMATH DE number 1497823
• Static analysis, abstract interpretation and verification in (constraint logic) programming
• Abstract interpretation based verification of logic programs

Cited in

(14)

• Abstract interpretation using typed decision graphs
• How to transform an analyzer into a verifier
• scientific article; zbMATH DE number 4178791 (Why is no real title available?)
• Abstract Interpretation as Automated Deduction
• The Abella Interactive Theorem Prover (System Description)
• Propositional Interpolation and Abstract Interpretation
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• Abstract interpretation from Büchi automata
• scientific article; zbMATH DE number 6315451 (Why is no real title available?)
• Structural Abstract Interpretation: A Formal Study Using Coq
• Algebraic Methodology and Software Technology
• Automated Reasoning with Analytic Tableaux and Related Methods
• Applications and Theory of Petri Nets 2005
• A systematic approach to abstract interpretation of program transformations

Describes a project that uses

Uses Software

• HOL

This page was built for publication: Abstract interpretation with a theorem prover

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