ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| MODELLI DI CALCOLO | INF/01 | LEZIONI | 72 |
|
Students are expected to acquire solid knowledge about the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Moreover, they will acquire some knowledge about the operational and observational semantics of two process description languages (CCS and pi-calculus), about temporal and modal logics (HM, LTL, CTL*, mu-calculus) and operational nondeterministic models with discrete probabilities. The latter are presented from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.
In the written exam the student must demonstrate his/her knowledge of the course material and to organise an effective and correctly written reply. During the oral exam the student must be able to demonstrate his/her knowledge of the course material and be able to discuss the reading matter thoughtfully and with propriety of expression.
Methods:
Further information:
The evaluation will be based on written and oral exams. The written exam is not necessary if the mid-terms exams are evaluated positively.
At the end of the course the student should be able to state and prove formal properties of imperative, declaratice, concurrent and probabilistic systems. In particular, they should be able to apply several induction principles and fixpoint theory.
The written exam consists of exercises that require to apply formal analysis techniques to some carefully chosen cases.
The oral exam focuses on the definitions and properties presented in the course.
At the end of the course the student should be able to understand logic systems and inductive definitions, to assign semantics to programs, to reason about program equivalence and compliance to abstract specifications.
Written and oral exam.
There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, first-order logic formulas, context-free grammars, and code fragments in imperative and functional style.
None
Some topics in the course can be useful for attending the courses on
Delivery: face to face
Learning activities:
Attendance: Advised
Teaching methods:
The introduction of five different computational models (imperative: IMP, functional: HOFL, processes: CCS, nominal: pi-calculus, probabilistic and stochastic: Segala automata and PEPA) together with induction principles and formal proof methods.
Main text:
Other readings:
No variation.
Written (two mid-term, or one regular) exam and oral exam.
The written exam consists of a series of exercises to be solved in 2 hours. Each exercise is assigned some score and the overal score is the sum of scores for each exercise. The texts of exams from previous sessions and academic years are linked from the web page of the course.
The oral exam can involve the discussion of the written exam as well as questions about the main topics of the course topics. The average duration of the oral exam is 40'
None
http://didawiki.di.unipi.it/doku.php/magistraleinformatica/mod/start
Some teaching tools overviewed in the course are:
None
