Ufuk Topcu: Autonomous systems in the intersection of learning theory, formal methods and controls

Abstract: Autonomous systems are emerging as a driving technology for countlessly many applications. Numerous disciplines tackle the challenges toward making these systems agile, adaptable, reliable, user friendly and economical. On the other hand, the existing disciplinary boundaries delay and possibly even obstruct progress. I argue that the non-conventional problems that arise in the design and verification of autonomous systems require hybrid solutions at the intersection of learning, formal methods and controls.

I will present our recent results in two problems. The first one is on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for dynamics that are subject to rich temporal logic specifications, heterogenous uncertainties and possibly adversarial environments. They combine ideas from control theory with those from formal methods, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. My studies of the second problem have resulted in a series of new reinforcement learning algorithms that build on both learning theory and formal methods. A common feature in these algorithms is the guarantees they provide during both training and execution with respect to given formal specifications expressed in variants of temporal logic.

Xiaowei Huang: Verification of Robotics and Autonomous Systems

Abstract: Critical breakthrough has been made in Artificial Intelligence (AI) that AI achieved human-level intelligence in several tasks such as speech recognition, image recognition, and video game playing. AI has been applied to areas as diverse as autonomous vehicles, robotics, chatbots, healthcare, smart cities, and financial trading. The research is needed to bridge the gap between the fast-growing development and deployment of AI systems, particularly AI-enabled Robotics and Autonomous Systems (RAS), and their dependability and trustworthiness. In this talk, I will discuss our recent works on the verification of RAS. The first part will be on the verification of deep neural networks (DNN). DNN is an indispensable component of RAS to implement their cognitive and/or control capability, but has been criticised for its safety problem, i.e., instability to adversarial examples. To ensure the safety of RAS in critical applications, it is important to verify the DNN before its deployment. The second is on the trustworthiness of RAS. Humans must be able to trust the actions of AI to want to work with them, and AI must develop or establish trust in the actions of human co-workers to ensure effective collaboration. To enable an effective human-robot cooperation, it will be essential to enhance AI systems with trust mechanism to correctly evaluate and dynamically track the trust levels between human and AI.

Dino Distefano: Facebook Infer Static Analyser

Infer is an open-source static analyser developed at Facebook. Originally based on Separation Logic, Infer has lately evolved from a specific tool for heap-manipulating programs to a general framework which facilitates the implementation of new static analyses. In this talk, I will report on the Infer team’s experience of applying our tool to Facebook mobile code, each day helping thousands of engineers to build more reliable and secure software. Moreover, I will discuss the team’s current effort to turn Infer into a static analysis platform for research and development useful both to academic researchers and industrial practitioners.

Bernhard K. Aichernig: Smart Black-box Testing – Combining Model Learning and Model-based Testing

Testing has always been a challenge due to (1) its incompleteness by nature, (2) the lack of good specifications and (3) by its high demand for resources. With the growing complexity of the systems-under-test the situation is not likely to improve. The combination of model-learning with model-based testing offers an opportunity to master this complexity. In my talk I will introduce this line of research and report about our recent results including applications in the Internet of Things.  Our goal is a natural evolution of testing: with the trend of our environment becoming “smarter”, e.g. smart homes, smart cars, smart production, smart energy, our testing process needs to become smart as well. We are seeing the advent of smart testing.

Alfons Laarman: LTSmin: Exploiting Locality for High-Performance, Language-Independent Model Checking

Symbolic model checkers harness the power of modern SAT/SMT solvers and/or decision diagrams. To achieve this, the input problem has to be encoded in logic. For complicated inputs, such as software, this encoding quickly becomes infeasible, prompting many model checkers to instead opt for a mere “soundy” encoding of the original problem.

LTSmin therefore takes another approach: It learns the transition relation while executing the steps in the input program. Locality is exploited to learn the relation in parts, which makes the engine truly symbolic. The learned relation is stored in Decision Diagrams (DDs). Typically, after only a few learning steps, the model checker can continue the exploration completely symbolically, i.e., using only DD operations.

In this talk, we will have a detailed look at the symbolic engine of the LTSmin model checker. Moreover, we will point out several other uses of locality to boost the performance in model checking. An open question is whether a similar approach can also be used with SAT/SMT-based techniques.

Gabriel Ebner: The Lean Theorem Prover

Lean is a new, open source, interactive theorem prover designed to support mathematical reasoning as well as hardware and software verification. One of the goals is to bridge the gap to automated theorem proving by integrating automated reasoning tools such as E-matching, congruence closure, and simplfication. These are implemented in a white-box fashion, allowing the user to access their internals, for example the equivalence classes of the congruence closure algorithm. Because its logical foundation, dependent type theory, has a computational interpretation, we can also use Lean as a programming language and evaluate expressions with a fast bytecode evaluator.

In this tutorial, I will give an introduction to the Lean language, show how to write definitions, and how to use tactics to prove properties about them. I will then showcase the integrated automation tools on examples from software verification.

Speakers

Ufuk Topcu

Dr. Topcu joined the Department of Aerospace Engineering and Engineering Mechanics at The University of Texas at Austin as an assistant professor in Fall 2015. He received his Ph.D. degree from the University of California at Berkeley in 2008. Before joining The University of Texas, he was with the Department of Electrical and Systems Engineering at the University of Pennsylvania. He was a postdoctoral scholar at California Institute of Technology until 2012.

His research is on the design and verification of autonomous systems.

Xiaowei Huang

Xiaowei joined Oxford University, working with Prof. Marta Kwiatkowska, in July 2015. Before that, from January 2009 to June 2015, Xiaowei worked as a research fellow in the School of Computer Science and Engineering, University of New South Wales, Australia, working with Prof. Ron van der Meyden. Xiaowei obtained his Ph.D. degree from Academy of Mathematics and System Sciences, Chinese Academy of Sciences, under the supervision of Prof. Weiming Lu, and visited Prof. Huimin Lin for 3 months at the Institute of Software, Chinese Academy of Sciences.

Xiaowei’s research concerns the correctness (e.g., safety, normality, trustworthy, etc) of autonomous systems, including

• logic-based approaches for the specification, verification, and synthesis of autonomous multi-agent systems, and
• safety verification of machine learning techniques such as neural network-based deep learning.

Dino Distefano

Dino Distefano is a  Professor of Software Verification in the School of Electronic Engineering and Computer Science at Queen Mary, University of London. Previously he was a Royal Academy of Engineering Research Fellow.

He was also a founder of Monoidics Ltd a technology startup specialised in automatic verification tools.

Monoidics was acquired by Facebook in July 2013.

Dino received his Ph.D. from the University of Twente, in The Netherlands.

Bernhard K. Aichernig

Bernhard K. Aichernig is a tenured associate professor at Graz University of Technology, Austria. He investigates the foundations of software engineering for realising dependable computer-based systems.

Bernhard is an expert in formal methods and testing. His research covers a variety of areas combining falsification, verification and abstraction techniques. Current topics include the Internet of Things, model learning, and statistical model checking. Since 2006, he participated in four European projects. From 2004-2016 Bernhard served as a board member of Formal Methods Europe, the association that organises the Formal Methods symposia. From 2002 to 2006 he had a faculty position at the United Nations University in Macao S.A.R., China. Bernhard holds a habilitation in Practical Computer Science and Formal Methods, a doctorate, and a diploma engineer degree from Graz University of Technology.

Alfons Laarman