Università degli Studi di Urbino Carlo Bo / Portale Web di Ateneo


A.Y. Credits
2016/2017 12
Lecturer Email Office hours for students
Alessandro Aldini wednesday 11-13 lecturer office
Teaching in foreign languages
Course with online activities entirely in a foreign language English
For this course offered in face-to-face/online mixed mode, online teaching is entirely in a foreign language and the final exam can be taken in the foreign language.

Assigned to the Degree Course

Applied Informatics (L-31)
Giorno Orario Aula

Learning Objectives

The objective of this course is to introduce the theory of formal languages and to illustrate techniques for modeling the architecture of complex software systems and verifying their properties by means of formal methods based on automata, algebra, and logics.


01. Introduction to modeling and verification:
      01.01 The need for formal methods in software development.
      01.02 Formal languages and automata.
      01.03 Grammars and Chomsky classification.
      01.04 Formal approaches to language semantics.
      01.05 Concurrency theory, logics, and algebra.

02. Regular languages and finite-state automata:
      02.01 Deterministic finite-state automata.
      02.02 Nondeterministic finite-state automata.
      02.03 Nondeterministic finite-state automata with epsilon-transitions.
      02.04 Minimization and equivalence for finite-state automata.
      02.05 Finite-state automata and linear grammars.
      02.06 Closure properties of regular languages and pumping lemma.
      02.07 Regular expressions.
      02.08 Regular expressions and finite-state automata.

03. Context-free languages and pushdown automata:
      03.01 Free grammars and syntax trees.
      03.02 Chomsky normal form.
      03.03 Properties of context-free languages.
      03.04 Pushdown automata and relation with free grammars.
      03.05 Top-down parsing.
      03.06 Bottom-up parsing.

04. Denotational semantics:
      04.01 Denotational semantics for an imperative language.
      04.02 Denotational semantics for an imperative language with blocks and procedures.

05. Operational semantics:
      05.01 Natural semantics for an imperative language.
      05.02 Natural semantics for an imperative language with blocks and procedures.
      05.03 Structural operational semantics for an imperative language.

06. Temporal logics and model checking:
      06.01 Kripke models.
      06.02 Temporal logics.
      06.03 Linear-time logics vs. branching-time logics.
      06.04 Model checking algorithms.

07. Process algebra and behavioral equivalences:
      07.01 Concurrency and nondeterminism.
      07.02 Syntax and semantics of behavioral operators.
      07.03 Trace based equivalence.
      07.04 Bisimulation based equivalence.

08. Languages for the specification of software architectures:
      08.01 Components, connectors, and architectural styles.
      08.02 Syntax of an architectural language based on process algebra.
      08.03 Semantics of an architectural language based on process algebra.

09. Laboratory activity:
      09.01 Specification of systems through Kripke models.
      09.02 Model checking of systems specified through Kripke models.
      09.03 Specification of systems through architectural languages.
      09.04 Equivalence and model checking of systems specified through architectural languages.

Bridging Courses

Although there are no mandatory prerequisites for this exam, students are strongly recommended to take it after Procedural and Logic Programming, Computer Architecture, Discrete Structures and Linear Algebra.

Learning Achievements (Dublin Descriptors)

Knowledge and understanding: the student will be able to understand the semantics of the most used programming languages and the methodological principles behind the formal methods for design and verification of software systems that are illustrated in the program.

Applying knowledge and understanding: the student will be able to design the base modules of the compilers for programming languages and to specify and verify formally software systems through the tools used in the classrooms.

Making judgements: the student will be able to evaluate the correctness of syntax and semantics of any programming language and to represent and compare formally the several specifications of a software system under design and development.

Communication skills: the student will be able to illustrate in a proper way the semantic features of the programming languages and to describe formally the functionalities and the properties of a software system by using the modeling and verification tools used in the classrooms.

Learning skills: the student will learn how to describe formally syntax and semantics of programming languages and how to model and check software systems.

Teaching Material

The teaching material prepared by the lecturer in addition to recommended textbooks (such as for instance slides, lecture notes, exercises, bibliography) and communications from the lecturer specific to the course can be found inside the Moodle platform › blended.uniurb.it

Didactics, Attendance, Course Books and Assessment


Theory lectures and laboratory exercises, both face-to-face and on-line.


Although recommended, course attendance is not mandatory.

Course books

Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità", Addison-Wesley, 2009
Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, 2007).
Nielson, Nielson, "Semantics with Applications: An Appetizer", Springer, 2007
Clarke, Grumberg, Peled, "Model Checking", MIT Press, 1999
Aldini, Bernardo, Corradini, "A Process Algebraic Approach to Software Architecture Design", Springer, 2010


Individual project, written exam, and oral exam.

The individual project consists of modeling and verifying a software system. The project specification, one per session and the same for everybody, is published online at least one month before the beginning of every session, with delivery deadline by the noon of two days before the date of the written exam of interest. The project, even if passed, is valid only within the related session. The project text is given by the specification of a real system to model and verify. The student can freely choose the software tool to use, the abstraction level of the system, the variants and configurations under analysis, and the properties to verify. Delivery is by email with subject LPVS: consegna progetto name_surname and must include source files with specifications and analysis results, each part adequately commented. The project mark is at most 10/30.

The written exam can be given only after the delivery of the project related to the same session. Its duration is 90 minutes and it consists of practical exercises. Notes and didactical material can be used. The written exam mark is at most 20/30. In the winter session a partial written exam can be given to be integrated with another partial written exam in the summer session. In such a case, the two written exams are associated with the project of the summer session.

The oral exam is mandatory about the individual project and is optional about the course program. The optional oral exam yields a positive or negative adjustment (at most 5 points) to the final mark.

For texts of projects and written exams, see this link.


The course is offered also on-line inside the Moodle platform > elearning.uniurb.it

« back Last update: 05/06/17


Questo contenuto ha risposto alla tua domanda?

Il tuo feedback è importante

Raccontaci la tua esperienza e aiutaci a migliorare questa pagina.

Il tuo 5x1000 per sostenere le attività di ricerca

L'Università di Urbino destina tutte le risorse che deriveranno da questa iniziativa alla ricerca scientifica ed al sostegno di giovani ricercatori.

Numero Verde

800 46 24 46

Richiesta informazioni


Posta elettronica certificata



Performance della pagina

Università degli Studi di Urbino Carlo Bo
Via Aurelio Saffi, 2 – 61029 Urbino PU – IT
Partita IVA 00448830414 – Codice Fiscale 82002850418
2019 © Tutti i diritti sono riservati