Improving the results of program analysis by abstract interpretation beyond the decreasing sequence

DOI10.1007/s10703-017-0310-yzbMath1425.68064OpenAlexW4289233987MaRDI QIDQ1620957

Rémy Boutonnet, Nicolas Halbwachs

Publication date: 15 November 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0310-y

zbMATH Keywords

program analysisabstract interpretationfixpoint approximationfixpoint improvementwidening/narrowing

Mathematics Subject Classification ID

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

Related Items

Decoupling the ascending and descending phases in abstract interpretation

Uses Software

• Apron
• LLVM
• Dagger
• Aspic
• PPL
• ASTREE
• FAST

Cites Work

• Widening and narrowing operators for abstract interpretation
• Program Analysis with Local Policy Iteration
• Widening with Thresholds for Programs with Complex Control Graphs
• Guided Static Analysis
• Combining Widening and Acceleration in Linear Relation Analysis
• A Linear Time Algorithm for Finding Minimum Cutsets in Reducible Graphs
• Stratified Static Analysis Based on Variable Dependencies
• Abstracting Induction by Extrapolation and Interpolation
• Numerical Software with Result Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Widening Polyhedra with Landmarks
• Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
• Automatically Refining Abstract Interpretations
• Static Analysis
• Depth-First Search and Linear Graph Algorithms
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Precise Fixpoint Computation Through Strategy Iteration
• Tools and Algorithms for the Construction and Analysis of Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item