Computer-aided verification

General data

Course ID:	1000-2N09WWK
Erasmus code / ISCED:	11.303 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration The ISCED (International Standard Classification of Education) code has been designed by UNESCO.
Course title:	Computer-aided verification
Name in Polish:	Weryfikacja wspomagana komputerowo
Organizational unit:	Faculty of Mathematics, Informatics, and Mechanics
Course groups:	(in Polish) Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka Elective courses for Computer Science
ECTS credit allocation (and other scores):	(not available) Basic information on ECTS credits allocation principles: the annual hourly workload of the student’s work required to achieve the expected learning outcomes for a given stage is 1500-1800h, corresponding to 60 ECTS; the student’s weekly hourly workload is 45 h; 1 ECTS point corresponds to 25-30 hours of student work needed to achieve the assumed learning outcomes; weekly student workload necessary to achieve the assumed learning outcomes allows to obtain 1.5 ECTS; work required to pass the course, which has been assigned 3 ECTS, constitutes 10% of the semester student load. view allocation of credits
Language:	English
Type of course:	elective monographs
Prerequisites:	Foundations of mathematics 1000-211bPM Languages, automata and computations 1000-214bJAO
Mode:	Classroom
Short description:	Automatic verification of computer systems: model checking, static analysis, proving of correctness of programs. Theoretical foundations, complexity, algorithms, tools. Method of fighting against the state-space explosion: symbolic approaches, abstractions, state-space reductions. Abstract interpretation. Property specification languages and correctness proofs. Program extraction. In the lab, we learn selected tools (e.g. SMV, SPIN, CBMC, UPPAAL, Coq, Why) and their practical applications.
Full description:	1. Introduction to computer-aided verification, history of the domain (1 lecture) 2. Linear- and branching-time temporal logics: LTL, CTL, CTL* (1-2 lectures) 3. Model checking: complexity, global and local (on-the-fly) algorithms, SPIN and its specification language Promela, state-space reduction methods (2-3 lectures) 4. Symbolic approaches: symbolic model checking using OBDDs, bounded model checking using SAT-solvers, SMV, CBMC (2-3 lectures) 5. Abstractions, counter-example guided abstraction refinement (CEGAR) (1-2 lectures) 6. Chosen methods of static analysis of programs, abstract interpretation and its applications (2-3 lectures) 7. Property specification languages, program correctness proofs using for example Coq proof assistant and software verification platform Why, program extraction (2-3 lectures) 8. (optional) Verification of probabilistic and timed systems, UPPAAL (1-2 lectures).
Bibliography:	1. E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, MIT Press, 2002. 2. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen, P. McKenzie, Systems and Software Verification, Springer, 2001. 3. C. Baier, J.-P. Katoen, Principles of Model Checking. MIT Press, 2008. 4. G. J. Holzmann, The SPIN Model Checker. Pearson Educational, 2003. 5. F. Nielson, H.R. Nielson, C. Hankin, Principles of Program Analysis, Springer, 2005.
Learning outcomes:	Knowledge 1.Has a structured, theoretically founded general knowledge concerning algorithms and complexity of model checking (K_W02) 2. Has general knowledge in proving of program correctness with help of proof assistants (K_W02) Skills 1. Is able to write, check and verify program properties in a selected programming environment. (K_U05) 2. Is able to acquire information from literature, Internet and other reliable sources, integrate and interpret them. (K_U02) Competences 1. Knows the limitations of own knowledge and understands the need of further education. (K_K01) 2. Is able to do unsupervised search for information in the literature, also in foreign languages(K_K05)
Assessment methods and assessment criteria:	The final grade is based upon a written exam and laboratory assignments.

This course is not currently offered.

Course descriptions are protected by copyright.
Copyright by University of Warsaw.