Saturday, November 20

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:00Introduction (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 (pdf)
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 (pdf)
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 (pdf)
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 (pdf)
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 (pdf)
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)

Sunday, November 21

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 (pdf)
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 (pdf)
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 (pdf)
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 (pdf)
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 (pdf)
Adam Petz, Perry Alexander and Grant JurgensenPresenter: Adam Petz
00:30-01:00 17:30-18:00 08:30-09:00Break
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]

Monday, November 22

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:30Modeling 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 (pdf)
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 (pdf)
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 (pdf)
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 (pdf)
Felix Freiberger, Stefan Schupp, Holger Hermanns and Erika ÁbrahámPresenter: Felix Freiberger
00:15-00:30 17:15-17:30 08:15-08:30 Sampling of Shape Expressions with ShapeEx (pdf)
Nicolas Basset, Thao Dang, Felix Gigler, Cristinel Mateis and Dejan NickovicPresenter: Felix Gigler
00:30-01:00 17:30-18:00 08:30-09:00Break
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