NASA Logo, National Aeronautics and Space Administration

Keynote Speakers

Léonard Bouygues
Google Loon

Title: Evolving airspace regulations and systems to enable large scale, highly automated operations in the stratosphere

Abstract: Loon is a network of stratospheric vehicles that provide connectivity to thousands of people living in underserved regions around the world. With over 350k flight hours in 2019 and over one million flight hours total, it is the world’s first large-scale automated fleet of unmanned vehicles.

Aviation regulations, concepts of operations, and aviation systems need to evolve to enable new technologies like Loon. Loon is partnering with regulators, the entire community of stratospheric operators, and research organisations to cooperatively evolve this airspace. 1) Develop collaborative traffic management concepts that are necessary to handle the unique vehicle performance characteristics, and the dynamic ecosystem. 2) Develop new risk and performance based safety frameworks needed to ensure a safe environment in which technologies and designs can evolve rapidly. 3) Develop new validation methods for modern software development techniques and a rapidly evolving software ecosystem. 4) Propose adaptations to roles and responsibilities of humans in the context of large scale automated systems.

Bio: Leonard is currently Head of Aviation Strategy at Loon. Loon is a network of high-altitude balloons that provide telecommunications access to unserved and underserved populations. It is the first large-scale automated fleet of unmanned vehicles and has already surpassed one million flight hours.

In this role, Leonard is responsible for the development of innovative aviation concepts. He currently leads industry players in the development of the “Collaborative Traffic Management in the Stratosphere” CONOPs. He is also a key contributing author of the initial paper that he presented at Drone Enable 2019. Additionally, Leonard is currently working in partnerships with NASA, MITRE, academia and research organisations to evolve safety frameworks within FAA’s safety continuum, in particular for in-time safety management, risk budgeting and human automation teaming for the supervision of large autonomous fleets.

After joining Loon in 2015, Leonard led Loon’s Flight Operations from 2017-2019. In this position, he built and managed the company’s Operation Control Center, enabling Loon to supervise a fleet of hundreds of autonomous vehicles. In this effort, Leonard’s team also developed technology for live risk computation of Loon operations.

Leonard started at Google’s European headquarters as an Analytical Lead, before joining the Mountain View office to work as a Product Lead in the advertising division. Leonard holds a Master’s in Aeronautical Engineering from Imperial College London, a M.Sc. in Management of Technology and Innovation form MIT, and a M.Sc. in management from HEC Paris.

Byron Cook
Amazon Web Services (AWS) and University College London (UCL)

Title: Automated Reasoning at Amazon

Abstract: This talk will discuss the development and use of formal verification tools within Amazon Web Services (AWS) to increase the assurance of its cloud infrastructure and to help customers help themselves build correct cloud-based systems. I will also discuss some open challenges that could inspire future research in the community.

Bio: Byron Cook is Professor of Computer Science at University College London (UCL) and Senior Principal Scientist at Amazon. Byron’s interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. See here for more information.

David Dill
Facebook and Stanford University

Title: A formal verifier for the Libra blockchain Move language

Abstract: The Libra blockchain, which was initiated last year by Facebook, includes a novel programming language called Move for implementing smart contracts. We plan for the Libra blockchain to host massive amounts of assets, and all transactions are mediated by Move programs, and smart contracts on other blockchains have had devastating bugs resulting in major losses of assets, so we consider the correctness of Move programs to be critical. The Move language is designed to be as safe as we can make it, and it is accompanied by a formal specification and automatic verification tool, called the Move Prover. Our aspiration is that ever Move program will be thoroughly specified and verified before being deployed on the blockchain.

Bio: David L. Dill is a Lead Researcher at Facebook, working on the Libra blockchain project. He is also Donald E. Knuth Professor, Emeritus, in the School of Engineering at Stanford University. He was on the faculty in the Department of Computer Science at Stanford from 1987 until going emeritus in 2017, and starting his current position at Facebook in 2018. Prof. Dill’s research interests include formal verification of software, hardware, and protocols, with a focus on automated techniques, as well as voting technology and computational biology. He is an IEEE Fellow, an ACM Fellow and a member of the National Academy of Engineering and the American Academy of Arts and Sciences. He received an EFF Pioneer Award for his work in voting technology, and is the founder of

