Theoretically, it’s impossible to ensure that software is secure, bug-free, and will do everything it is supposed to do under all circumstances. But that doesn’t mean we shouldn’t keep trying. According to Dr. Oded Padon, a recent recruit to Weizmann Institute faculty, in some cases the best strategy is not to laboriously test software after it is developed. Instead, he says, a more complete verification of software systems can be achieved through mathematical proofs.
“Verification has been studied since the 1970s, but in software, the number of scenarios needed to achieve full verification is potentially infinite,” Dr. Padon says, who will join the Institute in 2022 after completing a postdoc at Stanford University. “That’s why it’s important to find a way to ensure that software is correct based on mathematical logical reasoning. This is particularly important for distributed systems involving networks of computers, which can have subtle bugs that can’t be ruled out by testing.”
Dr. Padon develops logical techniques that can be integrated into distributed software as it is being developed, thereby eliminating bugs and reducing the need to test software in the post-design phase. Building on topics he explored in graduate school, his approach emphasizes transparency of automated reasoning tools, and a foundation based on mathematical logic.
“Most existing verification tools hide the complexity of automated reasoning from the user,” he says. “The problem is, when there’s a bug or a time out, the user is left in the dark about what happened. My approach to verification is based on transparent automation as a design principle, such that the user is guaranteed to get some actionable output from the tool. This principle leads to increased productivity of the verification process.”
Dr. Padon became interested in computer programming as a child, and did his army service in the IDF’s Talpiot program, where he focused on both computer science and physics. After completing his army service at the age of 27, a meeting with Prof. Mooly Sagiv, an expert on software verification who would later become his doctoral advisor at Tel-Aviv University, opened his eyes to the excitement of basic research.
Biosketch
Born in Tel Aviv and raised in both Kiryat Ono and Ganei Tikva, Dr. Oded Padon served in the Talpiot, an elite research and technology unit in the Israel Defense Forces. During his army service, he completed BSc in physics and mathematics from the Hebrew University (2007) as well as an MSc environmental physics from Ben-Gurion University (2014).
He earned his doctorate in computer science from Tel-Aviv University (2018). From 2018 to 2020, Dr. Padon worked as a postdoctoral fellow at Stanford University, and then as a researcher at VMWare, a technology company headquartered in Palo
Alto, California.
Dr. Padon’s PhD Thesis won the Doctoral Dissertation Award from the European Joint Conferences on Theory and Practice Software Association (ETAPS) in 2020.
