Affine relationships among variables of a program
From MaRDI portal
Publication:1238409
DOI10.1007/BF00268497zbMath0358.68025MaRDI QIDQ1238409
Publication date: 1976
Published in: Acta Informatica (Search for Journal in Brave)
Related Items (58)
A generic framework for heap and value analyses of object-oriented programming languages ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ An abstract domain to infer symbolic ranges over nonnegative parameters ⋮ Algebraic program analysis ⋮ Porous invariants ⋮ Backward symbolic execution with loop folding ⋮ Some ways to reduce the space dimension in polyhedra computations ⋮ The octagon abstract domain ⋮ Computing polynomial program invariants ⋮ Recent advances in program verification through computer algebra ⋮ Iterative methods of program analysis ⋮ Reflexive transitive invariant relations: A basis for computing loop functions ⋮ Modular inference of subprogram contracts for safety checking ⋮ A quantifier-elimination based heuristic for automatically generating inductive assertions for programs ⋮ Automatic generation of invariants and intermediate assertions ⋮ Transformation-Enabled Precondition Inference ⋮ String abstract domains and their combination ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ What else is undecidable about loops? ⋮ Inferring Congruence Equations Using SAT ⋮ Reference count analysis with shallow aliasing ⋮ Discovering invariants via simple component analysis ⋮ Convex Hull of Arithmetic Automata ⋮ Inferring Min and Max Invariants Using Max-Plus Polyhedra ⋮ Analysing All Polynomial Equations in ${\mathbb Z_{2^w}}$ ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Verification conditions for source-level imperative programs ⋮ Generating all polynomial invariants in simple loops ⋮ Property-directed incremental invariant generation ⋮ Algebra-based synthesis of loops and their invariants (invited paper) ⋮ Precise interprocedural dataflow analysis with applications to constant propagation ⋮ Efficient SAT-based bounded model checking for software verification ⋮ Constructing invariants for hybrid systems ⋮ The Abstract Domain of Parallelotopes ⋮ An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations ⋮ Loop invariants ⋮ Inferring Loop Invariants Using Postconditions ⋮ Abstract interpretation of mobile systems ⋮ Unnamed Item ⋮ Pentagons: a weakly relational abstract domain for the efficient validation of array accesses ⋮ Static Contract Checking with Abstract Interpretation ⋮ An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints ⋮ Reasoning Algebraically About P-Solvable Loops ⋮ Non-disjunctive Numerical Domain for Array Predicate Abstraction ⋮ Transfer Function Synthesis without Quantifier Elimination ⋮ Program Analysis Using Weighted Pushdown Systems ⋮ Acceleration in Convex Data-Flow Analysis ⋮ Information Leakage Analysis by Abstract Interpretation ⋮ Precise interprocedural dataflow analysis with applications to constant propagation ⋮ Range and Set Abstraction using SAT ⋮ Region Analysis for Race Detection ⋮ Applications of polyhedral computations to the analysis and verification of hardware and software systems ⋮ Combining Equational Reasoning ⋮ Context unification with one context variable ⋮ Mathematics for reasoning about loop functions ⋮ Discovery of invariant equalities in programs over data fields ⋮ Intensional Kleene and Rice theorems for abstract program semantics ⋮ Abstract cofibered domains: Application to the alias analysis of untyped programs
Cites Work
This page was built for publication: Affine relationships among variables of a program
