A DECISION PROCEDURE FOR THE FIRST ORDER THEORY OF REAL ADDITION WITH ORDER.FERRANTE J; RACKOFF C.1975; S.I.A.M. J. COMPUTG; U.S.A.; DA. 1975; VOL. 4; NO 1; PP. 69-76; BIBL. 5 REF.Article

REMARKS ON RECURSION VERSUS DIAGONALIZATION AND EXPONENTIALLY DIFFICULT PROBLEMSMACHTEY M; YOUNG P.1981; J. COMPUT. SYST. SCI.; ISSN 0022-0000; USA; DA. 1981; VOL. 22; NO 3; PP. 442-453; BIBL. 9 REF.Article

A 2^22PN UPPER BOUND ON THE COMPLEXITY OF PRESBURGER ARITHMETICOPPEN DC.1978; J. COMPUTER SYST. SCI.; USA; DA. 1978; VOL. 16; NO 3; PP. 323-332; BIBL. 7 REF.Article

Quantifier elimination for modules with scalar variablesVAN DEN DRIES, L; HOLLY, J.Annals of pure and applied logic. 1992, Vol 57, Num 2, pp 161-179, issn 0168-0072Article

Computing Affine Hulls over Q and Z from Sets Represented by Number Decision DiagramsLATOUR, Louis.Lecture notes in computer science. 2006, pp 213-224, issn 0302-9743, isbn 3-540-31023-1, 1Vol, 12 p.Conference Paper

On the convergence of population protocols when population goes to infinityBOURNEZ, Olivier; CHASSAING, Philippe; COHEN, Johanne et al.Applied mathematics and computation. 2009, Vol 215, Num 4, pp 1340-1350, issn 0096-3003, 11 p.Conference Paper

Verifying and reflecting quantifier elimination for presburger arithmeticCHAIEB, Amine; NIPKOW, Tobias.Lecture notes in computer science. 2005, pp 367-380, issn 0302-9743, isbn 3-540-30553-X, 1Vol, 14 p.Conference Paper

Theories of initial segments of standard models of arithmetics and their complete extensionsKRYNICKI, Michał; TOMASIK, Jerzy; ZDANOWSKI, Konrad et al.Theoretical computer science. 2011, Vol 412, Num 31, pp 3975-3991, issn 0304-3975, 17 p.Article

FAST extended releaseBARDIN, Sébastien; LEROUX, Jérome; POINT, Gérald et al.Lecture notes in computer science. 2006, pp 63-66, issn 0302-9743, isbn 3-540-37406-X, 1Vol, 4 p.Conference Paper

Structural Presburger digit vector automataLEROUX, Jérome.Theoretical computer science. 2008, Vol 409, Num 3, pp 549-556, issn 0304-3975, 8 p.Article

Vector Addition System Reachability Problem: A Short Self-Contained ProofLEROUX, Jérôme.ACM SIGPLAN notices. 2011, Vol 46, Num 1, pp 307-316, issn 1523-2867, 10 p.Conference Paper

What's decidable about arrays?BRADLEY, Aaron R; MANNA, Zohar; SIPMA, Henny B et al.Lecture notes in computer science. 2006, pp 427-442, issn 0302-9743, isbn 3-540-31139-4, 1Vol, 16 p.Conference Paper

Deciding Presburger arithmetic by model checking and comparisons with other methodsGANESH, Vijay; BEREZIN, Sergey; DILL, David L et al.Lecture notes in computer science. 2002, pp 171-186, issn 0302-9743, isbn 3-540-00116-6, 16 p.Conference Paper

Presburger modal logic is PSPACE-completeDEMRI, Stéphane; LUGIEZ, Denis.Lecture notes in computer science. 2006, pp 541-556, issn 0302-9743, isbn 3-540-37187-7, 1Vol, 16 p.Conference Paper

Decision procedures for recursive data structures with integer constraintsTING ZHANG; SIPMA, Henny B; MANNA, Zohar et al.Lecture notes in computer science. 2004, pp 152-167, issn 0302-9743, isbn 3-540-22345-2, 16 p.Conference Paper

Cache behavior analysis of a compiler-assisted cache replacement policyXINGYAN TIAN; KEJIA ZHAO; HUOWANG CHEN et al.Lecture notes in computer science. 2004, pp 30-43, issn 0302-9743, isbn 3-540-23003-3, 14 p.Conference Paper

On the automata size for presburger arithmeticKLAEDTKE, Felix.Symposium on Logic in Computer Science. 2004, pp 110-119, isbn 0-7695-2192-4, 1Vol, 10 p.Conference Paper

The commutative closure of a binary slip-language is context-free: a new proofRIGO, Michel.Discrete applied mathematics. 2003, Vol 131, Num 3, pp 665-672, issn 0166-218X, 8 p.Article

Memory optimization by counting points in integer transformations of parametric polytopesSEGHIR, Rachid; LOECHNER, Vincent.International Conference on Compilers, Architectures, and Synthesis for Embedded Systems. 2006, pp 74-82, isbn 1-59593-543-6, 1Vol, 9 p.Conference Paper

Decision procedures for queues with integer constraintsTING ZHANG; SIPMA, Henny B; MANNA, Zohar et al.Lecture notes in computer science. 2005, pp 225-237, issn 0302-9743, isbn 3-540-30495-9, 1Vol, 13 p.Conference Paper

DECIDING WHETHER A RELATION DEFINED IN PRESBURGER LOGIC CAN BE DEFINED IN WEAKER LOGICSCHOFFRUT, Christian.Informatique théorique et applications (Imprimé). 2008, Vol 42, Num 1, pp 121-135, issn 0988-3754, 15 p.Article

L'arbre de la complexité : Les problèmes difficiles en mathématiquesRecherche (Paris, 1970). 2007, Num 407, pp 40-41, issn 0029-5671, 2 p.Article

Verifying mixed real-integer quantifier eliminationCHAIEB, Amine.Lecture notes in computer science. 2006, pp 528-540, issn 0302-9743, isbn 3-540-37187-7, 1Vol, 13 p.Conference Paper

Multitree automata that countLUGIEZ, Denis.Theoretical computer science. 2005, Vol 333, Num 1-2, pp 225-263, issn 0304-3975, 39 p.Conference Paper

Memory usage verification for OO programsCHIN, Wei-Ngan; HUU HAI NGUYEN; SHENGCHAO QIN et al.Lecture notes in computer science. 2005, pp 70-86, issn 0302-9743, isbn 3-540-28584-9, 17 p.Conference Paper