LPAR-25 will feature the following invited talks:
Nate Foster (EPFL)
TITLE: NetKAT: Learning Models and Solving Equations
ABSTRACT: NetKAT is a domain-specific language for specifying and verifying packet-switched networks. Based on Kleene algebra with tests, it has a sound and complete equational theory and a decidable equivalence problem, which enables verification of many network properties. However, verification assumes a model of the network as a concrete program. This talk surveys two lines of recent work that relax this assumption: an approach for building NetKAT models based on automata learning, and an approach for solving NetKAT (in)equations with unknowns via program synthesis.
BIOGRAPHY: Nate Foster is a Professor of Computer and Communication Sciences at EPFL and a Visiting Researcher at Jane Street. He currently serves as Vice Chair of DARPA's Information Science and Technology (ISAT) study group. The goal of Nate’s research is to develop languages and tools that make it easy for programmers to build secure and reliable systems. His current work focuses on the design and implementation of languages and tools for programmable networks. In the past he has also worked on bidirectional languages (also known as “lenses”), database query languages, data provenance, type systems, mechanized proof, and formal semantics. Nate received a PhD in Computer and Information Science from the University of Pennsylvania, an MPhil in History and Philosophy of Science from Cambridge University, and a BA in Computer Science from Williams College. He is an ACM Fellow, and his awards include a Sloan Research Fellowship, an NSF CAREER Award, the SIGPLAN Robin Milner Award, the SIGCOMM Rising Star Award, as well as several paper and teaching awards.
Marieke Huisman (University of Twente)
TITLE: Bug-free embedded software: a realisable dream? (and how VerCors will help…)
ABSTRACT:
Software is everywhere, and (almost) everything we do relies on software. But can we actually rely on software? Software bugs are just as old as software, and frequently cause major disruptions, such as the recent CrowdStrike’s outage due to a software update. I will argue that it should be possible to improve this situation by developing program verification tools that can be used efficiently to provide guarantees about programs in different programming languages, and for a wide range of properties. I will outline how we work towards this dream with the VerCors team. In particular, I will discuss some of the recent developments around VerCors on various use cases for program verification.
BIOGRAPHY: Marieke Huisman is well-known for her work on specification and verification of parallel software. At the University of Twente, she heads the CS department and leads the Formal Methods and Tools group. With her team, she develops the VerCors verifier, a practical verifier for concurrent software verification. She advances the field of program verification, but also actively collaborates with industry on practical case studies and usability studies. Her work has been supported by several grants, such as the ERC Starting Grant for the VerCors project (2011), the EU project CARP (2011), NWO Top project VerDi (2015), VICI project Mercedes (2018), NWO OTP project Cheops (2019), and the SAVES project with WWU Münster (2020). She chairs IPN, the Platform of Dutch Computer Science researchers, and is actively involved in various organisations such as the Netherlands Academy of Engineering, ETAPS, and VerifyThis. She received the Netherlands Prize for ICT research 2013.
Nina Narodytska (VMWare Research by Broadcom)
TITLE: Using Formal Verification for the Text-to-SQL Task
ABSTRACT: Large Language Models (LLMs) have made significant progress in assisting users to query databases in natural language. While LLM-based techniques provide state-of-the-art results on many standard benchmarks, a number of challenging problems remain unresolved, which we discuss in this talk. First, we provide an overview of the Text-to-SQL problem and its interactive version, where the agent can ask the user clarification questions. Second, we consider the main
challenges that the agent faces in solving this problem, including complex relationships, multi-turn conversations, ambiguous user queries, and weak evaluation procedures. Third, we explore formal verification–driven solutions for improving and evaluating Text-to-SQL. For example, a verification-driven performance evaluation of ten Text-to-SQL methods on the high-profile BIRD dataset suggests that existing methods often overlook differences between the generated query and the ground truth, leading to incorrect evaluation results. Finally, we discuss the possible logical formalization of the interactive Text-to-SQL problem and outline its remaining challenges.
BIOGRAPHY: Nina Narodytska is a staff researcher at VMware Research by Broadcom. Prior to VMware, she was a researcher at Samsung Research America. She completed postdoctoral studies in the Carnegie Mellon University School of Computer Science and the University of Toronto. She received her PhD from the University of New South Wales. She was named one of "AI's 10 to Watch" researchers in the field of AI in 2013. She has presented invited talks and tutorials at FMCAD'18, CP'19, AAAI'20, IJCAI'20, LMML'22, CP'22, ESSAI'23, KR'24, CapeKR'25, and FMCAD'25
Cesare Tinelli (University of Iowa)
TITLE: Reasoning about Collections in SMT
ABSTRACT: Research in Satisfiability Modulo Theories (SMT) has dedicated lots of effort and has had great success in the development of efficient and scalable solving techniques for constraints in the theories of various scalar types. In contrast, relatively little attention has been paid to theories of collection types such as finite sets, multisets, relations, and tables. However, being able to reason about such collections efficiently is crucial for verification problems in a variety of applications involving, for instance, database schemas and SQL queries, access-control policies, software design models, ontologies and knowledge graphs, normative requirements, network configurations, distributed protocols, and memory consistency. This talk presents an overview of a line of research focused on reasoning about collection types in SMT in the context of the popular CDCL(T ) deductive framework, where theory reasoning can be limited to sets of literals and localized to specialized theory solvers. In this context, a clear pattern emerges that reduces reasoning about collections of elements to reasoning about three types of constraints — membership, congruence, and cardinality constraints — and leads to analogous solutions across different collection types. The talk illustrates a general approach, based on deductive calculi, that capitalizes on the features of CDCL(T) solvers, pointing to important differences between the calculi for each theory. It also briefly discusses theoretical properties of those calculi such as soundness, completeness and termination, as well as experimental results obtained with implementations in the SMT solver cvc5, concluding with promising directions of current and future research.
BIOGRAPHY: Cesare Tinelli is an Erich Funke Professor in Computer Science at the University of Iowa. His research interests include automated reasoning and formal methods. He has done seminal work in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has appeared in more than 120 peer-reviewed publications. He has co-led the development of the widely used and award-winning CVC3, CVC4 and cvc5 SMT solvers. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He is an associate editor of the Journal of Automated Reasoning and a co-founder of the SMT workshop series and the Midwest Verification Day series.
He has served in the program committee of more than 90 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FroCoS, FTP, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15 and CADE-29. He received an NSF CAREER award in 2003, a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community, and a CAV Conference award in 2021 for his role in the development of SMT.