Dines Bjørner
Prof. emeritus, Dr.techn., Dr.h.c.
Technical University of Denmark
Receiver of FME's 2021 Fellowship award
Technical University of Denmark
Receiver of FME's 2021 Fellowship award
- An Essence of Domain Engineering - A Basis for Trustworthy Aeronautics and Space Software
- Before software can be designed one must have a reasonable grasp of its requirements. Before requirements can be prescribed one must have a reasonable grasp of the domain in which the software is to serve. So we must study, analyse and describe the application domain. We shall argue that domain science & engineering is a necessary prerequisite for requirements engineering. We survey elements of domain science & engineering -- and exemplify some elements of domain descriptions. We finally speculate on the relevance of domain engineering in the context of aeronautics and [outer] space.
- About the speaker: Dines Bjørner was born in 1937, and is a Danish citizen. He received his M.Sc. and PhD from the Technical University of Denmark, 1962 and 1969. He worked for IBM Sweden, IBM USA, and IBM Austria 1962-1975. Subsequently University of Copenhagen 1975-1976 as Guest Professor, and Technical University of Denmark 1976-2007 as Professor. He created Dansk Datamatik Center (DDC), of which he was Scientific Director, 1979-1989. He founded the United Nations University's International Institute for Software Technology, of which he was Director, 1991-1997. He was co-creator of VDM, the Vienna Development Method, and instigator of RAISE: Rigorous Approach to Industrial Software Engineering. He led the first European DoD validated Ada compiler project & product. He has written 7 books, and more than 120 papers. He is Knight of the Danish order of Dannebrog, knighted by the Danish Queen. He has received the Hungarian John von Neumann medal, and the Masaryk University Gold Medal. He is member of Academia Europaea, the Danish Academy of Technology and Science, member of the Russian Academy of Natural Sciences, ACM Fellow, IEEE Fellow, and in 2021 became FME Fellow.
Steve Chien
Senior Research Scientist
Supervisor of the Artificial Intelligence Group
Jet Propulsion Laboratory
Supervisor of the Artificial Intelligence Group
Jet Propulsion Laboratory
- Formal Methods for Trusted Space Autonomy, Boon or Bane?
- Trusted Space Autonomy is challenging in that space systems are complex artifacts deployed in a high stakes environment with complicated operational settings. Thus far these challenges have been met using the full arsenal of tools: formal methods, informal methods, testing, runtime techniques, and operations processes. Using examples from previous deployments of autonomy to the Autonomous Sciencecraft on EO-1, WATCH on MER, IPEX, AEGIS on MER, MSL, and M2020, and the M2020 Onboard planner, I provide examples of how each of these approaches have been used to enable successful deployment of autonomy. I then focus on relatively limited use of formal methods (both prior to deployment and runtime methods). From the needs perspective, formal methods represent the best chance for reliable autonomy as testing, informal methods, and operations accommodations do not scale well with increasing complexity of the autonomous system. However from the practice perspective, formal methods have been limited in their application due to difficulty in eliciting formal specifications and challenges in representing complex constraints such as metric time and resources. I will discuss some of these challenges as well as the opportunity to extend formal and informal methods into runtime validation systems.
- About the speaker: Dr. Steve Chien is a JPL Fellow, Senior Research Scientist, and Head of the Artificial Intelligence Group, at the Jet Propulsion Laboratory, California Institute of Technology. He has led the deployment of AI software to a wide range of missions including: Autonomous Sciencecraft on EO-1, Earth Observing Sensorweb, WATCH on MER, IPEX, ESA’s Rosetta, ECOSTRESS, and OCO-3. He is currently supporting the development of an onboard scheduler for the Mars 2020 rover mission as well as formulating future AI-driven space mission concepts. Dr. Chien has received numerous awards for these efforts. In 1995 he received the Lew Allen Award for Excellence. He has been recognized four times in the NASA Software of the Year competition (1999, 1999, 2005, and 2011). He has received four NASA Medals for his work in AI for Space (1997, 2000, 2007, 2015). In 2011 He was awarded the inaugural AIAA Intelligent Systems Award, for his contributions to Spacecraft Autonomy. In 2015 He was awarded a JPL Magellan Award as well as the NASA Exceptional Achievement Medal for his contributions to automated science scheduling for ESA's Rosetta mission. Dr. Chien has supported the Office of the Secretary of Defense, the Defense Sciences Board studies on Autonomy, and 2018-2021 he served as commissioner on the National Security Commission on Artificial Intelligence.
Daniel Jackson
Professor of Computer Science
MIT CSAIL
MIT CSAIL
- Concept Design Moves. Or: How to Become a Great Software Designer
- Why are some apps so much better than others, and some designers so much more successful? For the last decade or so, I’ve been trying to answer this question. My approach has been to study hundreds of popular apps, identifying good and bad parts, and then looking for a way to codify this knowledge so that anyone can use it to become a better designer. In this talk, I’ll explain some of the key ideas I came up with: (a) concepts: a way to define the experience of using an app in modular terms, and a basis for codifying common patterns, and (b) design moves: some archetypal moves that software designers make to improve their designs. Most of the examples and ideas will be drawn from my recently published book, The Essence of Software.
- About the speaker: Daniel Jackson is professor of computer science at MIT, and associate director of CSAIL. For his research in software, he won the ACM SIGSOFT Impact Award, the ACM SIGSOFT Outstanding Research Award and was made an ACM Fellow. He is the lead designer of the Alloy modeling language, and author of Software Abstractions: Logic, Language and Analysis (2006). He chaired a National Academies study on software dependability, and has collaborated on software projects with NASA on air-traffic control, with Massachusetts General Hospital on proton therapy, and with Toyota on autonomous cars.
Julia Lawall
Senior Research Scientist
Inria-Paris
Inria-Paris
- The Coccinelle C-program matching and transformation tool
- Coccinelle is a program matching and transformation tool for C code that was originally directed towards modernizing Linux kernel device drivers. It is based on a patch-like syntax for describing matching and transformation rules that is intended to be expressive but easy for Linux kernel developers to learn to use. Over 9000 patches in the Linux kernel have used Coccinelle, and it is used by some other projects such as wine, systemd, and git, to search for bug patterns or make widespread changes in the code base. In this talk, we will give an overview of the use of Coccinelle, examine the main design decisions, and illustrate its impact.
- About the Speaker: Julia Lawall is a Senior Research Scientist (Directrice de Recherche) in the Whisper group at Inria-Paris. She also participates in the IRILL. Her current research focuses on the design and implementation of domain-specific languages, mostly targetting problems in operating systems. She have also worked on partial evaluation, optimal reduction of the lambda calculus and continuations.
Sriram Sankaranarayanan
Professor of Computer Science
University of Colorado Boulder
University of Colorado Boulder
- Are we there yet? Reachability Analysis for Cyber-Physical Systems
- Reachability analysis is a fundamental verification problem that decides if a system initialized within some given set of initial states can reach a designated "unsafe" set of states. This problem is of central importance to the field of formal verification, especially for cyber-physical systems that combine continuous and discrete dynamics. In this talk, we will provide a historical overview focused on reachability analysis techniques for cyber-physical systems, beginning with a description of current techniques and how they have evolved over the past three decades. We will highlight some successful applications to verify the safety of important applications in areas such as robotics, autonomous vehicles, medical devices and space systems. Reachability analysis continues to be a fertile area of research. We will describe some recent developments such as the use of decompositions to speed up reachability computations, data-driven approaches for reachability analysis, reachability analysis for neural networks and reachability analysis used for providing real-time warnings of impending failures during deployment. We will conclude with a discussion of some open challenges in this area for the upcoming decades.
- About the Speaker: Sriram Sankaranarayanan is a professor of Computer Science at the University of Colorado Boulder. His research interests include automatic techniques for reasoning about the behavior of computer and cyber-physical systems. Sriram obtained a PhD in 2005 from Stanford University where he was advised by Zohar Manna and Henny Sipma. Subsequently he worked as a research staff member at NEC research labs in Princeton, NJ where he contributed to the F-Soft software verification project for C/C++ programs. He has been on the faculty at CU Boulder since 2009. Sriram has been the recipient of awards including the Siebel Scholarship (2005), CAREER award from NSF (2009) and various awards for teaching and research at CU Boulder.
Alex Summers
Associate Professor
University of British Columbia
University of British Columbia
- The Prusti Project: Formal Verification for Rust
- Rust is a modern systems programming language designed to offer both performance and static safety. A key distinguishing feature of Rust is its strong type system, enforcing by default that memory is either shared or mutable, but never both. This guarantee is used to prevent common pitfalls such as memory errors and data races. We developed the Prusti verifier for Rust, demonstrating that it this guarantee can also be exploited to greatly simplify formal verification, enabling verification of rich correctness properties of Rust programs with a very modest annotation overhead. In this talk I’ll provide an overview of the Prusti project: our main design goals, what we have achieved and what we learned so far. I’ll explain some important outcomes from the three key perspectives of a Prusti user, a verification expert, and a tool developer.
- About the Speaker: Alex Summers is an Associate Professor of Computer Science at the University of British Columbia (UBC). Prior to moving to UBC he worked at ETH Zurich as a senior researcher in the Chair of Programming Methodology group run by Peter Müller. Alex works the general area of program correctness, including developing new specification and verification logics and type systems, and developing automated tools for constructing proofs about heap-based and concurrent programs, usually building on SMT solvers. He co-ordinated the Viper project for several years, and also started the Prusti project presented in this talk. Alex is broadly interested in software verification for a wide variety of concurrent and imperative programming paradigms, and has been awarded the 2015 Dahl-Nygaard Junior Prize for his work in these areas.
Emina Torlak
Associate Professor
Paul G. Allen School of Computer Science & Engineering
University of Washington
Paul G. Allen School of Computer Science & Engineering
University of Washington
- Solver-Aided Programming for All
- Solver-aided tools have automated the verification and synthesis of practical programs in many domains, from high-performance computing to executable biology. These tools work by reducing verification and synthesis tasks to satisfiability queries, which involves compiling programs to logical constraints. Developing an effective symbolic compiler is challenging, however, and until recently, it took years of expert work to create a solver-aided tool for a new domain. This talk presents Rosette, a programming language for rapid creation of solver-aided tools. To build a new tool, you write an interpreter for the tool's input language, and Rosette lifts this interpreter into a symbolic compiler. The lifting is made possible by Rosette's symbolic virtual machine, which can translate both a language implementation and programs in that language to efficient constraints. Since its first public release in 2014, Rosette has enabled a wide range of programmers, from professional developers to high school students, to create over 30 new verification and synthesis tools. Example applications include verifying radiation therapy software in current clinical use, synthesizing GPU kernels, and verifying and synthesizing just-in-time compilers that are part of the Linux operating system. This talk will provide a brief introduction to Rosette and describe recent applications.
- About the Speaker: Emina Torlak is an Associate Professor in the Paul G. Allen School of Computer Science & Engineering at the University of Washington, and a visiting researcher at Amazon Web Services. She works on new languages and tools for computer-aided design, verification, and synthesis of software. She received her Bachelors (2003), Masters (2004), and Ph.D. (2009) degrees from MIT, and subsequently worked at IBM Research, LogicBlox, and as a research scientist at U.C. Berkeley. Emina is the creator of the Kodkod solver, which has been used in over 70 academic and industrial tools for software engineering. Her work on the Rosette system integrates solvers into programming languages, enabling programmers to create their own solver-aided tools for all kinds of systems, from radiotherapy machines to automated algebra tutors. Emina is a recipient of the Robin Milner Young Researcher Award (2021), NSF CAREER Award (2017), Sloan Research Fellowship (2016), and the AITO Dahl-Nygaard Junior Prize (2016).
Edwin Brady
Reader
Computer Science
University of St. Andrews
Computer Science
University of St. Andrews
- Total Functional Programming with Idris 2 (Tutorial)
- About the Speaker: Edwin Brady is a Reader in Computer Science at the University of St Andrews, interested in making state of the art programming language techniques accessible to sofware developers and practitioners. This involves type theory, dependently typed functional programming, compilers and metaprogramming. He is currently working on a new implementation of Idris, a dependently typed functional programming language.
Ankush Desai
Senior Applied Scientist
Amazon Web Services
Amazon Web Services
- Formally Reasoning about Distributed Systems using P (Tutorial)
- P is a state machine based programming language for modeling and specifying complex distributed systems. P allows programmers to model their system as a collection of communicating state machines. P supports several backend analysis engines (based on automated reasoning techniques like model checking and symbolic execution) to check that the distributed system modeled in P satisfies the desired correctness specifications. Not only can a P program be systematically tested (e.g., model checking), but it can also be compiled into executable code. Essentially, P unifies modeling, specifying, implementing, and testing into one activity for the programmer. P is currently being used extensively inside Amazon (AWS) for analysis of complex distributed systems. P is also being used for programming safe robotics systems. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone.
- About the Speaker: Ankush Desai is a senior applied scientist in the automated reasoning group at Amazon. He works on applying formal methods techniques like model checking and systematic testing to reason about the correctness of distributed systems. He graduated with a PhD in computer science from UC, Berkeley (2019), co-advised by Prof. Sanjit Seshia and Dr. Shaz Qadeer. Before joining graduate school, he spent 2+ years working at Microsoft Research, India with Sriram Rajamani. During his time at IIT, Kanpur, he was part of the team that built the first Indian Nano-Satellite JUGNU. The satellite was successfully launched on 12 October, 2011 . He was head of the On-Board Computers team managing all the software framework for the satellite.
Anastasia Mavridou
Research Computer Scientist
KBR Inc / NASA Ames Research Center
KBR Inc / NASA Ames Research Center
- Capturing and Analyzing Requirements with FRET (Tutorial)
- FRET is an open source tool, developed at NASA Ames, for writing, understanding, formalizing, and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. FRET helps users write FRETish requirements both by providing grammar information and examples during editing, but also through English and diagrammatic explanations to clarify subtle semantic issues. For each requirement, FRET automatically produces formalizations and supports interactive simulation of produced formalizations to ensure that they capture user intentions. Through its analysis portal, FRET connects to analysis tools by exporting verification code. Currently FRET connects to (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs. FRET also supports the consistency/realizability analysis of requirements for identifying conflicting requirements. In this tutorial, we introduce FRET and learn to speak and analyze FRETish through several examples.
- About the Speaker: Anastasia Mavridou is a member of the Robust Software Engineering (RSE) Group at NASA Ames Research Center, employed by KBR Inc, where she performs research on formal methods and software engineering. More specifically, she works on the NASA Ames' Formal Requirements Elicitation Tool (FRET) and her research focuses on requirements engineering, component-based system design, and compositional verification. Before joining RSE, she worked as a postdoc with Prof. Janos Sztipanovits at the Institute for Software Integrated Systems, Vanderbilt University, USA. She received my PhD in December 2016 from École polytechnique fédérale de Lausanne (EPFL), Switzerland, supervised by Prof. Joseph Sifakis and Dr. Simon Bliudze. She has authored more than 25 publications spanning the broad areas of formal methods and software engineering, with a focus on system design and formal analysis techniques. She have also served on the program committees of numerous workshops and conferences in those areas, including being the general chair of the NASA Formal Methods (NFM) 2020 symposium.
Leonardo de Moura
Senior Principal Researcher
Microsoft Research
Microsoft Research
Sebastian Ullrich
PhD Student
Karlsruhe Institute of Technology, Germany
Karlsruhe Institute of Technology, Germany
- An Introduction to the Lean 4 theorem prover and programming language (Tutorial)
- Lean 4 is an implementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom-proof automation procedures in Lean itself. In this tutorial, we introduce the Lean theorem prover with examples and describe some of its applications.
- About the Speakers: Leonardo de Moura
is a Senior Principal Researcher at Microsoft in the
RiSE group. He joined Microsoft in 2006, and before
that, he was a Computer Scientist at SRI
International. He works with theorem proving and
automated reasoning. In 2010, he received the Haifa
Verification Award for his work on automated
reasoning. In 2014, one of his articles, “Z3: an
efficient SMT solver,” was nominated as the most
influential tool paper in the first 20 years of
TACAS. In 2015, Z3 received the Programming Languages
Software Award from the ACM. He received the Herbrand
award in 2019 to recognize his numerous and vital
contributions to SMT solving, including its theory,
implementation, and application to a wide range of
academic and industrial needs. He received the CAV
award in 2021 for his contributions to SMT solving.
His current project, the Lean theorem prover, has
been featured in many popular science magazines,
including Wired, Quanta, Nature, BigThink, to cite a
few.
Sebastian Ullrich is a PhD student in the programming paradigms group at the Karlsruhe Institute of Technology, Germany. His PhD topic is on an extensible frontend for the Lean 4 theorem prover, which he has been collaborating on together with Leonardo de Moura since 2018. His research interests are in language design, macro systems, and program verification.