Keynote Speakers

Rob Manning

(NASA Jet Propulsion Laboratory, USA)

Talk Title: The Challenge of Designing Reliable Complex Mars Landers and Rovers

About the speaker: Rob Manning is Chief Engineer for NASA’s Jet Propulsion Laboratory (JPL) as well as Chief Engineer for JPL’s Engineering and Science Directorate. An Engineering Fellow, he has been designing, testing and operating robotic spacecraft for 40 years including Galileo to Jupiter, Cassini to Saturn and Magellan to Venus and many Mars missions.
In the early 1990's, Rob became the Mars Pathfinder Chief Engineer where he also led the Entry Descent and Landing (EDL) team. After successfully landing and operating the first airbag lander and rover on another planet, he co-conspired the idea to modify the Pathfinder and Sojourner Rover designs to become the Mars Exploration Rovers (MER), Spirit and Opportunity. On MER he led the rover system engineering team as well as the EDL team. At this time, he co-conceived the idea of skycrane landing that was later used by Mars Science Laboratory (MSL).
After MER he became the Mars Program Chief Engineer where he helped plan and integrate the various Mars missions like Phoenix Lander, Mars Reconnaissance Orbiter, MSL and and beyond.
In 2007, Rob became the Chief Engineer for the MSL Project that successfully landed Curiosity Rover on Mars on August 5, 2012. Rob was responsible for ensuring that the design, the test program and the team, working together, would result in a successful landing and a productive rover. Rob wrote about his experiences in a book called “Mars Rover Curiosity: An Inside Account from Curiosity’s Chief Engineer”.
Most recently Rob helped create a team to design and build an emergency use ventilator specifically for the COVID-19 pandemic.
As a result of his luck at JPL, Rob has received four NASA medals, is in the Aviation Week Magazine Space Laureate Hall of Fame in the Smithsonian Air and Space Museum, has received two honorary PhDs, has a minor planet named after him and is an Associate Fellow of the American Institute of Aeronautics and Astronautics. In 2004, SpaceNews magazine named Rob as one of 100 people who made a difference in civil, commercial and military space since 1989.
Rob is a graduate of Caltech and Whitman College where he studied math, physics, computer science, and control systems. He makes his home in Pasadena, CA with his wife Dominique and their daughter, Caline.

Erika Abraham

(RWTH Aachen University, Germany)

SMT Solving: Past, Present and Future

Since the development of the first computer algebra systems in the '60s, automated decision procedures for checking the satisfiability of logical formulas gained more and more importance. Besides symbolic computation techniques, some major achievements were made in the '90s in the relatively young area of satisfiability checking, and resulted in powerful SAT and SAT-modulo-theories (SMT) solvers. Nowadays, these sophisticated tools are at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas. In this talk we give a historical overview of this development, describe our own solver SMT-RAT and discuss some fascinating new developments for checking the satisfiability of real-arithmetic formulas.

About the speaker: Erika Abraham graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Since 2008 she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.

Matthew B. Dwyer

(University of Virginia, USA)

Distribution-aware Validation of Neural Networks

Neural networks (NN) are trained to produce a statistically accurate function approximation for data drawn from a target data distribution. The data distribution can be thought of as an implicit precondition on the use of the network. As with traditional software, the validation process need only focus on inputs satisfying the precondition -- attempts to invoke a function outside of its precondition constitute errors that should be mitigated at runtime.

In this talk, we advocate for the modeling of the data distribution and describe how it can be exploited for NN testing, verification, and falsification. Incorporating such a model into NN validation processes can reduce their cost and increase their effectiveness. We demonstrate this by speeding up the process of generating valid NN test inputs while completely avoiding the generation of invalid test inputs.

About the speaker: Matthew B. Dwyer is the Robert Thomson Distinguished Professor in the Department of Computer Science at the University of Virginia. He has authored more than 140 scholarly publications in program analysis, software specification, and automated formal methods. His research contributions have been recognized with the ICSE "Most Influential Paper" award (2010), the SIGSOFT "Impact Paper" award (2010), and the ESEC/FSE "Test of Time" award (2018). He was named an ACM Distinguished Scientist (2007), a Fulbright Research Scholar (2011), an IEEE Fellow (2013), a Parnas Fellow (2018), and an ACM Fellow (2019). He is most proud of his work with students including his 10 graduated PhD students, 5 of whom hold faculty positions and 3 of whom have won major awards (e.g., NSF CAREER), and his 6 current PhD students.

