When is a formula a loop invariant?

DOI10.1007/978-3-319-23165-5_13MaRDI QIDQ2945711zbMATH OpenOpenAlexFDO

Authors Stephan Falke, Deepak Kapur

Publication date 14 September 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-23165-5_13

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Invariant Checking for Programs with Procedure Calls
• Search for invariant linear relationships in programs
• On invariant checking
• An iterative method for generating loop invariants
• Could We Have Chosen a Better Loop Invariant or Method Contract?

Cites work

• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• A refutational approach to geometry theorem proving
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Generalized property directed reachability
• Generating all polynomial invariants in simple loops
• scientific article; zbMATH DE number 3941661 (Why is no real title available?)
• Ideals, Varieties, and Algorithms
• Linear ranking for linear lasso programs
• Model Checking Software
• On invariant checking
• Programming Languages and Systems
• Property directed polyhedral abstraction
• Property-directed incremental invariant generation
• SAT-Based Model Checking without Unrolling
• Synthesis of circular compositional program proofs via abduction
• Understanding IC3
• Verification Constraint Problems with Strengthening

Cited in

(5)

• On invariant synthesis for parametric systems
• Invariant Checking for Programs with Procedure Calls
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• WHEN IS A UNIT LOOP f-UNITARY?
• scientific article; zbMATH DE number 7559488 (Why is no real title available?)

This page was built for publication: When is a formula a loop invariant?

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