See all upcoming seminars in LäsIT and seminar web pages at the homepage for the PhD studentseminars, TDB, Vi2, Theory and Applications Seminars (TAS) @ UpMARC., Department of Mathematics and The Stockholm Logic Seminar.

Disputation | Dissertation
Tomorrow (21 Jan)
Tuan-Phong Ngo: Model Checking of Software Systems under Weak Memory Models
Location: ITC 2446, Time: 13:15

Tuan-Phong Ngo will present and defend his PhD thesis Model Checking of Software Systems under Weak Memory Models.
Opponent: Dr. Victor Vafeiadis, Max Planck Institute for Software Systems.
Supervisors: Mohamed Faouzi Atig, Parosh Aziz Abdulla and Philipp Rümmer.

DiVA includes an abstract and the full text of the thesis.

Tuesday 22 Jan
Prof. Margot Gerritsens: A discussion around Data Science Education
Location: Mässen, 6140, ITC, Time: 13:15-15:00

Prof. Margot from Stanford will visit TDB in January 2019. Margot Gerritsen ( ) was director of ICME (institute of computational and mathematical engineering) at Stanford University, see, 2010-2018. Since 5 years, they have a Data science track in their Master of Science education (, and Margot was heavily involved in developing it.


Tuesday 22 Jan
Chang Hyun Park (KAIST, South Korea): Hybrid Virtual Caching: An Effort to Capture the Best of Both Worlds
Location: ITC 1146, Time: 14:00-15:00

Today, virtual memory is used in virtually every computing machine we use. Virtual memory provides the convenience and flexibility of management for the user and the operating system. Unfortunately, as it is an indirection, every memory access needs to be translated from a virtual, program aware address, to a physical address, or the HW system aware address. This translation occurs for every Load/Store instruction executed by the program, because physically addressed caches are widely used. Using virtual addressed caches would allow translating addresses iff the virtually addressed cache does not hold the memory. Virtually addressed caching sounds promising, and was introduced decades ago; however it has not been widely adopted due to an issue that is difficult to solve.
In this talk, I will present my work “Efficient Synonym Filtering, and Scalable Delayed Translation for Hybrid Virtual Caching”. I will introduce the benefits of virtual caching, the reason virtual caching is not widely used, and our solution of enabling the use of virtual caching (to some extent).
Chang Hyun Park is a PhD Student at KAIST, South Korea. His research interests are focused towards the computer architecture and system software stack of computing. His prior research were focused on the boundaries and interaction between the architecture and the system software, especially in the memory architecture and management. His published work focus on improving the virtual address translation component of the CPU. His research also cover heterogeneous memory systems, storage systems, and security.

Disputation | Dissertation
Wednesday 23 Jan
Stephan Brandauer: Structured Data
Location: ITC 2446, Time: 13:15

Stephan Brandauer will present and defend his PhD thesis Structured Data.
Opponent: Doug Lea, Professor at State University of New York.
Supervisor: Tobias Wrigstad.

DiVA includes an abstract and the full text of the thesis.

Applied Optimisation Arena seminar
29 January
Niklas Handin from the Department of Pharmacy: A proteomics based deconvolution algorithm for quantification of different cell types
Location: ITC 1345, Time: 15:30-16:30

Half-time seminar
30 January
Arve Gengelbach: Conservative Extension in Higher-Order Logic
Location: ITC 1111, Time: 13:15

Commonly, logical frameworks allow extensions by definitions to introduce new symbols. These definitional extensions should entail no new theorems in the original language, thus be conservative. A particular variant of higher-order logic, implemented in the Isabelle theorem proving framework, allows extension by (overloaded) constant and type definitions and maintains consistency. We discuss a semantic (model-theoretic) criterion for conservative extension by definitions - generalising consistency - and derive a syntactic(proof-theoretic) criterion for conservative extension.

Lunchseminarium | Lunch seminar BiomedIT-arena
6 February
Douglas Spangler, Department of Public Health and Caring Sciences: Ongoing projects in machine learning at Akademiska sjukhuset
Location: ITC 2446, Time: 12:00

BiomedIT-arenan bjuder in till lunchseminarium Pågående maskininlärningsprojekt vid Akademiska sjukhuset med bland annat Douglas Spangler, Institutionen för folkhälso- och vårdvetenskap. Intresse finns för nya samarbeten och studentprojekt! Registrerade anställda vid UU får lunchsmörgås om anmälda senast 31 januari på

The BiomedIT arena invits to a lunch seminar, “Ongoing projects in machine learning at Akademiska sjukhuset”. Speakers include Douglas Spangler, Department of Public Health and Caring Sciences. There is a clear interest for new collaborations and student projects! UU staff will get a lunch sandwich if registering no later than January 31 on

DoCS/CSD seminar
8 February
Peter J. Stuckey, Monash University, Australia: Multi-agent Pathfinding
Location: ITC 1311, Time: 14:15-15:00

Multi-agent pathfinding (MAPF) is a planning problem which asks us to coordinate the movements of a team of agents: from a set of unique starting locations to a set of unique target positions all while avoiding collisions. This problem appears in a variety of different application areas including warehouse logistics, office robots, aircraft-towing vehicles and computer games. Often the the environment in which agents operate is given as an undirected graph, such a grid. Common objectives then include minimising the total arrival time of all agents (aka. sum-of-costs) and minimising the arrival of the last agent at its target location (aka. makespan). In each of these common settings MAPF is known to be NP-hard (Yu and LaValle 2013) to solve optimally. Interest in the problem has nevertheless generated a wide variety of methods including optimal, suboptimal and and bounded suboptimal techniques. In this talk we will examine the conflict based search approach to multi-agent path finding, which is currently state-of-the-art, and show how it can be improved by reasoning about symmetry and sub-problem splitting.

See also the list of all upcoming seminars.

Internal seminars. Lecturers may be either internal or external.