ICTAC 2020 Keynote Speakers

Klaus Havelund (Jet Propulsion Laboratory, California Institute of Technology, USA)

A Flight Rule Checker for the LADEE Lunar Spacecraft

Watch the keynote
As part of the design of a space mission, an important part is the design of so-called *flight rules*. Flight rules express constraints on various parts and processes of the mission, that if followed, will reduce the risk of failure. One such set of flight rules constrain the format of *command sequences* regularly (e.g. daily) sent to the spacecraft to control its next near term behavior. We present a high-level view of the automated flight rule checker FRC for checking command sequences sent to NASA’s LADEE Lunar mission spacecraft, used throughout its entire mission. A command sequence is in this case essentially a program (a sequence of commands) with no loops or conditionals, and it can therefore be verified with a trace analysis tool. FRC is implemented using the TraceContract runtime verification tool, an internal Scala DSL for checking event sequences against "formal specifications". The paper illustrates this untraditional use of runtime verification in a real context, with strong demands on the expressiveness and flexibility of the specification language, illustrating the advantages of an internal DSL.

Klaus Havelund is a Senior Research Scientist at the Laboratory for Reliable Software (LaRS), Jet Propulsion Laboratory (JPL), California Institute of Technology. He received his Ph.D degree in Computer Science from the University of Copenhagen, Denmark, in 1994, partly conducted at Ecole Normale Superieure, Paris, France. He has worked with formal methods more than 3 decades, and at NASA for more than two decades. His current research interests include runtime verification and development of embedded software systems in high-level programming languages. He is known for his earlier work on the Java PathFinder model checker for Java, and he was part of the RAISE project (Rigorous Approach to Industrial Software Engineering) which developed the RSL wide spectrum specification language. Other work areas include theorem proving and model checking.


Marieke Huisman (University of Twente, the Netherlands)

Teaching Software Verification using Snap!

Watch the keynote
With the progress in deductive program verification research, new tools and techniques have become available to reason about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. Therefore, in this presentation, we show how we developed program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We support both static and dynamic verification of Snap! programs. Moreover, we also outline how program verification in Snap! could be introduced to high school students in a classroom situation.

Marieke Huisman is a professor in Software Reliability at the University of Twente, leading the Formal Methods and Tools group. She is well-known for her work on program verification of concurrent software. In 2011, she obtained an ERC Starting Grant, which she used to start development of the VerCors verifier, a tool for the verification of concurrent software. Currently, as part of her NWO personal VICI grant Mercedes, she is working on further improving verification techniques, both by enabling the verification of a larger class of properties, and by making verification more automatic. A main characteristic of the VerCors verifier is that it can reason about different kinds of concurrent programs. In particular, VerCors was originally developed to reason about Java programs, but it can also be used to reason about OpenCL kernels (for GPU), or to prove that compiler directives for parallelisation, such as in OpenMP, are correct.


Naijun Zhan (State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, China)

Taming delays in cyber-physical systems

Watch the keynote
With the rapid development of feedback control, sensor techniques and computer control, time delay has become an essential feature of cyber-physical systems (CPSs), underlying both the continuous evolution of physical plants and the discrete transition of computer programs, which may well annihilate the stability/safety certificate and control performance of CPSs. In the safety-critical context, automatic verification and synthesis methods addressing time-delay in CPSs should therefore abound. However, surprisingly, they do not, although time-delay has been extensively studied in the literature of mathematics and control theory from a qualitative perspective. In this talk, we will report our recent efforts to tackle these issues, including controller synthesis for time-delayed systems in the setting of discrete time, bounded and unbounded verification of delay differential equations, and discuss remaining challenges and future trends.

Naijun Zhan is a research professor of Institute of Software Chinese Academy of Sciences (ISCAS). He got his bachelor degree and master degree both from Nanjing University, and his PhD from ISCAS. Prior to join ISCAS, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, concurrent computation models, modal and temporal logics, and so on. He is in the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, and Journal of Computer Research and Development, a member of the steering committees of SETTA and MEMOCODE. He published more than 100 papers in international leading journals and conferences, 2 books and 4 book chapters, and edited 4 conference proceedings and 2 journal special issues. See lcs.ios.ac.cn/~znj/ for more details.