Automated deduction for verification

DOI10.1145/1592434.1592437MaRDI QIDQ5228111zbMATH OpenOpenAlexFDO

Authors Natarajan Shankar

Publication date 9 August 2019

Published in ACM Computing Surveys (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1592434.1592437

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Deductive software verification: from pen-and-paper proofs to industrial tools
• Publication:4941841
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Abstract Interpretation as Automated Deduction
• Combining Model Checking and Deduction

Cited in

(10)

• Interpolation systems for ground proofs in automated deduction: a survey
• A system for deduction-based formal verification of workflow-oriented software models
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Verification conditions for source-level imperative programs
• Automated deduction techniques for the management of personalized documents
• Combining Model Checking and Deduction
• On interpolation in automated theorem proving
• scientific article; zbMATH DE number 1418281 (Why is no real title available?)
• Satisfiability modulo finite fields
• Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models

This page was built for publication: Automated deduction for verification

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