Formal verification of concurrent and reactive systems is necessary for many modern critical applications.

The Timed Concurrent Constraint Language (tccp in short) is a simple but powerful model for concurrent and reactive systems. In this language the notion of time is modeled by a global and discrete clock and the information on system variables is handled by an underlying constraint system.

The existing formal techniques for the verification of tccp are based on model checking, which suffers the well known state-explosion problem.

Abstract interpretation is an alternative to model checking: it is a theory of sound semantic approximation proposed with the aim of providing a general framework for analysis, verification and debugging of systems.

In this talk, I present a semantic framework for tccp based on abstract interpretation with the purpose of formally verifying and debugging tccp programs.

The key point for the efficacy of the proposed methodology is the adequacy of the underlying concrete semantics which models precisely the small-step behavior of tccp and is suitable to be used in the abstract interpretation framework.

The main idea behind my approach is to approximate this concrete semantics into suitable abstract domains in order to obtain effectiveness and efficiency at the price of losing some precision in the results.

More specifically, I present two different abstract domains: the first one approximates the information content of tccp behavioral traces, while the second one approximates the small-step semantics with temporal logic formulas.