Specialization Track in Software Development through Rigorous Methods





		UPM / IMDEA Track in Software Development through Rigorous Methods Table of Contents Formal methods for concurrent and reactive systems Coordinator(s)/Instructor(s) Length Prerequisites Course web page (if any) Summary and objectives Topics Evaluation Recommended reading Formal methods for concurrent and reactive systems Coordinator(s)/Instructor(s) Manuel Carro, Julio Mariño, Clara Benac, Lars-Åke Fredlund Scientific collaboration from IMDEA: César Sánchez, Pierre Ganty Length 4 credits (ECTS) Prerequisites Formal logic; introductory courses on concurrency and concurrent programming; good base on programming This course has specific requirements, and if your initial level is not adequate, you may not pass. Therefore, we ask you to please include it in the mail you ought to send to graduate.school (at) software.imdea.org with the list of courses you want to take from the IMDEA track. You will receive a mail stating the courses in which you are welcome to enroll. If you enroll in an IMDEA Track course for which you did not receive explicit approval, you may be asked to switch over to a different one. 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 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




Fractals are used with permission from their author Cory Ench \| © 2006-2007. IMDEA Software. All rights reserved \| Legal Notice \| Privacy Policy