Abstract: This talk consists of two parts. In the first part of the talk I introduce the Message Passage Language (MPL), which is a statically typed concurrent programming language with message passing as the concurrency primitive. It brings communication safety to interacting processes using a type system. MPL consists of two languages, concurrent MPL and […]

Abstract: We have a lot of tools (static analyzers, type systems, proof assistants, linters) for analysing and proving things about programs written as source code in traditional languages. However, we are currently poorly equipped to analyze and prove things about machine learning models, simply because the resulting programs are represented as a bunch of weights […]

Abstract: In this talk we give an introduction to Mirrorsolve, a Coq library for solving Coq proofs using SMT solvers. Foundational theorem provers such as Isabelle/HOL and Coq are the gold standard for building certified systems, enabling the verification of extremely rich properties while having a minimal trusted code base. Unfortunately, these provers come with […]

Abstract: An introduction and overview of hacspec, its design principles, and usage. Bio:   Franziskus is a security & cryptography engineer and researcher based in Berlin. He is co-founder of Cryspen, a company that builds custom high assurance cryptography. Franziskus holds a PhD in provable cryptography and was previously leading the security engineering efforts at Wire […]

Abstract: Autonomous Intelligent Systems are often designed with complex, interacting objectives, or have learned behavior that is difficult to specify. This obfuscates the social and ethical rules of systems like self-driving vehicles and nursing robots in hospitals. Though their missions (e.g., go from point A to point B) are known, we need to determine their […]

Abstract: Formally verifying security properties and the functional correctness of systems involves comprehensive analyses of system compatibility and interoperability. Many conventional approaches require trusted systems in order to assure properties of transmitted data that are difficult to authenticate, or the undesirable exposure of additional data for the purpose of verification. We overcome this limitation by […]

Abstract: The exponential rise in data has spurred significant interest in developing personalized machine models for a seemingly infinite range of applications. However, in the case of safety critical systems such as autonomous medical systems, classical algorithms have failed due to complications spanning from limited data to the requirement that systems be explainable and verifiably […]

Abstract: Software bugs are pervasive in modern software. As software is integrated into increasingly many aspects of our lives, these bugs have increasingly severe consequences, both from a security (e.g. Cloudbleed, Heartbleed, Shellshock) and cost standpoint. Fuzzing refers to a set of techniques that automatically find bug-triggering inputs by sending many random-looking inputs to the […]

Abstract: Industrial control systems have been frequent targets of cyber attacks during the last decade. Adversaries can hinder the safe operation of these systems by tampering with their sensors and actuators, while ensuring that the monitoring systems are not able to detect such attacks in time. In this talk, we present methods to design and […]

Abstract: Robots are increasingly deployed outside of carefully controlled factory settings. Advances in robot motion planning have made it possible to compute feasible motions for complex systems. My work is focused on increasing the abstraction level and time horizon of the types of robot tasks that (a) can be specified, (b) are computationally tractable, and […]