Precise interprocedural analysis through linear algebra

DOI10.1145/964001.964029zbMATH Open1325.68068OpenAlexW2171834078MaRDI QIDQ3452271FDOQ3452271

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

Recommendations

• Precise interprocedural dataflow analysis with applications to constant propagation
• Precise interprocedural dataflow analysis with applications to constant propagation
• Interprocedural analyses: a comparison
• Interprocedurally Analysing Linear Inequality Relations
• Precise interprocedural analysis using random interpretation

zbMATH Keywords

linear algebraweakest preconditionaffine relationinterprocedural analysispolynomial relation

Mathematics Subject Classification ID

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

Cited In (37)

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

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

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