Static Analysis by Abstract Interpretation: A Mathematical Programming Approach

DOI10.1016/j.entcs.2010.09.007zbMath1342.68086OpenAlexW2102181048MaRDI QIDQ2814107

Stéphane Le Roux, Leo Liberti, Fabrizio Marinelli, Eric Goubault, Jeremy Leconte

Publication date: 17 June 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2010.09.007

zbMATH Keywords

branch-and-boundconstraintspolicy iterationbilinear MINLPguaranteed smallest code invariant

Mathematics Subject Classification ID

Applications of mathematical programming (90C90) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Side-constrained minimum sum-of-squares clustering: mathematical programming and random projections, Mathematical programming: Turing completeness and applications to software analysis, Constraint qualification failure in action, Improving Strategies via SMT Solving

Uses Software

• CPLEX
• Bonmin
• FEASPUMP
• ROSE

Cites Work

• Unnamed Item
• Unnamed Item
• A new polynomial-time algorithm for linear programming
• An algorithmic framework for convex mixed integer nonlinear programs
• A feasibility pump for mixed integer nonlinear programs
• Foundations of computational intelligence. Volume 3: Global optimization
• Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs
• A lattice-theoretical fixpoint theorem and its applications
• Branching and bounds tighteningtechniques for non-convex MINLP
• Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
• Precise Relational Invariants Through Strategy Iteration
• Reformulations in Mathematical Programming: Definitions and Systematics
• Polynomial Precise Interval Analysis Revisited
• Preprocessing and Probing Techniques for Mixed Integer Programming Problems
• Automatic modular abstractions for linear constraints
• Abstract Interpretation Frameworks
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration
• Computer Aided Verification