This course aims to introduce the principles and foundations of programming languages in order to understand their structure and correctly interpret the behavior of programs. First, the objective involves the study of the theory of formal languages, which includes the tools for defining syntax (through grammars and automata) and formalizing semantics. Second, in the context of such formal tools, the goal is to address some techniques for modeling complex software systems and verifying their properties through the use of automata- and logic-based methodologies.

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. 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.

03. Regular languages:
      03.01 Finite-state automata and linear grammars.
      03.02 Closure properties of regular languages and pumping lemma.
      03.03 Regular expressions.
      03.04 Regular expressions and finite-state automata.

04. Context-free languages:
      04.01 Free grammars and syntax trees.
      04.02 Chomsky normal form.
      04.03 Properties of context-free languages and pumping lemma.

05. Pushdown automata and parsing:
      05.01 Pushdown automata and relation with free grammars.
      05.02 Top-down parsing.
      05.03 LL(1) grammars.
      05.04 Bottom-up parsing.
      05.05 SLR, LR(1), and LALR(1) grammars.

06. Denotational semantics:
      06.01 Denotational semantics for non-cyclic sequential programs.
      06.02 Denotational semantics for the while operator.
      06.03 Denotational semantics with blocks and procedures.

07. Operational semantics:
      07.01 Natural semantics for sequential programs.
      07.02 Natural semantics with blocks and procedures.
      07.03 Structural operational semantics.

08. Modeling and verification of reactive systems:
      08.01 Kripke structures.
      08.02 Linear temporal logic.
      08.03 Computation tree logic.
      08.04 Model checking algorithms.

09. Laboratory activity:
      09.01 Finite state machines.
      09.02 Modeling and verification in NuSMV.
      09.03 Complex reactive systems in NuSMV.

Although there are no mandatory prerequisites for this exam, students are strongly recommended to take it after the course of Software Architecture and Engineering and the course of 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

Handouts, excercises, and solutions of exams are available in the Moodle platform for blended learning.

Teaching

Theory lectures and laboratory exercises.

Innovative teaching methods

Project activities are planned for problem-based learning in small groups and the learning-by-doing approach.

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-05. The original version of the former book is Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley.

Sections 06 and 07 are inspired by Nielson, Nielson, "Semantics with Applications: An Appetizer" (Springer). Alternative book: Semantica operazionale e denotazionale dei linguaggi di programmazione, Rocco De Nicola (1999, CittàStudiEdizioni, Torino).

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

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

Assessment

Individual or group project, written exam, and oral exam.

The project consists of the modeling and verification of a software system using the NuSMV tool. The text of the project, one per session, is published at least one month before the start of each session, with delivery by noon two days before the written test to be taken. The project, even if passed, is valid only for the session with which it is associated. The text is given by the specification of a real system to be modeled and verified. The level of abstraction of the model, the variants and configurations under analysis, and the properties to be verified are freely chosen. Delivery is by email with subject LPVS: consegna progetto numero_di_matricola and containing source files with specifications and verification results, each part properly annotated. The purpose of the project is to verify the student's ability for autonomy in the practical use of the skills acquired in the area of modeling and verification of sofware. The project must be presented and discussed orally on the day of the written test. The compliance of the model with the specifications and the variety of properties taken into consideration, as well as the ratio of the complexity of the submitted project to the number of proposers (max. two people), are subject to evaluation. The project is considered sufficient if evaluated with a minimum score of 6/10 (the result weighs one-third of the overall grade).

The written exam can be taken only after the project of the same session has been handed in. It lasts 90 minutes and consists of practical exercises related to grammars, automata, and formal semantics (sections 01-07 of the syllabus). Notes and other materials are available for reference. The purpose of the written exam is to test the ability to apply the knowledge acquired regarding the theoretical topics covered in the course. The correctness of the solution and approach to solving the exercises, as well as the methodological rigor, are subject to evaluation. The test is considered sufficient if passed with a minimum score of 12/20 (the result weighs two-thirds of the overall grade).

The oral is optional on the course syllabus and involves a positive or negative adjustment (of at most 5 points) on the overall grade determined by the sum of the project grade and the written exam grade. The purpose of the oral is to assess independent judgment, communication skills, and level of understanding of the subject matter.

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.

Teaching

As for attending students.

Attendance

As for attending students.

Course books

As for attending students.

Assessment

As for attending students.

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.