Abstract FR:

Cette these se divise en deux parties: la premiere partie presente un modele permettant de representer des systemes concurrents parametres (c'est-a-dire, manipulant une quantite non bornee de donnees). On montrera dans cette premiere partie que le probleme de verification de proprietes de ces systemes se ramene a un probleme d'evaluation ascendante de programmes logiques. Dans la deuxieme partie, nous apportons une contribution au probleme du calcul du resultat de l'evaluation ascendante de programmes logiques avec des contraintes arithmetiques. Nous definissons une classe de programmes logiques sur des entiers dans laquelle le processus d'evaluation ascendante engendre toujours une formule arithmetique lineaire. Un programme appartenant a cette classe contient au plus trois regles recursives, qui possedent, chacune, un seul atome arithmetique dans le corps. Nous adoptons une approche geometrique pour construire le resultat du processus d'evaluation ascendante