Aspic swMATH ID: 4954 Software Authors: Gonnord, Laure; Halbwachs, Nicolas Description: 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. Homepage: http://laure.gonnord.org/pro/aspic/aspic.html Related Software: ASTREE; FAST; Apron; z3; FLATA; HyTech; Coq; LUSTRE; SPEED; Octagon; Yices; ABC; Interproc; CORA; HyLAA; Flow*; HySon; C2e2; STRONG; SpaceEx Cited in: 24 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Combining widening and acceleration in linear relation analysis. Zbl 1225.68071Gonnord, Laure; Halbwachs, Nicolas 2006 all top 5 Cited by 48 Authors 3 Jeannet, Bertrand 3 Monniaux, David P. 3 Schrammel, Peter 2 Bouissou, Olivier 2 Chapoutot, Alexandre 2 Gawlitza, Thomas Martin 2 Gonnord, Laure 2 Halbwachs, Nicolas 2 Maisonneuve, Vivien 2 Seladji, Yassamine 1 Abate, Alessandro 1 Alias, Christophe 1 Amato, Gianluca 1 Boutonnet, Rémy 1 Bozga, Marius 1 Brauer, Jörg 1 Brockschmidt, Marc 1 Cattaruzza, Dario 1 Cyphert, John 1 Darte, Alain 1 Di Nardo Di Maio, Simone 1 Falke, Stephan 1 Feautrier, Paul 1 Frohn, Florian 1 Garoche, Pierre-Loïc 1 Giesl, Jürgen 1 Girault, Alain 1 Hensel, Jera 1 Hermant, Olivier 1 Iosif, Radu 1 Irigoin, François 1 Kapur, Deepak 1 Kincaid, Zachary 1 King, Andy 1 Kröning, Daniel 1 Lakhdar-Chaouch, Lies 1 Massé, Damien 1 Meo, Maria Chiara 1 Naaf, Matthias 1 Perarnau, Swann 1 Prakken, Henry 1 Reps, Thomas W. 1 Roux, Pierre 1 Schulze Frielinghaus, Stefan 1 Scozzari, Francesca 1 Seidl, Helmut 1 Sinz, Carsten 1 Vogler, Ralf Cited in 5 Serials 3 Formal Methods in System Design 3 Logical Methods in Computer Science 2 Journal of Symbolic Computation 2 Journal of Automated Reasoning 1 Acta Informatica Cited in 5 Fields 24 Computer science (68-XX) 4 Numerical analysis (65-XX) 1 Mathematical logic and foundations (03-XX) 1 Operations research, mathematical programming (90-XX) 1 Systems theory; control (93-XX) Citations by Year