Title: Proofs of protocols using logic programming
by Laurent Fribourg

Abstract: In order to model concurrent systems whose resources (channels, messages, clocks, parameters,...)
may take an illimited number of values, it is natural to consider extended forms of finite-state automata.
Two main methods emerged these latter years for analysing such infinite-state models. The first method, called ``symbolic model-checking'', defined suitable classes of extended automata (timed automata, hybrid systems,...) and developed specific analysis tools (HyTech, Kronos, Uppaal, Polka,...). The second method, called ``deductive-algorithmic method'', consists in integrating decision procedures, based on finite-state model-checking, into general theorems provers (PVS, SteP, ...).

On the other hand, pursuing the same goal of infinite-state systems verification, several researchers recently explored the use of tools originating from logic programming with constraints (XSB, CLP(R), 2lp, Datalog with gap-constraints,...). In this tutorial, I will compare such a logic-programming based approach to the symbolic model-checking and deductive-algorithmic methods, by considering concrete examples of industrial protocol telecommunications. I will try to point out the merits and shortcomings of logic programming methods, and indicate some prospects.