Přístupnostní navigace
E-application
Search Search Close
Course detail
FIT-FAVAcad. year: 2010/2011
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 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). Formal analysis and verification of systems working in real time (Uppaal, Kronos, HyTech, TReX, and similar tools).
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 reading
Classification of course in study plans
branch MBI , any year of study, winter semester, electivebranch MPV , any year of study, winter semester, electivebranch MGM , any year of study, winter semester, electivebranch MIS , any year of study, winter semester, compulsory-optionalbranch MBS , any year of study, winter semester, compulsory-optionalbranch MIN , any year of study, winter semester, compulsory-optionalbranch MMI , any year of study, winter semester, electivebranch MMM , 1. year of study, winter semester, compulsorybranch MSK , 2. year of study, winter semester, compulsory-optionalbranch MPS , 2. year of study, winter semester, elective
Lecture
Teacher / Lecturer
Syllabus
Project