Cristina Cifuentes

(Oracle Labs, Australia)

The Flavour of Real-World Vulnerability Detection and Intelligent Configuration

The Parfait static code analysis tool focuses on detecting vulnerabilities that matter in C, C++, Java and Python languages. Its focus has been on key items expected out of a commercial tool that lives in a commercial organisation, namely, precision of results (i.e., high true positive rate), scalability (i.e., being able to run quickly over millions of lines of code), incremental analysis (i.e., being able to run over deltas of the code quickly), and usability (i.e., ease of integration into standard build processes, reporting of traces to the vulnerable location, etc). Today, Parfait is used by thousands of developers at Oracle worldwide on a day-to-day basis.

In this presentation we’ll sample a flavour of Parfait — we explore some real world challenges faced in the creation of a robust vulnerability detection tool, look into two examples of vulnerabilities that severely affected the Java platform in 2012/2013 and most machines since 2017, and conclude by recounting what matters to developers for integration into today’s continuous integration and continuous delivery (CI/CD) pipelines. Key to deployment of static code analysis tools is configuration of the tool itself - we present our experiences with use of machine learning to automatically configure the tool, providing users with a better out-of-the-box experience.

About the speaker: Cristina Cifuentes is a Senior Director of R&D, serves as the Director of Oracle Labs Australia and is an Architect at Oracle. Headquartered in Brisbane, the Lab focuses on Intelligent Application Security aiming at making intelligent security of applications a reality, at scale. Prior to founding Oracle Labs Australia, Cristina was the Principal Investigator of the Parfait bug tracking project at Sun Microsystems, then Oracle. Today, Oracle Parfait has become the defacto tool used by thousands of Oracle developers for bug and vulnerability detection in real-world, commercially sized C/C++/Java applications. Parfait's success is founded on the pioneering work in advancing static program analysis techniques by Cristina’s team of Researchers and Engineers at Oracle Labs Australia. Cristina’s passion for tackling the big issues in the field of Program Analysis began with her doctoral work in binary decompilation at Queensland’s University of Technology. In an interview with Richard Morris for Geek of the Week, Cristina talks about Parfait, Walkabout and her career journey in this field. Before she joined Oracle and Sun Microsystems, Cristina held teaching posts at major Australian Universities, co-edited Going Digital, a landmark book on cybersecurity, and served on the executive committees of ACM SIGPLAN and IEEE Reverse Engineering. Cristina continues to play an active role in the international programming language, compiler construction and software security communities. On the weekends, she channels her interests into mentoring young programmers through the CoderDojo network.

Azadeh Farzan

(University of Toronto, Canada)

Talk Title: Composing Proofs From Program Behaviours

Compositional proofs have always been the holy grail of reasoning about concurrent programs. Classically, compositionality strictly means composing correctness arguments over individual program components (threads, processes, ..) into a correctness argument for the entire program, with some extra supporting arguments that are preferably kept at a minimum required. In this talk, I will outline a different approach to verification of (concurrent) programs based on a different notion of compositionality. This notion is closer to the (mostly) informal way that programmers reason about the correctness of their code, namely operational reasoning. The correctness argument for a full program is composed from proofs of finitely many program behaviours.

Beyond providing novel solutions to the classic (hard) verification problems, that is safety and liveness of concurrent programs, I will argue that the framework becomes vitally important in accommodating solutions for more sophisticated verification problems. This includes the use of program reductions, which are broadly used to simplify reasoning about the correctness of concurrent and distributed programs.

About the speaker: Azadeh Farzan is a Professor at the department of computer science at University of Toronto. Her research focuses on the theory and applications of formal methods, in particular, verification of concurrent programs and synthesis of recursive, parallel, and reactive code. She received her PhD from University of Illinois at Urbana-Champaign in 2007. She was a recipient of an OMR early career award and National Science and Engineering Council of Canada DAS award.