Precise interprocedural analysis through linear algebra

DOI10.1145/964001.964029zbMath1325.68068OpenAlexW2171834078MaRDI QIDQ3452271

Helmut Seidl, Markus Müller-Olm

Publication date: 11 November 2015

Published in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/964001.964029

zbMATH Keywords

interprocedural analysislinear algebraweakest preconditionaffine relationpolynomial relation

Mathematics Subject Classification ID

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

Related Items (33)

Analysis of linear definite iterative loops ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Model Checking Procedural Programs ⋮ Computing polynomial program invariants ⋮ Recent advances in program verification through computer algebra ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ The structure of polynomial invariants of linear loops ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis ⋮ A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis ⋮ Reference count analysis with shallow aliasing ⋮ Nonlinear invariants for linear loops and eigenpolynomials of linear operators ⋮ Polynomial invariants for linear loops ⋮ Generating all polynomial invariants in simple loops ⋮ Data flow analysis of asynchronous systems using infinite abstract domains ⋮ Interprocedural shape analysis using separation logic-based transformer summaries ⋮ An Iterative Method for Generating Loop Invariants ⋮ Elimination Techniques for Program Analysis ⋮ A method of proving the invariance of linear inequalities for linear loops ⋮ LTL over integer periodicity constraints ⋮ Certification Using the Mobius Base Logic ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ Inter-procedural Two-Variable Herbrand Equalities ⋮ Interprocedural Analysis of Concurrent Programs Under a Context Bound ⋮ Upper Adjoints for Fast Inter-procedural Variable Equalities ⋮ Program Analysis Using Weighted Pushdown Systems ⋮ View-Augmented Abstractions ⋮ Invariant Checking for Programs with Procedure Calls ⋮ Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem ⋮ A new abstraction framework for affine transformers ⋮ Reducing concurrent analysis under a context bound to sequential analysis ⋮ Intensional Kleene and Rice theorems for abstract program semantics

This page was built for publication: Precise interprocedural analysis through linear algebra