**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:

**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).*

*Artificial Intelligence Journal*. He is currently Editor-in-Chief of

*ACM*

*Transactions on Quantum Computing*.

**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.

**Short Bio**: Assia Mahboubi is a tenured researcher (chargée de recherche) at Inria, in the Gallinette team, Nantes, France. She is also an endowed professor in the Algebra and Number Theory section of the Vrije Universiteit Amsterdam, in the Netherlands. Her research interests revolve around the foundations and formalization of mathematics in type theory and the automated verification of mathematical proofs. In particular, she is interested in the new insights that one often gets on familiar mathematical objects when looking for their most adequate formal representation for the purpose of computer-aided proof checking. She also has a special interest for the interplay between computer algebra and formal proofs, and more generally for computer-aided mathematics. I am a happy, intensive user of the Coq interactive proof assistant, and a lead developer of the Mathematical Components libraries.