IMADA Mini-student-seminar

Katrine von Bornemann Hjelmborg and Viktor Strate Kløvedal are the presenters at this semesters Mini-Student-seminar.


Below you’ll find a short summary of their presentations.


Katrine von Bornemann Hjelmborg, graduate student in Mathematics:

“Quantum Metrics on the Natural Numbers”

This is a presentation about joint research with Konrad Aguilar.

Quantum metrics in the sense of Rieffel were introduced in the beginning of the 21st
century in order to prove some statements arising in the high-energy physics
literature. Since then, the area of quantum metric geometry has been used to
answer questions stemming from within mathematics as well. To prove such results,
it is often the case that certain properties of a quantum metric are sufficient enough,
and explicit calculations of the quantum metric are rare. Thus, in this talk, we focus
on certain quantum metrics introduced by Aguilar and Latrémolière the space of
complex-valued convergent sequences, and calculate exactly the metrics on the
natural numbers that these quantum metrics induce.


Viktor Strate Kløvedal, graduate student in Computer science:

“Formal verification of fault-tolerant peer-to-peer networks”

This is a presentation about my Bachelor's thesis.

Distributed systems play a critical role in modern server infrastructure, where
services are expected to handle thousands of requests per second, to be highly
available and respond quickly to requests from all over the world.
But making distributed systems robust and error-free is notoriously hard as the
number of possible states and interactions between just a few actors quickly expand
exponentially to the thousands or even millions. Traditional software testing
methods do not apply well to distributed systems, as they are not well suited for
testing these many possible interactions.

Formal specifications try to solve this problem by separating the design of the
system from the implementation. A formal specification describes the design of a
system in a higher level than code would, but it is precise enough that it can be
verified by a model checker, a computer program that explores all possible states in
the model and checks that the specified properties and invariants always hold. This
not only helps to test the validity of the system, but it also forms as documentation
of the system which can be used by engineers to implement or validate existing
implementations.