Title:  Formal Analysis and Verification 

Code:  FAV 

Ac.Year:  2008/2009 

Sem:  Winter 

Curriculums:  

Language of Instruction:  Czech, English 

Public info:  http://www.fit.vutbr.cz/study/courses/FAV/public/ 

Credits:  5 

Completion:  examination (verbal) 

Type of instruction:  Hour/sem  Lectures  Seminar Exercises  Laboratory Exercises  Computer Exercises  Other 

Hours:  26  0  0  0  26 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  60  0  0  0  40 



Guarantor:  Vojnar Tomáš, prof. Ing., Ph.D. (DITS) 

Lecturer:  Vojnar Tomáš, prof. Ing., Ph.D. (DITS) 
Faculty:  Faculty of Information Technology BUT 

Department:  Department of Intelligent Systems FIT BUT 

Prerequisites:  

 Learning objectives: 

  The goal of the course is to introduce formal analysis and verification
to students as a modern and promising method of automated
evaluation of properties of various kinds of safetycritical systems
(such as drivers and other parts of operating systems, control
software, workflow, communication protocols, parts of hardware, etc.).
The course acquaints students both with the
theoretical background of the given area, with computeraided
tools based on them as well as with successful applications of formal
analysis and verification in practice (Microsoft, Intel, Nasa, Airbus, ...).  Description: 

  Formal analysis and verification as a modern complement and/or
alternative to validating properties of systems by
means of simulation or testing. Model checking  formal verification
based on a systematic state space exploration. Selected modelling,
query, and specification
languages. Various approaches to state space reductions. Methods of
automated abstraction of systems being examined, especially predicate
abstraction. Automated theorem proving, decision procedures, modern
methods of SAT and SMT solving and their aplications in formal analysis
and verification. Static analysis based on looking for error patterns,
data flow analysis, and abstract interpretation. A brief description of
several advanced computeraided tools for formal
analysis and verification:
SMV, Spin, Slam, Blast,
Java
PathFinder, ARMC, FindBugs, etc.
(according to the current state of the art). Formal analysis and
verification of systems working in real time (Uppaal, Kronos, HyTech, TReX, and
similar tools).
 Knowledge and skills required for the course: 

  Knowledge of discrete mathematics, the theory of formal languages, and algorithmics on the bachelor's level is assumed.
 Subject specific learning outcomes and competencies: 

  Students are acquainted with principles and methods of formal analysis
and
verification and with their application within the process of designing
safetycritical systems. Students know capabilities and the basic
ways of using computeraided tools for formal analysis and verification.  Generic learning outcomes and competencies: 

  Acquired knowledge about the significance and possibilities of using
formal methods within the development of various kinds of systems and
about their growing use in practice.  Syllabus of lectures: 


 The meaning of the terms ``formal analysis and verification''.
Capabilities and advantages of methods of formal analysis and verification.
Various approaches to formal analysis and verification: model checking,
static analysis, and theorem proving.
 State spaces, state space paths, abstractions of states and
transitions. Interleaving and true concurrency. Linear and branching
time. Safety, liveness, and fairness.

Temporal logics CTL and CTL*, model checking systems whose properties
are specified in CTL or CTL* using explicitly represented state spaces.
 Binary decision diagrams for a compact, symbolic representation of state spaces and their implementation.
 Lattices, fix points, and the KnasterTarski theorem as a formal
basis for symbolic model checking. Symbolic model checking for CTL and
CTL*.
 The
temporal logic LTL, the correspondence between Büchi automata and LTL
formulae, model checking systems whose properties are specified in LTL
using Büchi automata.
 The partial order state space reduction. The symmetry state space
reduction. An overview of other state space reduction methods.
Compositional verification.
 Methods of automated abstraction of systems, the predicate
abstraction, the counterexample guided abstraction refinement loop,
Craig interpolation.
 Decision procedures and modern methods of SAT and SMT solving and
their use in formal verification (e.g., in the predicate abstraction).
 Classical dataflow analyses (such as live variables, available
expressions, etc.) as well as some selected, more advanced dataflow
analyses (like some pointer analyses), their description via flow
equations, and iterative methods of solving these methods.
 A brief note on abstract interpretation and its use for defining
static analyses. Static analyses based on searching for bug patterns.
 Formal verification of realtime systems, especially via methods
based on timed automata and symbolic approaches using regions or zones.
 Theorem proving. Principles, automated support (PVS, etc.),
applications. Combining theorem proving and methods based on state
spaces
 Syllabus  others, projects and individual work of students: 


 Two home assignments devoted to verification of a simple
system by means of two chosen tools for
formal analysis and verification (Spin, Blast, ARMC, SMV, JPF, Uppaal,
TReX, PVS, FindBugs, etc.).
 Fundamental literature: 

  Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, 2008.
 Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, SpringerVerlag, 2005.
 Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
 Study literature: 


 Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, 2008.
 Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, SpringerVerlag, 2005.
 Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
 Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. The part devoted to static analysis.
 Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
 Valmari, A.: The State Explosion Problem. In Reisig, W.,
Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429528. SpringerVerlag, 1998.
 Chess, B., West,J.: Secure Programming with Static Analysis. AddisonWesley Professional, 2007.
 Materials presented within the lectures and made accessible via the Internet.
 Materials freely accessible on the Internet, especially
papers and documentation related to the various computeraided tools for formal analysis and verification.
 Progress assessment: 

   Two evaluated home assignments  each for 20 points.
 A final examination  60 points.
 To be allowed to sit for the written examination, a student is to earn at least 20 points during the semester.
 The passing boundary w.r.t. the ECTS assessment  50 points.
 Exam prerequisites: 

  Having at least 50% of the possible point evaluation of the homeworks.  
