On invariant checking

DOI10.1007/S11424-013-1296-1MaRDI QIDQ394493zbMATH OpenOpenAlexWikidataFDO

Authors Zhi-Hai Zhang, Deepak Kapur

Publication date 27 January 2014

Published in Journal of Systems Science and Complexity (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11424-013-1296-1

zbMATH Keywords

program verificationFloyd-Hoare logicinvariant generationloop invariantsprogram debugging

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Theoretical Aspects of Computing - ICTAC 2004
• Mechanical inference of invariants for FOR-loops
• Synthesizing invariants by solving solvable loops
• Maximal and compositional pattern-based loop invariants
• Inferring Loop Invariants Using Postconditions

Cites work

• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• An axiomatic basis for computer programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computer Aided Verification
• Computer Aided Verification
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Generating all polynomial invariants in simple loops
• Non-linear loop invariant generation using Gröbner bases
• Property-directed incremental invariant generation
• QEPCAD B
• Systematic design of program transformation frameworks by abstract interpretation
• The Daikon system for dynamic detection of likely invariants
• Verification Constraint Problems with Strengthening
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• Effective algebraic independence of values of \(E\)-functions
• Invariant Checking for Programs with Procedure Calls
• When is a formula a loop invariant?
• Finding inconsistencies in programs with loops

Describes a project that uses

Uses Software

• Daikon
• QEPCAD

This page was built for publication: On invariant checking

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