Invited Speakers

Name: Mingsheng Ying

Title: Model Checking for Verification of Quantum Circuits

Abstract: In this talk, I will describe a framework for assertion-based verification of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which:

(1) noiseless and noisy quantum circuits are modelled as quantum automata and quantum Markov chains, respectively, and they are further represented by tensor networks;

(2) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic;

(3) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks.

Bio: Mingsheng Ying is a Distinguished Professor and Research Director of the Center for Quantum Software  and Information at the University of Technology Sydney, Australia. He is also Deputy Director for Research (adjunct position) at the Institute of Software at the Chinese Academy of Sciences, and holds the Cheung Kong Chair Professorship at Tsinghua University, China. Ying was also the Director of the Scientific Committee of the National Key Laboratory of Intelligent Technology and Systems at Tsinghua University. His research interests include quantum computation, theory of programming languages, and logics in AI. He has published books: Model Checking Quantum Systems: Principles and Algorithms (2021) (with Yuan Feng), Foundations of Quantum Programming (2016) and Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs (2001).

Name:  Paula Herber

Title: Combine Forces - How to Formally Verify Informally Defined Embedded Systems

Abstract: Embedded systems are ubiquitous in our everyday lives, and they are often used in safety-critical applications, such as cars, airplanes, or medical systems. As a consequence, there is a high demand for formal methods to ensure their safety. Embedded systems are, however, concurrent, real-time dependent, and highly heterogeneous. Hardware and software are deeply intertwined, and the digital control parts interact with an analogous environment. Moreover, the semantics of industrially used embedded system design languages, such as Matlab/Simulink or SystemC, is typically only informally defined. To formally capture informally defined embedded systems requires a deep understanding of the underlying models of computation. Furthermore, a single formalism and verification tool are typically not powerful enough to cope with the heterogeneity of embedded systems. In this talk, I summarize our work on automated transformations from informal system descriptions into existing formal verification tools. I present ideas to combine the strengths of various languages, formalisms, and verification backends, and discuss promising results, challenges and limitations.

Short Bio: Prof. Dr.-Ing. Paula Herber received her Ph.D. from TU Berlin in 2010. She worked as a postdoc at the International Computer Science Institute (ICSI) in Berkeley, California, as a substitute professor at the University of Potsdam, and as a postdoc and independent research group leader in the Software Engineering and Embedded Systems group at TU Berlin. Since October 2018, she is a full professor at the University of Münster and head of the Embedded Systems Group at the Computer Science Department. Her main research interests are quality assurance for embedded systems, test automation, and formal methods.

Name: Clark Barrett

Title: Domain-Specific Reasoning with Satisfiability Modulo Theories

Abstract: General-purpose automated reasoning approaches such as automated theorem proving (ATP) and Boolean satisfiability (SAT) are extremely versatile. Many interesting and practical problems can be reduced to ATP or SAT problems. On the other hand, these techniques cannot easily incorporate customized domain-specific reasoning. In contrast, this is one of the strengths of approaches based on satisfiabiilty modulo theories (SMT). This talk showcases recent work in which domain-specific customization of SMT solvers plays a key role in making otherwise intractable problems tractable. The domains discussed include reasoning about neural networks and reasoning about string constraints.

Short Bio: Clark Barrett joined Stanford University as an Associate Professor (Research) of Computer Science in September 2016. Before that, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in constraint solving and its applications to system verification and security. His PhD dissertation introduced a novel approach to constraint solving now known as Satisfiability Modulo Theories (SMT). Today, he is recognized as one of the world's experts in the development and application of SMT techniques. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. He is an ACM Distinguished Scientist.

Name: Assia Mahboubi

Title: Formal verification of computational mathematics

Abstract: Computers have changed the practice of research in mathematics, even in its most abstract fields. Widely used as observation instruments for testing and refining conjectures, they can actually also substantiate actual proof steps. A large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation.