 Learning goals
Q3, Topic 1: Graphtransformation (Arend Rensink)
The student acquires:
 Knowledge and understanding of the basic concepts of graph transformation
 Insight in the use of graph transformation for modelling and verification in general
 Skill in applying graph transformation for the construction and manipulation of syntax graphs and heap graphs
Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)
After passing this class, the student is able to
 Explain the basic concepts of risk management
 Identify and model system risks via fault trees and FMECAs
 Quantify risks via appropriate metrics, e.g, risk priority number, reliability, availability
 Devise appropriate counter measures to reduce the system risks, and study the effect of counter measures on the risk metrics
Q4, Topic 1: Verification of Concurrent Software (Marieke Huisman)
The student acquires:
 Knowledge about the use of program logics to reason about the behaviour of sequential and concurrent software
 Understanding how tool support for the use of program logics can be developed
 Practical experience with program verification using program logics
Q4, Topic 2: Multicore model checking (Jaco van de Pol)
The student acquires:
 Knowledge about various model checking algorithms, in particular explicit and symbolic algorithms for CTL and LTL model checking
 Knowledge about parallel implementations of model checking algorithms, in particular for multicore shared memory systems
 Practical skills to implement and experiment with parallel model checking algorithms.
 Understanding of the experimental tradeoffs between efficient algorithms and parallel scalability
 Content
Software is everywhere, and our society is depending more and more on software working reliably and efficiently. To make it more reliable and efficient, we need to have a thorough understanding of the behavior of software systems, and how we can analyse and improve this behavior. This course gives insights in current research directions in the area of software systems, and how these new ideas can be used to improve software.
The goal of the course Software Science is to teach several topics related to active, ongoing research in software engineering and formal methods. Each edition of the course consists of two topics of roughly 4 weeks each. Each topic consists of four lectures, complemented with exercise or lab sessions to gain practical experiences with the material introduced during the lectures. Each topic is finished with an individual homework assignment. The homework assignment is assessed by the topic teacher, and the final grade of the course is the average of the two topic grades.
If one is interested in more than two topics, it is possible to follow the course a second time choosing two different topics. In this way, one can study 4 topics for 10 ECTS.
The list of projects and topics will be revised every year. In the course year 2017/2018, we plan to teach the following topics:
 Q3, Topic 1: Graphtransformation (Arend Rensink)
 Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)
 Q4, Topic 1: Verification of concurrent software (Marieke Huisman)
 Q4, Topic 2: Multicore model checking (Jaco van de Pol)
Q3, Topic 1: Graphtransformation (Arend Rensink)
Graph transformation is a very widely applicable modelling paradigm, which here is used to capture the syntax and semantics of programming languages. This involves recognising that both the syntactic structure of a program itself and its effect in terms of what happens during execution can be represented by graphs. Graph transformation rules can then be defined to manipulate these graphs in a deterministic fashion reflecting what happens during parsing and execution of a program. In this part of the course, we explain the basic concepts of graph transformation and how they can be applied in the way described above. This is supported by a tool called GROOVE (which stands for “GRaphs for ObjectOriented VErification”) in which you can try out everything you have learned and develop rule systems yourself.
Q3, Topic 2: Quantitative Risk Analysis (Mariëlle Stoelinga)
How do we ensure that robots, drones, Internet of Things devices, and medical systems function correctly? That is the role of risk management: identify the main system risks, assess their impact, and take appropriate counter measures. This class discusses two common methods for quantitative risk analysis, namely fault tree analysis (FMTA) and failure mode, effect and criticality analysis (FMECA), as well as their underlying techniques.
Q4, Topic 1: Verification of Concurrent Software (Marieke Huisman)
We introduce the notion of program logic to verify software. Traditionally, program logics are used to reason about sequential software. Recently, extensions have been proposed to reason about concurrent software. We introduce the various logics, and discuss in particular permissionbased separation logic. We show how this logic is suitable to reason about concurrent software using different concurrency paradigms. We also discuss how use of the program logic can be supported by a tool. The homework assignment will ask the student to use program logics to verify some concurrent programs yourself.
Q4, Topic 2: Multicore model checking (Jaco van de Pol)
First, we introduce the basic algorithms for model checking properties of concurrent systems. In particular, we will treat explicit and symbolic graph algorithms for LTL and CTL properties. These algorithms are combinations of DepthFirst Search and BreadthFirst Search. Next, we study the concurrent datastructures and parallel algorithms that are needed for a highperformance implementation of these graph algorithms. The goal is to understand how the choice for a particular datastructure or algorithm influences the efficiency and parallel scalability of the model checking problem. The practical assignment evolves around the application of the LTSmin toolset to international modelchecking benchmarks and competitions.
 Assumed previous knowledge   Required materialsRecommended materialsCourse materialPapers will be provided via Blackboard 
 Instructional modesLecture
 Project unsupervised
 Tutorial

 TestsTest


 