| Beijing Time (+8:00 UTC) |
Amsterdam Time (+1:00 UTC) |
San Francisco Time (-8:00 UTC) | Event |
|---|---|---|---|
| 22:30-23:00 | 15:30-16:00 | 6:30-07:00 | Introduction (S. Arun-Kumar, Indranil Saha, Lijun Zhang) |
| 23:00-00:30 | 16:00-17:30 | 07:00-08:30 | Modeling and Verification of Hardware Systems (Chair: Lijun Zhang) |
| 23:00-23:20 | 16:00-16:20 | 07:00-07:20 | Polynomial Word-Level Verification of Arithmetic Circuits
Mohammed Barhoush, Alireza Mahzoon and Rolf Drechsler Presenter: Alireza Mahzoon |
| 23:20-23:40 | 16:20-16:40 | 07:20-07:40 | Simplification of numeric variables for PLC model checking
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Jean-Charles Tournier, Juan A. Rodriguez-Aguilar
and Enrique Blanco Viñuela Presenter: Ignacio D. Lopez-Miguel |
| 23:40-00:00 | 16:40-17:00 | 07:40-08:00 | LION: Real-Time I/O Transfer Control for Massively Parallel Processor Arrays
Dominik Walter and Jürgen Teich Presenter: Dominik Walter |
| 00:00-00:15 | 17:00-17:15 | 08:00-08:15 | SEESAW: A Tool for Detecting Memory Vulnerabilities in Protocol Stack Implementations
Farhaan Fowze and Tuba Yavuz Presenter: Tuba Yavuz |
| 00:15-00:30 | 17:15-17:30 | 08:15-08:30 | Formal Modelling of attack scenarios and mitigation strategies in IEEE 1588
Kelvin Anto, Partha Roop and Akshya Swain Presenter: Kelvin Anto |
| 00:30-01:00 | 17:30-18:00 | 08:30-09:00 | Break |
| 01:00-02:00 | 18:00-19:00 | 09:00-10:00 | Keynote Talk: Synthesizing Correct and Optimal Control Programs using Model Checking and Machine Learning Kim Guldstrand Larsen, Aalborg University (Session Chair: Indranil Saha) |
| Beijing Time (+8:00 UTC) |
Amsterdam Time (+1:00 UTC) |
San Francisco Time (-8:00 UTC) | Event |
|---|---|---|---|
| 23:00-00:30 | 16:00-17:30 | 07:00-08:30 | Modeling and Verification of Software Systems (Chair: Holger Hermanns) |
| 23:00-23:20 | 16:00-16:20 | 07:00-07:20 | Enforcement FSMs - Specification and Verification of Non-Functional Properties of Program Executions
on MPSoCs
Khalil Esper, Stefan Wildermann and Jürgen Teich Presenter: Khalil Esper |
| 23:20-23:40 | 16:20-16:40 | 07:20-07:40 | Translating Structured Sequential Programs to Dataflow Graphs
Klaus Schneider Presenter: Klaus Schneider |
| 23:40-00:00 | 16:40-17:00 | 07:40-08:00 | Verified functional programming of an IoT operating system's bootloader
Shenghao Yuan and Jean-Pierre Talpin Presenter: Shenghao Yuan |
| 00:00-00:15 | 17:00-17:15 | 08:00-08:15 | Translation of Continuous Function Charts to Imperative Synchronous Quartz Programs
Marcel Christian Werner and Klaus Schneider Presenter: Marcel Christian Werner |
| 00:15-00:30 | 17:15-17:30 | 08:15-08:30 | Design and Formal Verification of a Copland-based Attestation Protocol
Adam Petz, Perry Alexander and Grant Jurgensen Presenter: Adam Petz |
| 00:30-01:00 | 17:30-18:00 | 08:30-09:00 | Break | 01:00-02:30 | 18:00-19:30 | 09:00-10:30 | Q/A Session Title: If you're Not Writing a Program Don't Use a Programming Language (Session Chair: Dominique Mery) Leslie Lamport, Microsoft Leslie Lamport invites attendees of its Q/A session to watch his
recorded talk entitled "If you're Not Writing a Program Don't Use a
Programming Language" ; any attendee of the Q/A session should watch
one of the two slightly different versions of that talk on video:
One given at the National University of Singapore in January 2020 It's
at [1]
One given at the 2018 Heidelberg Laureate Forum in September at
[2]
|
| Beijing Time (+8:00 UTC) |
Amsterdam Time (+1:00 UTC) |
San Francisco Time (-8:00 UTC) | Event |
|---|---|---|---|
| 23:00-00:30 | 16:00-17:30 | 07:00-08:30 | Modeling and Verification of Cyber-Physical Systems (Chair: Sven Schewe) |
| 23:00-23:20 | 16:00-16:20 | 07:00-07:20 | Learning Optimal Decisions for Stochastic Hybrid Systems
Mathis Niehage, Arnd Hartmanns and Anne Remke Presenter: Mathis Niehage |
| 23:20-23:40 | 16:20-16:40 | 07:20-07:40 | A Secure Insulin Infusion System using Verification Monitors
Abhinandan Panda, Srinivas Pinisetty and Partha Roop Presenter: Abhinandan Panda |
| 23:40-00:00 | 16:40-17:00 | 07:40-08:00 | Online Monitoring of Spatio-Temporal Properties for Imprecise Signals
Ennio Visconti, Ezio Bartocci, Michele Loreti and Laura Nenzi Presenter: Ennio Visconti |
| 00:00-00:15 | 17:00-17:15 | 08:00-08:15 | Controller Verification meets Controller Code: A Case Study
Felix Freiberger, Stefan Schupp, Holger Hermanns and Erika Ábrahám Presenter: Felix Freiberger |
| 00:15-00:30 | 17:15-17:30 | 08:15-08:30 | Sampling of Shape Expressions with ShapeEx
Nicolas Basset, Thao Dang, Felix Gigler, Cristinel Mateis and Dejan Nickovic Presenter: Felix Gigler |
| 00:30-01:00 | 17:30-18:00 | 08:30-09:00 | Break |
| 01:00-02:00 | 18:00-19:00 | 09:00-10:00 | Keynote Talk: Domain-Specific Reasoning with Satisfiability Modulo Theories Clark Barrett, Stanford University (joint with FM) |
| 02:00-02:30 | 19:00-19:30 | 10:00-10:30 | Concluding Remarks |