Professor in Computer Science
Technische Universität Dresden, Germany
Standpoint logics have been introduced in recent work by Alvarez et al. as a multi-modal logic to reason about the integrated knowledge of multiple agents that might have different, possibly contradicting views (``standpoints''). The essential new feature are modalities for expressing that a property is conceivable according to the view of an agent. The talk considers the model checking problem for a standpoint extension of classical linear temporal logic (LTL) with five semantics for the standpoint modalities. The semantics differ in the information an agent can extract from the history. Starting with a generic non-elementary model checking algorithm that is applicable to all five semantics, a more detailed complexity analysis leads to improved upper bounds for four of the semantics. In three cases, the model checking problem turns out to be PSPACE-complete, i.e., not harder than the model checking problem for classical LTL, which stands in contrat to the known EXPSPACE-completeness result for the satisfiability problem for standpoint LTL.
Christel Baier is a full professor and head of the chair for Algebraic and Logic Foundations of Computer Science at the Faculty of Computer Science of the Technische Universität Dresden since 2006. Since 2022 she holds an honorary doctorate (Dr. rer. nat. h.c.) from RWTH Aachen. From the University of Mannheim she received her Diploma in Mathematics in 1990, her Ph.D. in Computer Science in 1994 and her Habilitation in 1999. She was an associate professor for Theoretical Computer Science at the University of Bonn from 1999 to 2006. She was member of the DFG (German Research Foundation) review board for computer science from 2012 to 2019, and is a member of the DFG senate commission on Research Training Groups since 2020. She is a member of Academia Europaea and of the Saxony Academy of Science. Her research focuses on modeling, specification and verification of reactive systems, quantitative analysis of stochastic systems, probabilistic model checking, temporal and modal logics and automata theory.
Professor of Quantum Programming
University of Edinburgh, UK
Quantum computing inherently has concurrent aspects. Even with only local operations, qubits can influence each other. This ability leads to genuinely new quantum communication protocols, but also raises even thornier questions of causality than in classical concurrent computing. Monoidal categories and their string diagrams form a convenient and popular language for quantum computing. After an introduction to quantum concurrency, I will discuss the framework of tensor topology, which aims to analyse the interaction of several agents in monoidal categories, using notions from sheaf theory and ordered locales.
Chris Heunen is the Professor of Quantum Programming at the University of Edinburgh, co-founder of the Quantum Software Lab, and Director of the Centre for Doctoral Training in Quantum Informatics. He has been working in theoretical computer science and quantum computing for over 20 years, obtaining his PhD at the Radboud University Nijmegen in the Netherlands and working at the University of Oxford and the California Institute of Technology before moving to Edinburgh. His expertise lies in categorical semantics of quantum programming, on which he has authored a textbook, and has published articles across top venues in computer science (LiCS, ICALP), mathematics (PNAS, Advances in Mathematics), and physics (PRL). His work has been awarded the 2012 Birkhoff-von Neumann prize by the International Quantum Structures Association.
Professor in Computer Science
Aalborg University, Denmark
Dependency graphs, introduced over two decades ago by Liu and Smolka, are directed graphs with hyperedges linking nodes to sets of target nodes to model causal dependencies. Many verification problems can be addressed by computing minimum or maximum fixed-point assignments on these graphs. I shall introduce the notion of dependency graph including efficient and distributed on-the-fly verification algorithms and demonstrate their applicability on a number of verification problems like CTL model checking of concurrent systems. In classical dependency graphs, assignments map nodes to Boolean values, but recent work has expanded to more general, even infinite, domains. In the second part of the talk, I will review recent advancements in extending dependency graphs towards verification of quantitative, probabilistic, parameterized, and timed systems and provide a link to existing verification tools supporting the dependency graph approach.
Jiri Srba is professor in computer science at Aalborg University, Denmark. He obtained his first PhD degree in 2003 at BRICS international PhD school in Aarhus and a second one in
2005 from Faculty of Informatics, Masaryk University in Brno, Czech Republic. Jiri Srba co- authored more than 140 peer-reviewed scientific papers and a book about verification of reactive systems. He is a steering committee member of CONCUR and a founder and prime investigator of the award-winning model checker TAPAAL. His research focuses on modeling, verifying, and analyzing real-time and embedded systems, with applications in web services, workflow analysis, and industrial cases, relying on formalisms like Petri nets, timed automata, modal transition systems, and process algebras. He also explores component-based software, energy game optimization, strategy synthesis, and the decidability and complexity questions for infinite-state processes.
Professor in Computer Science
University of Oxford, UK
Concerned with general temporal specifications over dynamical models and reactive programs, I discuss how sound synthesis plays a central role for the formal verification of stochastic systems. Verification can be attained via synthesis either of certificates based on proof rules, or of formal abstractions. For both problems, I discuss two separate approaches, the first (constructive) based on full knowledge of models, the latter (inductive) leveraging samples from their dynamics and the training of neural nets.
In the context of sequential decision making problems over stochastic systems, I additionally discuss how to generate policies/strategies/controllers, in order to formally attain given specifications, again with model-based and data-driven techniques.
Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received Laurea-MS/PhD degrees from the University of Padua and UC Berkeley.
Associate Professor in Computer Science
University of Virginia, USA
The rise of learning-enabled cyber-physical systems (CPS) in safety-critical domains calls for novel runtime safety assurance mechanisms. This talk presents our recent work in logic-guided predictive monitoring and adaptive shielding as foundational techniques for safeguarding learning-enabled CPS at runtime. We explore a range of systems employing various learning components: from monitoring sequential predictions generated by Bayesian Recurrent Neural Networks to shielding unsafe actions in reinforcement learning for multi-agent interactions, partially observable environments, and settings with hidden parameter variations. Extensive case studies in robotics, healthcare, and smart cities illustrate the potential impact of our methods, paving the way for safe and trustworthy learning-enabled CPS.
Lu Feng is an Associate Professor of Computer Science at the University of Virginia, USA. She holds a D.Phil. in Computer Science from the University of Oxford. Her research bridges formal methods, machine learning, and human-autonomy interaction to advance the development of learning-enabled cyber-physical systems that are provably correct and aligned with human values. Her work spans a range of application domains, including robotics, autonomous driving, medical devices, and smart cities. Dr. Feng serves as an Associate Editor for the ACM Transactions on Cyber-Physical Systems and is a steering committee member of the ACM/IEEE Conference on Cyber-Physical Systems.
University of Oldenburg, Germany
DTU Technical University of Denmark, Denmark
Over the last 15+ years, probabilistic programs have received much attention. By now, there exists a plethora of proof rules for quantifying, amongst others, the termination probability or expected runtimes of such programs. Those rules must be adapted and combined to enable the verification of feature-rich probabilistic programming languages. In this talk, I will discuss ongoing work on developing an intermediate verification infrastructure for automating proof rules for probabilistic programs.
Christoph Matheja is a Professor at the University of Oldenburg and an associate professor at the Technical University of Denmark. His research interests include deductive verification techniques and model checking of probabilistic and heap-manipulating systems.
Associate Professor in the Formal Methods and Tools group
University of Twente, NL
The study of quantitative system properties such as resilience, response times, and throughput is crucial in the design and operation of complex cyber-physical systems. The formal methods community has developed a variety of approaches to evaluate and optimise such properties with clear correctness and optimality guarantees. In practice, however, every application poses new challenges that require adaptations and novel combinations of the "off-the-shelf" methods we usually present in scientific papers. In this presentation, I will use recent case studies ranging from water management for storm surge protection to routing in satellite constellations to (i) contrast the different demands on model expressiveness and tool capabilities of each application and (ii) highlight the capabilities of the Modest Toolset to solve these challenges with the varied modelling, simulation, and verification approaches it implements. Throughout, I will survey the degree to which our tools actually (fail to) deliver the correctness and optimality guarantees they claim.
Arnd Harmanns is associate professor in the Formal Methods and Tools group at the University of Twente. His primary research interests are modelling tools and formalisms for stochastic timed and hybrid systems (in particular Modest) and their applications in various fields. He advocates reproducibility in Computer Science research, via artifact evaluation initiatives, tool competitions, and standardised benchmark sets. He was previously a postdoc in the Formal Methods and Tools group at the University of Twente and the Dependable Systems and Software group at Saarland University, where he also completed his Ph.D. in computer science with a thesis On the Analysis of Stochastic Timed Systems in 2015.
Independent Researcher and Honorary Professor for Software-Based Innovations
Technical University of Berlin, Germany
In industry, software testing is the primary method to verify and validate the functionality, performance, security, usability, and so on, of software-based systems. Test automation has gained increasing attention in industry over the last decade, following decades of intense research into test automation and model-based testing. However, designing, developing, maintaining and evolving test automation is a considerable effort. Meanwhile, AI's breakthroughs in many engineering fields are opening up new perspectives for software testing, for both manual and automated testing. This paper reviews recent research on AI augmentation in software test automation, from no automation to full automation. It also discusses new forms of testing made possible by AI. Based on this, the newly developed taxonomy, ai4st, is presented and used to classify recent research and identify open research questions.
Ina Schieferdecker is an independent researcher and Honorary Professor for Software-Based Innovations at the Technical University of Berlin. Since her PhD, she has been active in protocol testing, software testing, test automation, model-based testing, performance testing and security testing - in telecommunications, automotive, data platforms, smart cities and medical IT. She was a member of the TTCN-3 team at ETSI, an initiator of the UML testing profile at OMG, and an initiator of the test automation syllabus at ISTQB - and is a 1st day member and now an honorary member of the German Testing Board.
