Integration of linear arithmetic and goal-oriented resolution for software reasoning

MaRDI QIDQ2782497zbMATH OpenFDO

Authors Tie-Chung Wang, Allen Goldberg

Publication date 3 April 2002

zbMATH Keywords

linear arithmetic decision procedure

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4112064
• A practical approach to satisfiability modulo linear integer arithmetic
• Integrating Linear Arithmetic into Superposition Calculus
• An even closer integration of linear arithmetic into inductive theorem proving
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Integration of linear arithmetic and goal-oriented resolution for software reasoning

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