Invariant Checking for Programs with Procedure Calls

DOI10.1007/978-3-642-03237-0_22zbMath1248.68143OpenAlexW1585143074MaRDI QIDQ3392933

Guillem Godoy, Ashish Kumar 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

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

Related Items (3)

Interprocedural Reachability for Flat Integer Programs ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Inter-procedural Two-Variable Herbrand Equalities

Cites Work

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

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