Computing invariants with transformers: experimental scalability and accuracy. (English) Zbl 1337.68168

Simon, Axel (ed.) et al., Proceedings of the 5th international workshop on numerical and symbolic abstract domains, NSAD 2014, Munich, Germany, September 10, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 307, 17-31, electronic only (2014).
Summary: Using abstract interpretation, invariants are usually obtained by solving iteratively a system of equations linking preconditions according to program statements. However, it is also possible to abstract first the statements as transformers, and then propagate the preconditions using the transformers. The second approach is modular because procedures and loops can be abstracted once and for all, avoiding an iterative resolution over the call graph and all the control flow graphs.
However, the transformer approach based on polyhedral abstract domains encurs two penalties: some invariant accuracy may be lost when computing transformers, and the execution time may increase exponentially because the dimension of a transformer is twice the dimension of a precondition.
The purposes of this article are 1) to measure the benefits of the modular approach and its drawbacks in terms of execution time and accuracy using significant examples and a newly developed benchmark for loop invariant analysis, ALICe, 2) to present a new technique designed to reduce the accuracy loss when computing transformers, 3) to evaluate experimentally the accuracy gains this new technique and other previously discussed ones provide with ALICe test cases and 4) to compare the executions times and accuracies of different tools, ASPIC, ISL, PAGAI and PIPS.
Our results suggest that the transformer-based approach used in PIPS, once improved with transformer lists, is as accurate as the other tools when dealing with the ALICe benchmark. Its modularity nevertheless leads to shorter execution times when dealing with nested loops and procedure calls found in real applications.
For the entire collection see [Zbl 1310.68020].


68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)


isl; ALICe; Aspic; Omega; PAGAI
Full Text: DOI


[1] Ammarguellat, Z., A control-flow normalization algorithm and its complexity, IEEE Trans. Software Eng., 18, 237-251, (1992)
[2] C. Ancourt, F. Coelho, F. Irigoin, A modular static analysis approach to affine loop invariants detection (2010), pp. 3-16, NSAD, 2010. · Zbl 1342.68065
[3] Ancourt, C.; Coelho, F.; Irigoin, F., A modular static analysis approach to affine loop invariants detection (extended version), (2010), MINES ParisTech, CRI, Technical Report A-419 · Zbl 1342.68065
[4] Bielecki, W.; Kraska, K.; Klimek, T., Transitive closure of a union of dependence relations for parameterized perfectly-nested loops, (Parallel Computing Technologies, (2013)), 37-50
[5] Bourdoncle, F., Sémantiques des langages d’ordre supérieur et interprétation abstraite, (1992), École polytechnique, Ph.D. thesis
[6] Bultan, T.; Gerber, R.; Pugh, W., Symbolic model checking of infinite state systems using Presburger arithmetic, (Computer Aided Verification, (1997)), 400-411
[7] Dillig, I.; Dillig, T.; Li, B.; McMillan, K., Inductive invariant generation via abductive inference, (OOPSLA ’13, (2013)), 443-456
[8] Feautrier, P.; Gonnord, L., Accelerated invariant generation for C programs with aspic and c2fsm, Electron. Notes Theor. Comput. Sci., 267, 3-13, (2010)
[9] Gonnord, L.; Halbwachs, N., Combining widening and acceleration in linear relation analysis, (Yi, K., Static Analysis, Lecture Notes in Computer Science, vol. 4134, (2006)), 144-160 · Zbl 1225.68071
[10] Gulavani, B. S.; Henzinger, T. A.; Kannan, Y.; Nori, A. V.; Rajamani, S. K., Synergy: A new algorithm for property checking, (SIGSOFT ’06, (2006)), 117-127
[11] Gulwani, S.; Zuleger, F., The reachability-bound problem, (Zorn, B. G.; Aiken, A., PLDI, (2010)), 292-304
[12] Halbwachs, N.; Henry, J., When the decreasing sequence fails, (SAS, (2012)), 198-213
[13] Henry, J.; Monniaux, D.; Moy, M., Pagai: A path sensitive static analyser, Electron. Notes Theor. Comput. Sci., 289, 15-25, (2012)
[14] Irigoin, F., Interprocedural analyses for programming environments, (Environments and Tools for Parallel Scientific Computing, (1993)), 333-350
[15] Irigoin, F.; Jouvelot, P.; Triolet, R., Semantical interprocedural parallelization: an overview of the PIPS project, (ICS ’91, (1991)), 244-251
[16] Khaldi, D., Automatic resource-constrained static task parallelization, (2013), MINES ParisTech, Ph.D. thesis
[17] V. Maisonneuve, Convex invariant refinement by control node splitting: a heuristic approach (2012), NSAD, pp. 49-59, 2011. · Zbl 1294.68059
[18] V. Maisonneuve, O. Hermant, F. Irigoin, ALICe: A framework to improve affine loop invariant computation, 2014, 5th Workshop on INvariant Generation.
[19] Maisonneuve, V.; Hermant, O.; Irigoin, F., Alice: A framework to improve affine loop invariant computation, (2014), MINES ParisTech, CRI, Technical Report A-559
[20] D. Massé, Policy iteration-based conditional termination and ranking functions, VMCAI, 2014, pp. 453-471. · Zbl 1428.68125
[21] Nguyen, T. V.N.; Irigoin, F., Efficient and effective array bound checking, ACM Trans. Program. Lang. Syst., 27, 527-570, (2005)
[22] Popeea, C.; Chin, W.-N., Inferring disjunctive postconditions, (ASIAN’06, (2007)), 331-345
[23] Pugh, W., The omega library
[24] Verdoolaege, S., ISL: an integer set library for the polyhedral model, (2010) · Zbl 1294.68166
[25] Verdoolaege, S.; Cohen, A.; Beletska, A., Transitive closures of affine integer tuple relations and their overapproximations, (SAS’11, (2011)), 216-232
[26] Wonnacott, D., Extending scalar optimizations for arrays, (Languages and Compilers for Parallel Computing, (2001)), 97-111 · Zbl 1014.68680
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.