UPM / IMDEA Software Institute Specialization Track in Software Development through Rigorous Methods (2017-2018)
Table of Contents
Note: this course is taught at the the IMDEA Software Institute (in the Montegancedo Campus, 500 m. from the CS School). Please get in touch with the coordinator or one of the instructors for more details regarding the exact meeting place and possible schedule changes.
This course has specific requirements. If you are not a student affiliated to the IMDEA Software Institute, please follow these instructions. If you do not follow them, you may be asked to register in some other course.
Formal methods for concurrent and reactive systems
Coordinator(s)
Instructor(s)
Length
4 credits (ECTS)
Prerequisites
Formal logic; introductory courses on concurrency and concurrent programming; good base on programming
Course web page (if any)
Not yet available.
Summary and objectives
Reactive systems, such as concurrent programs, communication protocols and control systems, are characterized by their non-terminating behavior and their persistent interaction with their environment. This course introduces the theory and practice of formal methods for the design and analysis of reactive systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity.
Topics
- Background
- Automata
- Decidability
- Complexity
- Logics (syntax and semantics)
- Decision Procedures.
- Models and semantics of reactive systems
- State transition systems
- Finite vs infinite state spaces
- Non-determinism
- Concurrency
- Synchrony vs. asynchrony
- Safety vs. liveness
- Refinement
- Real-time and hybrid systems
- Open systems
- Specification languages
- Temporal logics.
- Verification algorithms
- Temporal logic model checking
- Theory of omega automata
- Games
- Reachability
- State explosion
- Verification techniques
- Deductive vs algorithmic
- Symbolic model checking
- State space reduction methods
- Compositional and hierarchical reasoning
- Over-approximation, under-approximation and refinement.
Evaluation
Depending on student performance.
Recommended reading
Will be given depending on the previous background of the students.
Back to the initial page
Go to the IMDEA Software Institute page
