On invariant checking

DOI10.1007/s11424-013-1296-1zbMath1310.68147OpenAlexW2038243321WikidataQ125290155 ScholiaQ125290155MaRDI QIDQ394493

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

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

Related Items (2)

When Is a Formula a Loop Invariant? ⋮ Effective algebraic independence of values of \(E\)-functions

Uses Software

• QEPCAD
• Daikon

Cites Work

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

This page was built for publication: On invariant checking