ABSTRACT. To take advantage of today's and tomorrow's multi-core processors, shared-memory concurrent programming—a notoriously complex enterprise—is becoming increasingly important. One of the key challenges pertains to safe implementation of interaction protocols: admissible patterns of synchronization/communication that threads are supposed to abide by for the whole program to behave as intended, but which are particularly hard to implement right (and, as such, a common source of deadlocks and data races). This talk gives an overview of a high-level, declarative, domain-specific language for implemeting interaction protocols, based on a formal theory of automata.

ABSTRACT. If we wish to compromise some password-protected system as an attacker (i.e. a member of the red team), we have a large number of popular and actively-maintained tools to choose from in helping us to realise our goal. Password hash cracking hardware and software, online guessing tools, exploit frameworks, and a wealth of tools for helping us to perform reconnaissance on the target system are widely available. By comparison, if we wish to defend a password-protected system against such an attack as a member of the blue team, we have comparatively few tools to choose from. In this research abstract, we present our work to date on Passlab, a password security tool designed to help system administrators take advantage of formal methods in order to make sensible and evidence-based security decisions using a clean and intuitive user interface.

ABSTRACT. This work addresses the problem of formally verifying robustness of support vector machines (SVMs), a major machine learning model for classification and regression tasks. Robustness properties asserts whether a model produces similar outputs on similar inputs, which is a key concept in adversarial machine learning, an emerging hot topic studying vulnerabilities of machine learning (ML) techniques in adversarial scenarios whose main objective is to design methodologies for making learning tools robust to adversarial attacks. An exhaustive robustness test is usually unfeasible. To overcome this issue, one can deploy abstract interpretation techniques by running a sound abstract version of the classifier, computing a super set of classes of points in a given adversarial region. This information can be therefore used to assert whether a classifier is robust on a given input with respect to a certain perturbation.

ABSTRACT. Blockchains have become ubiquitous. At the core of blockchains lies the ability to reach consensus among distributed and malicious participants. One recently developed and efficient consensus protocol is Blockmania. In this abstract we describe how we aim to (1) develop a formal specification of Blockmania, (2) give a formal proof of correctness, and (3) relate and re-use Blockmania with other protocols.

ABSTRACT. Type systems are a powerful tool in modern programming languages. Types in logic programming are usually based on an over approximation of the program's semantics or they have to be declared by the programmer. None of these approached as been widely accepted by the community. Based on the principles of types in functional programming, our goal is to define a highly expressive type system that deals with data types and type constraints and a type inference algorithm that automatically infers these types and is sound with respect to the type system. We plan to integrate this new type inference algorithm in the YAP Prolog System.

ABSTRACT. Combining gradual typing and polymorphism based in intersection types in a single language has been the focus of my work. Besides devising type systems and operational semantics that verify and run a language with these features, developing sound and complete type inference is also an important goal. This paper presents an overview of my work and recent advancements.

ABSTRACT. Python is an increasingly popular dynamic programming language, which is particularly used in the scientific community, and well-known for its powerful and permissive high-level syntax. The goal of this PhD is to develop static analyses for Python, i.e. to detect automatically uncaught exceptions in programs without running them. The current focus is to detect type and attribute errors using a type analysis.

ABSTRACT. Industrial control systems are becoming more complex and interconnected. These systems are moving from isolated, locally accessible to distributed and cloud connected architectures. This paradigm shift brings challenges especially in the area of cyber security. Often the systems in question control vast amounts of physical devices or critical infrastructure, hence strong assurance of security is required. Formal verification can provide this assurance, but complexity of these systems requires finding the right compromises and correct tools for the task. This research project investigates usage of formal verification in the setting of cloud connected industrial control systems. The goal is to provide methods and frameworks adaptable for industrial use.

ABSTRACT. Delays arise naturally in feedback loops in modern forms of embedded digital control, like networked control systems where communication between the plant and the controller is crucial. Especially when dealing with safety-critical systems, the communication delay in the feedback loop may however, become significant. In continuous control, delays are modeled by Delay Differential Equations (DDE) and it is already well-known that such delays may cause oscillations which directly affect the stability and control performance of the system. However, despite a large portion of digital control schemes being an integration of discrete and continuous state dynamics, i.e., hybrid state dynamics, there has not been much interest in considering delays in hybrid systems. To the best of our knowledge, neither an established notion of delayed hybrid system nor corresponding verification methods exist. Thus, the main objective of this project is to introduce a reasonable model of delayed hybrid automata, based on which verification techniques for delayed hybrid systems shall be established.

ABSTRACT. Correctness of autonomous driving systems is crucial as incorrect behaviour may have catastrophic consequences. Many different hardware and software components (e.g. sensing, decision making, actuation, and control) interact to solve the autonomous driving task, leading to a level of complexity that brings new challenges for the formal verification community. Though formal verification has been used to prove correctness of software, there are significant challenges in transferring such techniques to an agile software development process and to ensure widespread industrial adoption. In the light of these challenges, new research is needed to address them. This research abstract provides a background of the problem, the research questions and the method aimed to solve them, current state of research, and a very brief literature survey of related work.

ABSTRACT. In this research abstract, I cover an approach to synthesise monitors from specifications for cars in autonomous traffic. These monitors can be used to restrict the behaviour of the cars, so that a system consisting of cars equipped with the monitors satisfies certain properties. As the specification language, an extended version of Extended Multi-Lane Spatial Logic (EMLSL), a two-dimensional logic to reason about (highway) traffic is used.