The Logic seminar is held on Wednesdays at 12-14 in C124. After the seminar we have coffee together at 14-15 in the coffee room on the 4th floor.
The seminar is led by prof. Juha Kontinen and university lecturer Juliette Kennedy.
Schedule of the fall term 2019
Wed 4.9.2019 12-14, C124
Joni Puljujärvi: Scott sentences of metric structures in infinitary continuous logic
Wed 11.9.2019 12-13, C124
Bernd Finkbeiner (Universität des Saarlandes): Logics and Algorithms for the Synthesis of Distributed Systems
Abstract: Sixty years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of discrete systems. On the one hand, synthesis algorithms have found game-changing applications in many areas of computer science and systems engineering, from the automatic construction of control strategies for robots and manufacturing plants to the computer-aided design of coordination protocols and human-computer interfaces. On the other hand, the logical and algorithmic foundations of the synthesis problem are far from complete.
Synthesis is particularly difficult in the setting of distributed systems, where we try to find a combination of process implementations that jointly guarantee that a given specification is satisfied. A reduction from multi-player games shows that the problem is in general undecidable. Despite this negative result, there is a long history of discoveries where the decidability of the synthesis problem was established for distributed systems with specific architectures, such as pipelines and rings, or other restrictions on the problem, such as local specifications. Encouraged by these findings, new specification languages like Coordination Logic aim for a comprehensive logical representation and a uniform algorithmic treatment of the decidable synthesis problems.
In this talk, I will trace the progress from isolated decidability results towards universal synthesis logics and algorithms. I will demonstrate how the logical representation of the synthesis problem simplifies the identification of decidable cases and give an overview on the state of the art in decision procedures and strategy construction algorithms for the synthesis of distributed systems.
Wed 18.9.2019 12-14, C124
Wed 25.9.2019 12-14, C124
Davide Quadrellaro: Lattices of DNA logics and applications to Inquisitive Logic
Wed 2.10.2019 12-14, C124
Tapani Hyttinen: On discrete approximations of Hilbert space operators
Wed 9.10.2019 12-14, C124
Keijo Heljanko: Bounded Model Checking for Weak Memory Models
Abstract: We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.
Wed 16.10.2019 12-14, C124
Jeremias Berg: Bounded Treewidth Bayesian Network Structure Learning with Maximum Satisfiability
Wed 23.10.2019 12-14, C124
Wed 30.10.2019 12-14, C124
Anssi Yli-Jyrä: TBA
Wed 6.11.2019 12-14, C124
Wed 13.11.2019 12-14, C124
Max Sandström : TBA
Wed 20.11.2019 12-14, C124
Fausto Barbero: TBA
Wed 27.11.2019 12-14, C124
Tapio Saarinen: TBA
Wed 4.12.2019 12-14, C124
Otto Rajala: TBA
Wed 11.12.2019 12-14, C124
Antti Kuusisto: TBA
Wed 18.12.2019 12-14, C124