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.

Half-time seminar
Johan Janzén: Leveraging application diversity with GPU co-scheduling
Location: ITC 1145, Time: 13:15-14:00

GPU as a compute platform has become ubiquitous in high performance computing today and more classes of algorithms are successfully moved to this platform. Algorithms and tasks that struggle to scale to the full GPU efficiently present an opportunity for co-scheduling. This challenge requires available knowledge about task scalability as well fast-enough re-allocation features, and has the potential of efficient use of GPUs in multi-appliation and virtual environments in the future. By profiling online and with careful dynamic reallocation of compute resources we show that we can harness application diversity for improved performance when available, while keeping the performance high when tasks already scale.

Half-time seminar
Anke Stüber: Towards a framework of privacy notions for process algebra
Location: ITC 1111, Time: 15:15


Nowadays, where even toasters are connected to the Internet, and software routinely handles personal data, it has become important for software developers to tackle the difficult problem of ensuring privacy for their users. Process algebra gives us a tool to formally verify the privacy properties of concurrent systems, but until recently there existed no widely accepted formal definitions of privacy notions. Authors differed slightly in how they translated informal descriptions into formal definitions, making comparisons of their results difficult. In 2019, Kuhn et al. presented a hierarchy of formal definitions of privacy notions for anonymous communication networks, based on indistinguishability games. In this seminar I will present a related approach using process algebra, where behavioural equivalence tests are used instead of indistinguishability games, and where it is clearly defined which events are observable to an attacker. This formalisation will further the understanding of privacy properties, and may lead to the discovery of conditions that are sufficient to ensure certain privacy notions while being automatically verifiable with existing process algebra tools.

Disputation | Dissertation
Wednesday 18 Dec
Peter Backeman: Quantifiers and Theories: A Lazy Approach
Location: ITC 2446, Time: 9:00

Peter Backeman will present and defend his PhD thesis: Quantifiers and Theories: A Lazy Approach.
Opponent: Professor Jie-Hong Roland Jiang from National Taiwan University.
Supervisors: Philipp Rümmer

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

Licentiatseminarium | Licentia
9 January
Huu-Phuc Vo: Towards Machine-Assisted Reformulation for MiniZinc
Location: ITC 1213, Time: 15:15

Model reformulation plays an important role in improving models, reducing search space so that solutions can be found faster. Hence we categorise model reformulation into three types: a model is reformulated to another model with the same modelling language, a model with non constraint programming standard types is compiled to another model with constraint programming (CP) standard types, and a model is converted to Boolean satisfiability problem (SAT), Mixed-integer programming (MIP), Satisfiability modulo theories (SMT), and Mixed integer linear programming (MILP). Based on these categories, reformulation and compilation could be used in different ways to improve a model such as automatic reformulations, semiautomatic reformulations, MIP to constraint programming, implied constraints, set Constraint Satisfaction Problems (CSPs) to CSPs, string variables to CSP without string variables, symmetry breaking, pre-computation, non-binary to binary translations, and reformulations into SAT, MILP, and SMT. CP is a pervasive and highly successful technology for solving a wide variety of constraint satisfaction problems such as air traffic management, resource allocation, transportation, scheduling, and so on. Model reformulation can have a significant impact on solving time. Techniques from formal methods will be used to provide machine assistance for MiniZinc, which is the high-level modelling language to model CSPs. In this thesis, we present an overview of reformulation focusing on the contributions made in the area of reformulation of CSPs where significant performance improvements have been achieved. Our contributions are as follows: propose criteria and types that categorise model reformulations; we systematically unify and organise the vast literature; contrast and compare different categories of the reformulation for solving CSPs; propose a compiler for counter automata reformulation; ultimately, we propose a plan for future work, we identify the challenges, implement frameworks, and evaluate our experimental results of model reformulations.

See also the list of all upcoming seminars.

Internal seminars. Lecturers may be either internal or external.