Sign In

Courses 2006

Sort by AttachmentsUse SHIFT+ENTER to open the menu (new window).
Title Model Checking
Teacher Enrico Tronci, Dipartimento di Informatica, Università di Roma "La Sapienza"
Period February 2-24
  1. Sistemi Ibridi: HyTech (3h)
  2. Algoritmi di Model Checking Esplicito: Murphi, SPIN. (3h).
  3. Model Checking Simbolico:
    • OBDDs (2h)
    • CTL (2h)
    • mu-calculus via OBDDs (2h)
    • SMV, VIS (2h)
  4. Bounded Model Checking: bmc, SAT, zchaff (2h)
  5. Probabilistic Model Checking: PRISM, FHP-Murphi (2h)
  6. Software Model Checking: Survey (2h), CMC (2h).
  7. Counterexample Guided Abstraction Refinement (2h).
Title Interpretazione astratta per l'analisi e la verifica di linguaggi dichiarativi
Teacher Prof. Giorgio Levi, Dipartimento di Informatica, Università di Pisa
Period April 4-27
  1. Introduzione all'interpretazione astratta
  2. Inferenza dei tipi via interpretazione astratta
  3. Programmazione logica: semantica e analisi
  4. Verifica via interpretazione astratta
  5. Operatori di raffinamento

Title Categorical structures for system modelling
Teacher Jose Luiz Fiadeiro, Professor of Software Science and Engineering, Department of Computer Science - University of Leicester
Period May
The focus of this series of lectures is the support that category theory can bring to the modelling of complex software systems. It consists of an introduction to basic and more advanced categorical concepts and techniques using examples drawn from concurrency theory, algebraic specification (namely institutions) and software architecture (the language CommUnity). Our ambition is to show how category theory can provide a unifying, truly 'universal' approach to the handling of different levels of complexity that arise in the development of large and interaction-intensive systems. The course will be supported by the book "Categories for Software Engineering", Springer 20 (
Title Logica per l’informatica
Teacher Andrea Masini, Dipartimento di Informatica, Università di Verona
Period First two weeks of May
  • Logica Classica del I ordine:
    1. Sintassi e semantica;
    2. problemi di formalizzazione;
    3. deduzione naturale;
    4. correttezza e completezza;
  • 2) Logica Intuizionista:
    1. semantica;
    2. deduzione naturale;
    3. interpretazione BHK e teorie dei tipi;
  • Cenni ad altri sistemi deduttivi: sequenti, tableaux.

Title Computational Models based on Rewriting
Teacher Andrea Corradini, Fabio Gadducci, Dipartimento di Informatica, Università di Pisa
Period After mid May
Several computational models describe the evolution of systems using some rewriting mechanism: a set of rules is given, and a system moves from one state to the next one by applying a rule.
Depending on the structure of the states, such formalisms are presented with different names (Chomsky grammars, Petri nets, term rewriting systems, graph grammars,...) and a rich body of literature has been developed for each of them.
The goal of the course is to introduce the basics of several of such computational models in a uniform way, stressing their similarities and highlighting their differences. Moving from simpler to more complex models, basic notions of universal algebra and of category theory will be introduced, as they will provide a more adequate language as well as useful proof techniques.
For the various formalisms introduced, the main application fields will be briefly surveyed.
A preliminary list of topics (to be further refined during the first lessons) includes:
  • Abstract rewriting systems: relational presentation, basic definitions (residuation and equivalence), termination, confluence
  • Term rewriting systems: algebraic presentation (terms, substitutions, unification) and equational reasoning (equational logic), basic definitions and results (validity and decidability), confluence (critical pairs, completion), permutation equivalence, proof terms
  • Petri Nets: multiset-presentation, basic definitions and results, termination, reachability, parallelism, processes
  • Graph rewriting systems: categorical presentation, basic definitions and results, parallelism, processes
    Applications: basic overview on the use of rewrite systems for the specification of concurrent and distributed systems
  • Verification: basic overview on the analysis techniques so far available for rewrite systems, and their use in applied case studies
    Tools: basic overview on the available tools (as the Java applets collected on


Title Il lambda calcolo parametrico: un meta-modello di computazione
Teacher Simona Ronchi della Rocca, Dipartimento di Informatica, Università degli Studi di Torino
Period First half of June
Il lambda calcolo parametrico è un calcolo paradigmatico, che può sussumere (oltre ad altri calcoli) sia il lambda calcolo classico che il lambda calcolo per valore di Plotkin. Può quindi essere studiato come modello per studiare in modo uniforme la semantica (operazionale e denotazionale) di diversi modelli di computazione.
Programma di massima:
  • La sintassi
  • Le proprieta' fondamentali: confluenza e standardizzazione
  • Solvability e separability
  • Le macchine di valutazione e la semantica operazionale
  • Alcune relazioni interessanti tra call-by-name e call-by-value
  • La semantica denotazionale
  • I tipi intersezione e i filtri modelli
  • Costruzione di filtri modelli
  • Il problema della full-abstraction.

S. Ronchi Della Rocca, L.Paolini, "The Parametric Lambda Calculus: a meta-model for Computation, Texts in Computer Science, Springer, 2004