Tutorials and Invited Talks
Tutorials
Writing proofs in Dafny — Tuesday
K. Rustan M. Leino, Automated Reasoning Group, Amazon Web Services
Abstract: Dafny is a verification-aware programming language. In a nutshell, the language is Java-like and has support for writing specifications and proofs. It has a long history of being used in education, has been the cornerstone of several ambitious research projects, and is in industrial use at AWS.
This tutorial teaches how to write various kinds of proofs in Dafny. It covers proofs of imperative and functional programs, as well as the formalization of models and mathematical proofs. It demonstrates different proof styles and shows how to think about and debug proofs in the Dafny setting.
The tutorial does not assume any prior experience in using Dafny or other proof assistants.
Bio: K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct.
Leino is known for his work on programming methods and program verification tools and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.
Before Amazon, Leino was Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq Systems Research Center (SRC). He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.
Leino hosts the Verification Corner channel on YouTube. He is a multi-instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.
Invited Talks
Tackling Scalability Issues in Bit-Vector Reasoning — Wednesday
Aina Niemetz, Stanford University
Abstract: Efficiently reasoning about bit-vector constraints in Satisfiability Modulo Theories (SMT) has been an ongoing challenge for many years. The dominant state-of-the-art approach for solving bit-vector formulas in SMT is bit-blasting, an eager reduction to propositional logic that is typically combined with aggressive simplifications of the input constraints prior to the actual reduction step. Even though this eager reduction may come at the cost of significantly increasing the formula size, it is surprisingly efficient in practice—thanks to state-of-the-art SAT solvers, which are usually able to efficiently deal with complex formulas over millions of variables. This size increase, however, is a potential bottleneck and the main reason why bit-blasting does not generally scale well for increasing bit-widths, especially in the presence of arithmetic operators, which translate to large and complex Boolean circuits on the bit-level.
To tackle these scalability issues, there are two (orthogonal)
avenues to explore: developing alternative approaches that do not
(mainly) rely on translations to the SAT level, and improving the
scalability of bit-blasting itself. In this talk, we will highlight
techniques in each category: a propagtion-based local search
procedure as an alternative to bit-blasting, which can only
determine satisfiability but improves performances over bitblasting on satisfiable instances, and a CEGAR-style abstractionrefinement procedure that significantly improves the scalability
of bit-blasting. We extended the state-of-the-art SMT solver
Bitwuzla with both techniques and show that they significantly
improve solver performance on a variety of benchmark sets
across all logics supported by Bitwuzla, including combinations
of bit-vectors with arrays, uninterpreted functions and floatingpoint arithmetic.
Bio: Aina Niemetz is a Senior Research Scientist at Stanford University in the Department of Computer Science, affiliated with the Stanford Center for Automated Reasoning. She received her PhD from Johannes Kepler University Linz (Austria), supervised by Armin Biere.
Her research focus is on various aspects of Satisfiability Modulo Theories (SMT), in particular procedures for bit-vectors, arrays and uninterpreted functions. Other areas of interest include Boolean satisfiability (SAT) and automated testing and debugging techniques, in particular in the context of solver engineering.
She is one of the main developers (and senior technical leads) of the SMT solvers Bitwuzla, Boolector and cvc5. She joined the development team of the SMT solver CVC4 in June 2017, and served as one of its senior technical leads until it was succeeded by cvc5.
Some Adventures in Learning Proving, Instantiation and Synthesis — Thursday
Abstract: Human problem solvers often combine deductive reasoning and exploration with learning and pattern matching. In the recent years such combinations are also increasingly developed for building stronger automated theorem provers, SMT solvers and conjecturing and synthesis systems.
The methods in this field include equipping the current deductive systems with efficient statistically learned guidance that controls the choice of the inference steps, using for example fast decision trees, graph neural networks and their combinations.
Learning and AI methods can also be used to automatically design new symbolic strategies for today’s ATPs and SMTs. This has the advantage of producing explainable ideas for steering the search space, which can be further taken up and modified by the systems’ developers.
I will also discuss several methods that try to directly synthesize reasoning objects such as instantiations and OEIS explanations, using various neural approaches.
Perhaps the most interesting aspect of this research are the positive feedback loops between the proving and the learning methods. I will show that some of them can today go quite far and create quite interesting “alien” solutions.
Bio: Josef Urban is a distinguished researcher at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC) heading the ERC Consolidator project AI4REASON.
He is know for his work on automated reasoning in large semantically specified knowledge bases (some people call this “strong artificial intelligence”). It involves automated deductive reasoning (automated theorem proving), inductive reasoning (machine learning and discovery) and their combining. He is also involved in formalization and computer-verification of mathematics (see the QED Manifesto), especially in Mizar.
Before that, he was a postdoc researcher in the Foundations Group of ICIS at the Radboud University, Nijmegen, an assistant professor at the Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague, where he co-founded the Prague Automated Reasoning Group, and a Marie-Curie fellow at the Department of Computer Science at University of Miami.
Harnessing SMT Solvers for Reasoning about DeFi Protocols — Friday
Mooly Sagiv, Certora and Tel Aviv University
Abstract: DeFi (Decentralized Financial) Protocols implement financial programs using low-level programming. DeFi adoption started to go parabolic in 2020, and it’s still very robust in different market conditions in 2024. Today, DeFi assets exceed 300 billion USD. A fundamental principle behind DeFi is that small open-source software called “smart contracts” precisely define the trading conditions and create an open global economy not controlled by governments and people.
However, smart contracts are difficult to implement correctly since their behavior can radically change in different market conditions. Moreover, hackers constantly try to abuse the code to drain the money stored in the smart contracts. On the positive side, it is pretty natural to write high-level formal specifications of smart contracts since their economical utilities are well understood. Indeed, this is a unique domain where software developers are eager to write formal specifications.
I will describe the challenges of harnessing existing SMT solvers for reasoning about smart contracts.
Bio: Mooly (Shmuel) Sagiv is known for his work on static program analysis. He is currently Chair of Software Systems in the School of Computer Science at Tel Aviv University, and CEO of Certora, a startup company providing formal verification of smart contracts.
Sagiv’s research spans areas including static program analysis, shape analysis, abstract interpretation, logic, theorem proving, programming languages, formal methods, data-flow analysis, program slicing, network verification, and smart contracts. His most cited work is on shape analysis via three-valued logic, implemented in the TVLA system.
For his work, Sagiv was awarded the Wolf Foundation Fellowship (1989), IBM Outstanding Technical Achievement Award (1993), Friedrich Wilhelm Bessel Research Award (2002), IBM Faculty Awards (2000-2005), Chair of Software Systems in the School of Computer Science, Tel Aviv University (2008), ACM SIGSOFT Retrospective Impact Paper Award (with Thomas Reps, Susan Horowitz, and Genevieve Rosay, 2011), Microsoft Outstanding Collaborator Award (2016), and ACM Fellow (2016).