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

Floyd-Hoare logicinvariant generationloop invariantsprogram debuggingprogram verification

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

• 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 all polynomial invariants in simple loops
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• scientific article; zbMATH DE number 44976 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• 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)

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

Describes a project that uses

Uses Software

• QEPCAD
• Daikon

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)