Course of Automatic Software Verification (Verifica Automatica del Software)
2016-2017.
Face-to-face
course.
First Year
of the Laurea Magistrale in Ingegneria Informatica.
Teacher: Alberto Pettorossi.
Curriculum Vitae.
You can talk to
the teacher after the lectures
(also those of
Automata Theory and Formal Languages) or by appointment.
6 cfu
(crediti formativi). Code: 8039737.
Settore
Scientifico Disciplinare: Sistemi di Elaborazione delle Informazioni.
ING-INF/05
09-H1
60 hours of
face-to-face teaching (unique module).
Contratto
integrativo: Proofs of Properties of Programs
(Dr. Ing.
Xxx Yyy) (5 hours).
Lectures: from
03.10.16 to 28.01.17
Tuesday
11:30-13:15 (Room B5)
Friday
11:30-13:15 (Room B12)
The lecture of 25/10/2016 has been postponed to 26/10/2016 11:30 a.m. at the teacher's office.
Exams and
Seminars.
Same
time and place as the exams of the course: Automi
e Linguaggi.
Please, visit that site.
Exam
registration.
You
should register using the online system http://delphi.uniroma2.it
and send to the
teacher (pettorossi@info.uniroma2.it)
seven
days before the day of the call an
email
with the
subject: ite2016_Lastname_Firstname_RegistrationNumber
and the
message:
'Desidero prenotarmi per l'appello
del day/month/year.
Ho svolto il
take-home-exam da solo. First_name Family_name'
You should attach
(in .pdf format) a report of the solutions of the take-home-exam.
Normally,
you cannot register to more than one exam calls per exam session
and no more than three exam calls per academic year.
On the day of
the written exam you should hand-in a paper report
with the solution of the take-home-exam.
On
the day of the oral exam you should come with a PC with the programs
of the project A1 (or the projects A1 and A2), ready for
execution.
Learning
Objectives. The
course offers an overview of the methods for the definition
of the semantics of the imperative, functional, logic, and concurrent
programming languages.
Those methods deepen the logical and algebraic understanding of various
techniques
for specifying and verifying properties of programs written in those languages.
Some programming projects and the use of suitable software tools will
reinforce the understanding of the theoretical notions.
Detailed
Syllabus and Exam Questions.
Take-home-exam: to be done by yourself.
Syllabus.
1. Decidability and Turing
computability. Partial Recursive Functions.
2. Structural induction, well-founded induction, and rule induction.
Recursion Theorem.
3. Operational, denotational, and axiomatic semantics of an imperative
language.
Hoare's triples for partial correctness. Hoare's calculus:
soundness and relative completeness.
4. Operational and denotational semantics of a first order functional
language:
call-by-value and call-by-name regimes.
5. Domain theory. A metalanguage for denotational semantics. Bekic's
Theorem.
Inclusive predicates and proofs of properties of functional
programs.
6. Operational and denotational semantics of a higher order functional
language: eager semantics
and lazy semantics. Fixpoint operators. Beta and eta rules.
Adequacy and full abstraction.
7. Operational and denotational semantics of Horn-clause programs.
8. Dijkstra's nondeterministic guarded commands. Owicki-Gries rules for
parallel commands.
Milner's calculus for communicating concurrent processes.
9. mu-calculus and proofs of communicating systems and protocols. Local
model-checking.
Requirements
for the course: Fundamentals
notions of Computer Science. Algorithms and Data Structures.
Elements of Algebra
and elements of Predicate Calculus.
Attendance to lectures is compulsory.
Previous Exam Questions
Statistics of the outcome of previous exam sessions.
Exam
Information:
(i) Marks: 18 - 20: 10 exercises of the take-home-exam +
Project A1 + Written and Oral
Exam.
(ii) Marks: 21 - 25: 10 exercises of the take-home-exam +
Projects A1 and A2 + Written and Oral Exam.
(iii) Marks: 26 – 30L: all exercises of the take-home-exam + Projects A1 and A2
+ Written and Oral Exam.
Books:
[P1] Pettorossi, A.: Semantics of Programming Languages. Third
Edition, Aracne Editrice, 2016.
[P2] Pettorossi, A.: Elements of Computability, Decidability, and
Complexity, Fifth Edition.
Aracne Editrice, 2016.
[PP] Pettorossi, A., Proietti, M.: First Order Predicate Calculus and
Logic Programming,
Fourth Edition, Aracne Editrice, 2016.
Book for further reading:
[Wi] Winskel, G.: The Formal Semantics of Programming Languages: An
Introduction,
The MIT Press (1993) (Also available in Italian).
Errata Corrige
-------------------------------------------------------------