Invited Talks and Tutorials
Invited Speakers
The following speakers have accepted to give invited presentations at FMCAD 2024.
Aina Niemetz, Stanford University
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.
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).
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.
K. Rustan M. Leino, Automated Reasoning Group, Amazon Web Services
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.