This course aims to introduce the student to the principles and foundations of programming languages, in order to understand their structure and correctly interpret the behavior of programs. First of all, this goal is pursued through the study of the theory of formal languages, their syntax definition tools (through grammars and automata), and the formalization of their semantics. In the context of such formal tools, we address some techniques to model complex software systems and verify their properties through the use of methodologies based on automata and logics.

01. Foundations of programming languages:
      01.01 Theory of formal languages.
      01.02 Chomsky classification of sentential form grammars. 
      01.03 Theory of automata and Turing machines.
      01.04 Computability.

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 right-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 and pumping lemma.
      03.04 Pushdown automata and relation with free grammars.
      03.05 Top-down parsing.
      03.06 LL(1) grammars.
      03.07 Parsing bottom-up.
      03.08 SLR, LR(1), and LALR(1) grammars.

04. Denotational semantics:
      04.01 Denotational semantics for non-cyclic sequential programs.
      04.02 Denotational semantics for the WHILE operator.
      04.03 Denotational semantics with blocks and procedures.

05. Operational semantics:
      05.01 Natural semantics for sequential programs.
      05.02 Natural semantics with blocks and procedures.
      05.03 Structural operational semantics.

06. Modeling and verification of reactive systems:
      06.01 Kripke structures.
      06.02 Linear temporal logic.
      06.03 Computation tree logic.
      06.04 Model checking algorithms.

07. Laboratory activity:
      07.01 Finite state machines.
      07.02 Modeling and verification in NuSMV.
      07.03 Complex reactive systems in NuSMV.

Although there are no mandatory prerequisites for this exam, students are strongly recommended to take it after Object-Oriented Programming and Modeling, Software Architecture and Engineering, Operating Systems, by respecting the prerequisites of these courses.

Knowledge and understanding: the student will be able to understand the syntax structure, the compiler rules, and the semantics of the most used programming languages, as well as 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.

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

Teaching

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

Attendance

Although recommended, course attendance is not mandatory.

Course books

The two alternative books: Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità" (Terza Edizione, Pearson) and Aiello, Pirri, "Strutture, logica, linguaggi" (Pearson) cover the topics of sections 01-03. The original version of the former book is Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley.

Sections 04 and 05 are inspired by Nielson, Nielson, "Semantics with Applications: An Appetizer" (Springer).

The topics of section 06 are covered by Clarke, Grumberg, Peled, Veith, "Model Checking" (Second Edition, MIT Press). 

Section 07 is based on the software tool NuSMV http://nusmv.fbk.eu/

Assessment

Individual project, written exam, and oral exam.

The individual project consists of modeling and verifying a software system with NuSMV. 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 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 aim of the project is to check the capability of the student in the practical and autonomous use of the acquired skills about the modeling and verification of software.

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 related to grammars, automata, and formal semantics. Notes and didactical material can be used. The written exam mark is at most 20/30. The aim of the written exam is to verify the capability of applying the acquired competences concerning the theoretical topics of the program.

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. The objective of the oral exam is to estimate making judgements as well as communication and learning skills.

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

Disability and Specific Learning Disorders (SLD)

Students who have registered their disability certification or SLD certification with the Inclusion and Right to Study Office can request to use conceptual maps (for keywords) during exams.

To this end, it is necessary to send the maps, two weeks before the exam date, to the course instructor, who will verify their compliance with the university guidelines and may request modifications.