Invariant Checking for Programs with Procedure Calls

DOI10.1007/978-3-642-03237-0_22MaRDI QIDQ3392933zbMATH OpenOpenAlexFDO

Authors Guillem Godoy, Ashish Tiwari

Publication date 18 August 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03237-0_22

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

• When is a formula a loop invariant?
• On invariant checking
• Decidability of inferring inductive invariants
• Inadequacy of computable loop invariants
• Accurate invariant checking for programs manipulating lists and arrays with infinite data

Cites work

• scientific article; zbMATH DE number 1670780 (Why is no real title available?)
• A generic approach to the static analysis of concurrent programs with procedures
• Assertion Checking Unified
• Automata, Languages and Programming
• Automata, Languages and Programming
• Computing Procedure Summaries for Interprocedural Analysis
• Context unification with one context variable
• Equational formulae with membership constraints
• Interprocedurally Analyzing Polynomial Identities
• Logical Interpretation: Static Program Analysis Using Theorem Proving
• On Context-Free Languages
• Precise interprocedural analysis through linear algebra
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(4)

• What's decidable about program verification modulo axioms?
• Interprocedural reachability for flat integer programs
• When is a formula a loop invariant?
• Second-order programs with preconditions

This page was built for publication: Invariant Checking for Programs with Procedure Calls

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