Qualification and title awarded – Licenciatura in Computer Science, Licenciado

Regime: S2

2 hours/week - lectures. 3 hours/week - examples classes.

Programa:

Introduction and basic concepts. Axiomatic theory. Random variables, random vectors and probability distributions (discrete, continuous and others). Moments, probability inequalities, moment-generating functions and characteristic functions. Univariate and mulivariate parametric families. Functions of random variables. The normal model and special properties. Related models. Limit laws. Central Limit Theorem and Laws of Large Numbers. Computational simulation (along the course).

Métodos de Avaliação:

Periodic assessment / Final written examination.

One individual laboratorial work (worthing 45%), one individual theoretical and practical work in a computational laboratory (worthing 45%) plus two or three practical works (worthing 10%)
Pré-requisitos:

Real Analysis. Imperative programming. Basic knowledge of any algebraic software.

Resultados de Aprendizagem:

1. 
   Understand and be able to apply basic concepts of probability probabilistic fundamental results.
   
2. 
   Be familiar with several probability parametric models (discrete and continuous, univariate e multivariate) and related asymptotic results.
   
3. 
   Be familiar with some stochastic simulation techniques.
   
4. 
   To know and to apply several limit laws.
   
5. 
   Be able to use appropriate software to problem solving.
   

Pestana, D. , Velosa, S. -  Introdução à probabilidade e à estatística, Fundação Caloustre Gulbenkian, 2002

Docentes:

Processes and Concurrency

Regime: S6

Tipo: Compulsory

Língua de Instrução: Portuguese

Carga Total: 56

Créditos: 5

Métodos de Ensino:

Lectures and problem solving classes.

Programa:

Petri Nets:

- Modeling concurrent systems with Petri nets.

- Operational semantics based on transitition systems.

- Fundamental net properties: boundedness, liveness, reversibility.

- Determining place invariants.

- Extensions to standard nets: places with explicity capacity and inhibitor arcs.

- Tools for specification and animation of Petri nets (DaNAMiCS, PIPE).

Temporal Logic:

- Specification of safety and liveness properties with the temporal logic CTL.

- Explicit model checking of CTL formulas.

- Symbolic model checking of CTL formulas using OBDDs.

- Tools for symbolic model checking (SMV).

Process Algebra:

- Automata and transition systems. Interaction and behaviour.

- Modeling reactive systems with CCS. Operational semantics. Analysis and verification of transitions.

- Calculating reactive systems. Strict and observational equivalence in CCS. Expansion theorem. Equation solving.

- Calculating mobile systems. Motivation, syntax, semantics and equivalence between mobile processes.

- Animation and process analysis using CWB and MWB.

Métodos de Avaliação:

Individual exams.

Pré-requisitos:

Basic knowledge of concurrent programming and discrete mathematics.

Resultados de Aprendizagem:

- Understand and compare different models and languages for the specification of concurrent systems.

- Model concurrent systems of small/medium complexity using Petri nets.

- Specify safety and liveness properties using temporal logic.

- Understand and compare different verification techniques for temporal logic.

- Use tools to verify properties of concurrent systems.

- Model concurrent and mobile systems of small/medium complexity using process algebras.

- Reason about concurrent and mobile systems of small/medium complexity using process algebras.

Bibliografia:

- Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Claude Girault and Rüdiger Valk (editors). Springer-Verlag, 2003.

- Elements of Distributed Algorithms: modeling and analysis with petri nets. Wolfgang Reisig. Springer-Verlag, 1998.

- Model Checking. Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. MIT Press, 2001.

- Communicating and mobile systems: the pi calculus. Robin Milner. Cambridge University Press, 1999.

- The pi calculus: A Theory of Mobile Processes. D. Sangiorgi, D. Walker. Cambridge University Press, 2001.

- Reactive Systems: Modelling, Specification and Verification. Luca Aceto, A.Ingólfsdóttir, Kim Larsen, J. Srba. Cambridge University Press, 2007.

Docentes:

Manuel Alcino Cunha

Luís Soares Barbosa

8506N3 - Semantics of Programming Languages

Regime: S2

Tipo: Mandatory

Língua de Instrução: Portuguese

Horas/Semana: 56

Créditos: 5

Métodos de Ensino:

Lectures and problem solving classes.

Programa:

1. Introduction. Syntax and semantics. Operational,

denotational and axiomatics semantics.

2. Definition and proof by induction.

3. Introduction to the operational semantics of an imperative language.

4. Introduction to denotational semantics and domain theory.

5. Semantic equivalence for imperative languages.

6. Operational and denotational semantics of a functional language.

Métodos de Avaliação:

Individual tests.

Pré-requisitos:

Basic knowledge of programming and discrete mathematics.

Resultados de Aprendizagem:

- Understand and compare different methods and techniques for modelling

programming languages, their foundations and applications.

- Use such techniques and methods in the specification of concrete programming

languages as well as in the verification of semantic equivalences.

Bibliografia:

- G. Winskel. The formal semantics of programming languages. MIT Press. 1993.

- M. Hennessy. The semantics of programming languages. Wiley. 1990.

- B. Pierce. Types and programming languages}. MIT Press. 2000.

- T. Streicher. Domain-theorectic foundations of functional programs.

World Scientific. 2006.

Docentes:

Luís Soares Barbosa