Precise interprocedural analysis through linear algebra
From MaRDI portal
Publication:3452271
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
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
