Invariant Checking for Programs with Procedure Calls

DOI10.1007/978-3-642-03237-0_22zbMATH Open1248.68143OpenAlexW1585143074MaRDI QIDQ3392933FDOQ3392933

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

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

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

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

Cited In (4)

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

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)