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 | PhD defense
Tomorrow (21 Jan)
Anton Artemov: Parallelization of Dynamic Algorithms for Electronic Structure Calculations
, Time: 13:15

If you wish to attend on site, please contact phone 018-471 2979

Join via Zoom: Click here for Zoom link

Anton Artemov will present and defend his PhD thesis Parallelization of Dynamic Algorithms for Electronic Structure Calculations.

Opponent: Prof. Bo Kågström

Supervisor: Emanuel Rubensson

The aim of electronic structure calculations is to simulate behavior of complex materials by resolving interactions between electrons and nuclei in atoms at the level of quantum mechanics. Progress in the field allows to reduce the computational complexity of the solution methods to linear so that the computational time scales proportionally to the size of the physical system. To solve large scale problems one uses parallel computers and scalable codes. Often the scalability is limited by the data distribution.

This thesis focuses on a number of problems arising in electronic structure calculations, such as inverse factorization of Hermitian positive definite matrices, approximate sparse matrix multiplication, and density matrix purification methods. No assumptions are made about the data distribution, instead, it is explored dynamically.

The thesis consists of an introduction and five papers. Particularly, in Paper I we present a new theoretical framework for localized matrices with exponential decay of elements. We describe a new localized method for inverse factorization of Hermitian positive definite matrices. We show that it has reduced communication costs compared to other widely used parallel methods. In Paper II we present a parallel implementation of the method within the Chunks and Tasks programming model and do a scalability analysis based on critical path length estimation.

We focus on the density matrix purification technique and its core operation, sparse matrix-matrix multiplication, in Papers III and IV. We analyze the sparse approximate matrix multiplication algorithm with the proposed localization framework, add a prior truncation step, and derive the asymptotic behavior of the Frobenius norm of the error. We employ the sparse approximate multiplication algorithm in the density matrix purification process and propose a method to control the error norm by choosing the right truncation threshold value.

We present a new version of the Chunks and Tasks matrix library in Paper V. The library functionality and architecture are described and discussed. The efficiency of the library is demonstrated in a few computational experiments.

Tuesday 26 Jan
Shakir Mohamed (DeepMind): AI for Science and Responsibility
, Time: 13:00-14:00

Join via Zoom: Click here for Zoom link

Questions in research and science and how we generate and represent knowledge are increasingly entangled with the use of data and as part of our effort to understand and intervene within complex systems. AI enters as an oft-called on tool that transforms how we solve our world's complex challenges. And yes, there is a positive role for the tools of our field to have an impact and I hope to look at two areas of particular interest to me in healthcare and the environment. At the same time, what was once an obscure field of computer science is now a field driving profit and scrutinised by national policies and developmental strategies. We can motivate AI for science as one of using AI for good, but increasingly we need to consider that our work can instead be implicated in harm. To explore this other side of our field,

I'll discuss topics in technological neutrality and some of my recent work in imagining a new type of critical technical practice informed by our shared experience of colonialism, and more generally invite a discussion about values in AI technology.

Disputation | PhD defense
1 February
Bui Phi Diep: On Solving String Constraints
, Time: 9:15

If you wish to attend on site, please contact phone 0701679467

Join via Zoom: Click here for Zoom link

Bui Phi Diep will present and defend his PhD thesis On Solving String Constraints.

Opponent: Prof. Matthew Hague.

Supervisor: Mohamed Faouzi Atig.

Software systems are deeply involved in diverse human activities as everyone uses a variety of software systems on a daily basis. It is essential to guarantee that software systems all work correctly. Two popular methods for finding failures of software systems are testing and model checking. Various efficient testing and model checking approaches are satisfiability-based, where the core of the approaches is Satisfiability Modulo Theories (SMT) solvers for solving the path feasibility and/or reachability problems. The significant growth of string manipulating programs in modern programming languages, including Python and JavaScript, demands SMT solvers being capable of analysing string constraints. This thesis proposes two frameworks for checking the satisfiability of extensive classes of string constraints, discovers a new decidable fragment of string constraints, and introduces efficient solvers for solving string constraints.

The first framework for checking the satisfiability of string constraints is based on Counter-Example Guided Abstract Refinement (Cegar) procedure, and applicable to diverse classes of string constraints. It is worth mentioning that the framework is the first one ever that can support both context-free membership and transducer constraints. The framework has two components: under-approximation and over-approximation. The under-approximation uses flat automata to restrict the search for a solution to only strings generated by a flat automaton. The over-approximation abstracts the input constraints and produces a counter-example of the abstraction. In the second framework for checking the satisfiability string constraints, the under-approximation uses parametric flat automata to restrict the domain of variables, thus allows better performance. Furthermore, the second framework is capable of solving string-number conversion constraints. It is a crucial characteristic since string-number conversion is a part of the definition of core semantics in numerous program languages such as Python and JavaScript.

The thesis introduces a new decidable fragment of string constraints, called weakly-chaining. This fragment pushes the borders of decidability of string constraints by generalising the existing straight-line as well as the acyclic fragment of the string logic. The new decidable fragment is empirically useful as it helps string solvers guarantee termination in many more cases since the solvers do not provide any guarantee of termination to handle string constraints in general.

The thesis also presents three efficient solvers for solving string constraints, called Trau, Trau+, and Z3-Trau. Trau uses the first framework presented above and is capable of solving a large class of constraints including transducer and context-free grammar. Trau+ is a later version of Trau and implemented the decision procedure of the weakly-chaining fragment in the over-approximation. Z3-Trau follows the second framework above and uses parametric flat automata for under-approximating the domain of variables. These three string solvers are evaluated on not only existing but also newly generated benchmarks. Evaluation results show that the solvers significantly outperform other state-of-the-art string solvers.

Disputation | PhD defense
5 March
Oscar Samuelsson: Sensor fault detection and process monitoring in water resource recovery facilities
, Time: 13:15

Zoom link will be published soon.

Oscar Samuelsson will present and defend his PhD thesis Sensor fault detection and process monitoring in water resource recovery facilities.

Opponent: Prof. Elling W. Jacobsen
Supervisor: Bengt Carlsson

See also the list of all upcoming seminars.

Internal seminars. Lecturers may be either internal or external.