Verification Modulo Theories
Alberto Griggio, Fondazione Bruno Kessler, Italy
(Tutorial)
Abstract: In this tutorial, I will present techniques for automated formal verification of a variety of systems using Satisfiability Modulo Theories (SMT) solvers as main reasoning engines. The talk will focus mainly on the problem of verifying invariant properties on symbolic transition systems, but it will also cover techniques for the verification of Linear Time temporal logic (LTL) properties and extensions to deal with parameterized systems with an unbounded number of components. I will also introduce some concrete tools to solver Verification Modulo Theories problems automatically, and present a demo of their use in a realistic application.
Bio: Alberto Griggio is a researcher in the Formal Methods unit of Fondazione Bruno Kessler, Italy. He works on automated reasoning and formal verification, mainly focusing on techniques based on SMT solvers. He has been involved in the development of a number of verification tools (including the MathSAT SMT solver, the nuXmv symbolic model checker, and the Kratos program verifier) and their applications in industrial settings.
Systems Correctness Practices at AWS: Leveraging Formal and Semi-formal Method
Ankush Desai, Amazon Web Services, USA
(Tutorial)
Abstract: Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, fault-injection testing, deterministic simulation, event-based simulation, and runtime validation of execution traces. Formal methods have been an important part of the development process – perhaps most importantly, formal specifications as oracles or monitors that provide the correct answers for many of AWS’s testing practices. Correctness testing and formal methods remain key areas of investment at AWS. In this talk, we will cover some of these tools and techniques that have had impact within AWS and then also open challenges that remains to be solved to further amplify the adoption of formal methods in practice.
Bio: Ankush Desai is a Principal Applied Scientist at Amazon Web Services (AWS), where he develops tools and techniques to help developers build reliable distributed services. His research focuses on making rigorous software engineering practices accessible to developers, integrating formal methods, fuzzing, systematic testing, and runtime monitoring across the development lifecycle from design through production. As the creator and lead developer of the P programming framework, his work has been particularly impactful in ensuring the correctness of critical systems, including USB drivers in Windows and distributed services at AWS. He earned his PhD in Computer Science from UC Berkeley (2019). Before his doctoral studies, he spent over two years at Microsoft Research India, where he worked on formal verification of device drivers and distributed systems.
Program Synthesis: Pre-LLM and Post-LLM
Ashish Tiwari, Microsoft Research, USA
(Invited Talk)
Abstract: This talk will cover the exciting progress made in the field of Program Synthesis over the years. Program synthesis is broadly concerned with generating programs from specifications. Program synthesis is a fascinating field since it encompasses a whole spectrum of problems that are obtained by just considering different notions of specifications and different classes of programs. We will discuss general approaches that have been developed, including bottom-up synthesis, top-down synthesis, and constraint-based synthesis. We will also cover some applications of program synthesis. The advent of large language models had an influence on the field, and in the second part of the talk, we will cover more recent work on program synthesis in this new age of large language models, along with the new opportunities it presents.
Bio: Ashish Tiwari is currently a Principal Researcher at Microsoft in the PROSE team. Before joining Microsoft in 2018, he was a Staff Scientist in the formal methods group of the Computer Science Laboratory at SRI International. He works in the areas of formal methods, synthesis, static program analysis, automated deduction, verification, hybrid systems, and symbolic computation. Some of his significant contributions include work on automated abstractions and verification of hybrid systems and the development of novel paradigms and techniques for program synthesis. Dr. Tiwari received his Bachelors degree in Computer Science from the Indian Institute of Technology, Kanpur in 1995, and his Ph.D. in Computer Science from the State University of New York at Stony Brook in 2000.
Integrating Large Language Models in Automated Program Verification
Nina Narodytska, VMware Research by Broadcom, USA
(Invited Talk)
Abstract: The demonstrated code‑understanding capabilities of large language models (LLMs) raise the question of whether they can be used for automated program verification—a task that typically demands high‑level, abstract reasoning about program properties, which remains challenging for existing verification tools. In this talk, we overview several research directions, developed over the past two years, that propose methodologies for combining the strengths of LLMs and automated reasoners in program verification. We then take a closer look at Lemur, a tool that formally describes such a methodology as a set of derivation rules and proves its soundness. Lemur instantiates the calculus as a sound automated verification procedure and demonstrates practical improvements on a suite of synthetic and competition benchmarks.
Bio: 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 and CapeKR'25.