Combining widening and acceleration in linear relation analysis. Linear Relation Analysis is one of the first, but still one of the most powerful, abstract interpretations working in an infinite lattice. As such, it makes use of a widening operator to enforce the convergence of fixpoint computations. While the approximation due to widening can be arbitrarily refined by delaying the application of widening, the analysis quickly becomes too expensive with the increase of delay. Previous attempts at improving the precision of widening are not completely satisfactory, since none of them is guaranteed to improve the precision of the result, and they can nevertheless increase the cost of the analysis. In this paper, we investigate an improvement of Linear Relation Analysis consisting in computing, when possible, the exact (abstract) effect of a loop. This technique is fully compatible with the use of widening, and whenever it applies, it improves both the precision and the performance of the analysis.

References in zbMATH (referenced in 24 articles , 1 standard article )

Showing results 1 to 20 of 24.
Sorted by year (citations)

1 2 next

  1. Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel: Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration (2021)
  2. Amato, Gianluca; Di Nardo Di Maio, Simone; Meo, Maria Chiara; Scozzari, Francesca: Descending chains and narrowing on template abstract domains (2018)
  3. Boutonnet, Rémy; Halbwachs, Nicolas: Improving the results of program analysis by abstract interpretation beyond the decreasing sequence (2018)
  4. Schulze Frielinghaus, Stefan; Seidl, Helmut; Vogler, Ralf: Enforcing termination of interprocedural analysis (2018)
  5. Frohn, F.; Naaf, M.; Hensel, J.; Brockschmidt, M.; Giesl, J.: Lower runtime bounds for integer programs (2016)
  6. Roux, Pierre; Garoche, Pierre-Loïc: Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case (2015)
  7. Maisonneuve, Vivien; Hermant, Olivier; Irigoin, François: Computing invariants with transformers: experimental scalability and accuracy (2014)
  8. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Acceleration of the abstract fixpoint computation in numerical program analysis (2012)
  9. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  10. Gawlitza, Thomas Martin; Monniaux, David: Invariant generation through strategy iteration in succinctly represented control flow graphs (2012)
  11. Maisonneuve, Vivien: Convex invariant refinement by control node splitting: a heuristic approach (2012)
  12. Massé, Damien: Proving termination by policy iteration (2012)
  13. Prakken, Henry: Some reflections on two current trends in formal argumentation (2012)
  14. Schrammel, Peter; Jeannet, Bertrand: Applying abstract acceleration to (co-)reachability analysis of reactive programs (2012)
  15. Falke, Stephan; Kapur, Deepak; Sinz, Carsten: Termination analysis of C programs using compiler intermediate languages (2011)
  16. Gawlitza, Thomas Martin; Monniaux, David: Improving strategies via SMT solving (2011)
  17. Lakhdar-Chaouch, Lies; Jeannet, Bertrand; Girault, Alain: Widening with thresholds for programs with complex control graphs (2011)
  18. Peña, Ricardo; Delgado-Muñoz, Agustin D.: Size invariant and ranking function synthesis in a functional language (2011) ioport
  19. Alias, Christophe; Darte, Alain; Feautrier, Paul; Gonnord, Laure: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs (2010)
  20. Bouissou, Olivier; Seladji, Yassamine; Chapoutot, Alexandre: Abstract fixpoint computations with numerical acceleration methods (2010)

1 2 next