Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FAVAcad. year: 2013/2014
Formal analysis and verification as a modern complement and/or alternative to validating properties of systems by means of simulation or testing. Selected formalisms for specifying properties to be checked. Model checking: formal verification based on a systematic state space exploration. Various approaches to state space reductions, especially the partial order reduction. Methods of automated abstraction of systems being examined, especially predicate abstraction. 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 computer-aided tools for formal analysis and verification: SMV, Spin, Slam, Blast, Java PathFinder, ARMC, FindBugs, etc. (according to the current state of the art).
Language of instruction
Number of ECTS credits
Mode of study
Guarantor
Department
Learning outcomes of the course unit
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.
Prerequisites
Co-requisites
Planned learning activities and teaching methods
Assesment methods and criteria linked to learning outcomes
Course curriculum
Work placements
Aims
Specification of controlled education, way of implementation and compensation for absences
Recommended optional programme components
Prerequisites and corequisites
Basic literature
Recommended literature
Classification of course in study plans
branch MBS , 0 year of study, winter semester, compulsory-optionalbranch MIN , 0 year of study, winter semester, compulsory-optionalbranch MIS , 0 year of study, winter semester, compulsory-optionalbranch MMI , 0 year of study, winter semester, electivebranch MMM , 0 year of study, winter semester, compulsorybranch MPV , 0 year of study, winter semester, electivebranch MBI , 0 year of study, winter semester, electivebranch MGM , 0 year of study, winter semester, electivebranch MSK , 2 year of study, winter semester, compulsory-optional
Lecture
Teacher / Lecturer
Syllabus
Project