Interuniversity Attraction Poles program MoVES of the Belgian Federal Science Policy Office Grant 2.4530.02 of the Belgian Fund for Scientific Research (F.R.S.-FNRS).
Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, Vol. 1102, pp. 1-12. Springer, Heidelberg (1996) (Pubitemid 126101265)
Bruyére, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and precognizable sets of integers. Bulletin of the Belgian Mathematical Society 1(2), 191-238 (1994)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, Vol. 1855, pp. 403-418. Springer, Heidelberg (2000)
Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic 6(3), 614-633 (2005) (Pubitemid 41092677)
Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. Theoretical Computer Science 313, 17-29 (2004)
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Liége, Belgium (1998)
Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: An overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, Vol. 2401, pp. 1-19. Springer, Heidelberg (2002)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Methodoloy and Philosophy of Science, pp. 1-12. Stanford University Press, Stanford (1962)
Couvreur, J.-M.: A BDD-like implementation of an automata package. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, Vol. 3317, pp. 310-311. Springer, Heidelberg (2005) (Pubitemid 41190898)
Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Theory of Machines and Computation, 189-196 (1971)
Latour, L.: Presburger Arithmetic: From Automata to Formulas. PhD thesis, University of Liége, Belgium (2005)
Leroux, J.: A polynomial time Presburger criterion and synthesis for number decision diagrams. In: Proc. 20th LICS, pp. 147-156. IEEE Computer Society, Los Alamitos (2005) (Pubitemid 41462562)
Oppen, D.C.: A 222pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences 16, 323-332 (1978)
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congrés des Mathématiciens des Pays Slaves, Warsaw, pp. 92-101 (1929)
Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of presburger engines for EFSM reachability. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, Vol. 1427, pp. 280-292. Springer, Heidelberg (1998) (Pubitemid 128092346)
Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Mycroft, A. (ed.) SAS 1995. LNCS, Vol. 983, pp. 21-32. Springer, Heidelberg (1995)
