On invariant checking

DOI10.1007/S11424-013-1296-1zbMATH Open1310.68147OpenAlexW2038243321WikidataQ125290155 ScholiaQ125290155MaRDI QIDQ394493FDOQ394493

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

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

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)

Cites Work

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

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

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)