Title:  Formal Program Analysis 

Code:  FAD 

Ac.Year:  2009/2010 

Sem:  Winter 

Curriculums:  

Language of Instruction:  Czech 

Completion:  examination (verbal) 

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

Hours:  26  0  0  0  0 

 Exams  Tests  Exercises  Laboratories  Other 

Points:  100  0  0  0  0 



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

Faculty:  Faculty of Information Technology BUT 

Department:  Department of Intelligent Systems FIT BUT 

 Learning objectives: 

  The goal of the course is to acquaint the students with principles, possibilities, and restrictions of the currently most successful methods known, resp. being studied, in the area of applying formal methods for an automated analysis and verification of programs.  Description: 

  An overview of various methods of analysis and verification of programs with formal roots. Model checking of finitestate systems: the basic principles, specification of properties to be verified, temporal logics, the state explosion problem and existing approaches to solving it (esp. partial order reduction and symbolic verification based on binary decision diagrams). Predicate abstraction. Various ways of static analysis, dataflow analyses, bug pattern analyses, abstract interpretation. SAT solving and SMT solving. Dynamic analyses.  Knowledge and skills required for the course: 

  Acquaintance with basics of logics, algebra, graph theory, theory of formal languages and automata, compilers, and computability and complexity.  Subject specific learning outcomes and competencies: 

  Acquaintance with possibilities, limitations, and principles of the stateoftheart methods of program analysis on a formal basis. Ability to apply them in advanced projects and an overall knowledge of the way these techniques can evolve in the future.  Generic learning outcomes and competencies: 

  A deeper ability to read and create formal texts.  Syllabus of lectures: 


 An overview of the existing methods of formal analysis and verification of programs, their possibilities, advantages and disadvantages.
 Temporal logics CTL, LTL, and CTL*.
 Explicitstate CTL* model checking.
 The state explosion problem and possibilities of fighting it. Partial order reduction.
 Binary decision diagrams (BDDs).
 Symbolic verification based on BDDs.
 The automatatheoretic approach to LTL model checking.
 Automated abstraction with a stress on predicate abstraction, Craig interpolants.
 SAT solving, SMT solving.
 Classical dataflow analyses (such as live variables, available
expressions, etc.) as well as some selected, more advanced dataflow
analyses (like some pointer analyses).
 A note on abstract interpretation.
 Static analyses based on searching for bug patterns.
 Dynamic analyses.
 Syllabus  others, projects and individual work of students: 


 To read and understand a stateoftheart research paper (or papers) from the area of model checking, theorem proving, static or dynamic analysis and to write a report based on the paper (papers) read.
 Fundamental literature: 


 Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0262032708
 Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: ModelChecking Techniques and Tools, SpringerVerlag, 2001. ISBN 3540415238
 Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, SpringerVerlag, 2003. ISBN 1852332476
 Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429528. SpringerVerlag, 1998. ISBN 3540653066
 Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, SpringerVerlag, 2005. ISBN 3540654100
 Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
 Study literature: 


 Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0262032708
 Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, SpringerVerlag, 2005. ISBN 3540654100
 Controlled instruction: 

  Lectures and a preparation of a report.  Progress assessment: 

  Discussions within the lectures, a check of the prepared report.  
