LPAR-25 will feature the following invited talks:
Nate Foster (Professor of Computer & Communication Sciences EPFL, Visiting Researcher Jane Street)
TITLE: TBA
ABSTRACT: TBA.
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
TBA (TBA)
TITLE: TBA
ABSTRACT: TBA.
BIOGRAPHY: TBA.