*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                             Salle R, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 27 avril 2001 **** 14h00 *******************************

Paritosh K. PANDYA (Tata Institute of Fundamental Research)

Model Checking Duration Calculus

Re'sume' : Duration Calculus is a form of Interval Temporal Logic where
assertions describe behaviour as seen from a time interval.  Duration
of a proposition measures the amount of time for which the proposition
holds in a time interval. Using these notions, Duration Calculus
provides a novel and highly expressive formalism for specifying
complex timing requirements.  Duration Calculus has been used to
reason about requirements of real-time systems. It has also been used
to give compositional semantics of notations like Esterel and Timed
CSP.

In this talk we will describe our attempts at model checking Duration
Calculus formulae. For discrete time, an automata theoretic decision
procedure has been implemented into a tool called DCVALID. The tool
has been integrated with model checkers SMV, VIS and XEVE to allow
complex timing properties of SMV, Verilog and Esterel programs to be
checked.  We will also touch upon logic LIDL, a variant of dense time
Duration Calculus, whose models can be represented as timed words
accepted by integrator automata. Its subset LIDL- has been shown to
have exactly the expressive power of event recording automata.

*** Vendredi 27 avril 2001 **** 16h00 *******************************

Fred MESNARD (IREMIA/GCC, Universite de La Reunion)

Inferring termination conditions for logic programs 

Re'sume' : We present the theoretical framework and the implementation
of cTI, a system for universal left-termination inference of logic
programs.

Termination inference generalizes termination analysis/checking.  
Traditionally, a termination analyzer tries to prove that a given class
of queries terminates. This class must be provided to the system, 
requiring user annotations. With termination inference such annotations
are no longer necessary.  Instead, all provably terminating classes to 
all related predicates are inferred at once.
  
The architecture of cTI is described and some optimizations are 
discussed.  Running times for classical examples from  the termination 
literature in LP and for some middle-sized logic programs are given.
An approach for optimality detection is sketched.

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************