Dana Schulze
National Transportation Safety Board (NTSB)

Title: Improving Design Assurance Through Accident/Incident Lessons Learned

Abstract: The NTSB has investigated or participated in the investigation of numerous accidents and incidents involving the failure of complex aircraft systems. While accidents involving these types of failures are quite rare, their occurrence offers lessons learned for the design and certification communities. Findings in several cases suggest that these malfunctions are not typically the result of software production deficiencies but rather system or software requirements deficiencies. Case studies involving two NTSB investigations will be discussed and used to introduce the broader set of design issues that accident and incident investigations have revealed, which could be useful in understanding the improvements needed in design assurance methods and their implementation to improve complex system certification outcomes.

Bio: Dana Schulze, Director of the Office of Aviation Safety, has been with the National Transportation Safety Board since 2002. She began her career with the Safety Board as an Aircraft System Safety Engineer in the Aviation Engineering Division and served as a Group Chairman and investigator on numerous major domestic and international airline accident investigations, including Alaska Airlines flight 261, Pinnacle Airlines flight 3701, and American Airlines flight 587. In 2006, Ms. Schulze became Chief of the Aviation Engineering Division, which is responsible for investigating the airworthiness of aircraft involved in major aviation accidents and serious incidents. Ms. Schulze later served as the Chief of the Major Investigations Division where she oversaw more than a dozen major airline accident investigations, including the investigation of US Airways flight 1549 in Weehawken, New Jersey and Colgan Air flight 3407 in Clarence Center, New York and subsequently as Deputy Director, leading the organization’s execution of air carrier investigations and safety initiatives as well as the development of emergent programs for unmanned aircraft systems and commercial space accident investigation. In 2018, she was named the Acting Director of the Office of Aviation Safety and moved into the Director role in 2019. Prior to joining the NTSB, Ms. Schulze worked in the commercial aerospace industry in staff engineering and engineering management roles related to design, system safety, reliability, and quality. She received her Bachelor of Science degree in Space Sciences and Mechanical Engineering from the Florida Institute of Technology and Master of Science degree in Mechanical Engineering from the State University of New York. Ms. Schulze is also a recipient of the Distinguished Presidential Rank Award, which recognizes a select group of career members of the United States Government Senior Executive Service (SES) for sustained extraordinary accomplishments on a national or international level.

Sanjit Seshia
University of California Berkeley

Title: Verified Artificial Intelligence and Autonomy

Abstract: Verified artificial intelligence (AI) is the goal of designing AI-based systems that have strong, verified assurances of correctness with respect to mathematically-specified requirements. This goal is particularly important for autonomous and semi-autonomous systems. In this talk, I will consider Verified AI from a formal methods perspective and with a special focus on autonomy. I will describe the challenges for and recent progress towards attaining Verified AI, with examples from the domain of intelligent cyber-physical systems, with a particular focus on autonomous vehicles and aerospace systems.

Bio : Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, and the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award. He is a Fellow of the IEEE.

Vandi Verma
NASA Jet Propulsion Laboratory (JPL)

Title: Operable NASA Robots on Mars and Beyond

Abstract: The talk will provide an overview of Mars rovers and the challenges with developing operable space robots.

Bio: Vandi Verma leads the Operable Robotics group in the Mobility and Robotic Systems Section at NASA Jet Propulsion Laboratory. She has developed software for and operated multiple rovers on Mars and has worked on research rovers deployed in the Arctic, Antarctic and the Atacama. Vandi's interests include space robotics, autonomy, and operability. She is currently working on robotic arm and sample caching algorithms and flight software for the Mars 2020 Perseverance rover and is the software architect for the Europa Lander advanced autonomy prototype. She has a Ph.D. in Robotics from Carnegie Mellon University.

First Gov logo
NASA Logo -