Program

All times are Central European Time

DAY 1 Wednesday 8 December 2021

12:00-13:15 Opening and Keynote 1
     Chair: Radu Calinescu and Corina Pasareanu

12:00-12:15 SEFM 2021 Opening
12:15-13:15 RoboWorld: where can my robot work?
      Ana Cavalcanti, University of York, UK

13:15-13:40 Break

13:40-15:10 Session 1: Run-time Analysis and Testing
      Chair: Colin Paterson

13:40-14:00 Runtime Enforcement with Reordering, Healing, and Suppression
        Yliès Falcone and Gwen Salaün
14:00-14:20 Monitoring First-Order Interval Logic
        Klaus Havelund, Moran Omer and Doron Peled
14:20-14:40 Exhaustive Property Oriented Model-based Testing With Symbolic Finite State Machines
        Niklas Krafczyk and Jan Peleska
14:40-14:55 nfer - A Tool for Event Stream Abstraction (Tool Paper)
        Sean Kauffman
14:55-15:10 Mining Shape Expressions with ShapeIt (Tool Paper)
        Ezio Bartocci, Jyotirmoy Deshmukh, Cristinel Mateis, Eleonora Nesterini,
        Dejan Nickovic and Xin Qin

15:10-15:30 Break

15:30-16:50 Session 2: Security & Privacy
      Chair: Paolo Masci

15:30-15:50 Refining Privacy-Aware Data Flow Diagrams
        Hanaa Alshareef, Sandro Stucki and Gerardo Schneider
15:50-16:10 Hybrid Information Flow Control for Low-level Code
        Eduardo Geraldo, Jose Fragoso Santos and João Costa Seco
16:10-16:30 Upper Bound Computation of Information Leakages for Unbounded Recursion
        Johannes Bechberger and Alexander Weigl
16:30-16:50 On the Security and Safety of AbU Systems
        Michele Pasqua and Marino Miculan

Day 2 Thursday 9 December 2021

12:00-13:00 Keynote 2
      Chair: Radu Calinescu

12:00-13:00 Controller synthesis for Adaptive Mobile Robots. Abstractions, all change!?
        Sebastian Uchitel, University of Buenos Aires, Argentina;
        and Imperial College London, UK

13:00-13:30 Break

13:30-15:05 Session 3: Parallel Composition/CSP and Probabilistic Reasoning
      Chair: Mario Gleirscher

13:30-13:50 Parallelized sequential composition and hardware weak memory models
        Robert Colvin
13:50-14:10 Checking Opacity and Durable Opacity with FDR
        Brijesh Dongol and Jay Le-Papin
14:10-14:30 Translation of CCS into CSP, Correct up toStrong Bisimulation
        Gerard Ekembe Ngondi, Vasileios Koutavas and Andrew Butterfield
14:30-14:50 Probabilistic BDI Agents: Actions, Plans, and Intentions
        Blair Archibald, Muffy Calder, Michele Sevegnani and Mengwei Xu
14:50-15:05 A Debugger for Probabilistic Programs (Tool Paper)
        Alexander Hoppen and Thomas Noll

15:05-15:25 Break

15:25-17:00 Session 4: Verification & Synthesis
      Chair: Marie-Christine Jakobs

15:25-15:45 Verification of Programs with Exceptions through Operator-Precedence Automata
        Francesco Pontiggia, Michele Chiari and Matteo Pradella
15:45-16:05 Counterexample Classification
        Cole Vick, Eunsuk Kang and Stavros Tripakis
16:05-16:25 Be Lazy and Don’t Care: Faster CTL Model Checking for Recursive State Machines
        Clemens Dubslaff, Patrick Wienhöft and Ansgar Fehnker
16:25-16:45 Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL synthesis
        Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari and Stefano Tonetta
16:45-17:00 TACoS: A Tool for the MTL Controller Synthesis Problem (Tool Paper)
        Till Hofmann and Stefan Schupp

Day 3 Friday 10 December 2021

12:00-13:20 Session 5: Emerging Domains
      Chair: Hans de Nivelle

12:00-12:20 Lightweight Nontermination Inference with CHCs
        Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. Stuckey
12:20-12:40 A Denotational Semantics of Solidity in Isabelle/HOL
        Diego Marmsoler and Achim D. Brucker
12:40-13:00 Configuration Space Exploration for Digital Printing Systems
        Jasper Denkers, Marvin Brunner, Louis van Gool and Eelco Visser
13:00-13:20 Bit-precise Verification of Discontinuity Errors Under Fixed-point Arithmetic
        Stella Simic, Omar Inverso and Mirco Tribastone

13:20-13:40 Break

13:40-14:40 Session 6: Machine Learning and Cyber Physical Systems
      Chair: Heike Wehrheim

13:40-14:00 OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks
        Vahid Hashemi, Panagiotis Kouvaros and Alessio Lomuscio
14:00-14:20 Active Model Learning of Stochastic Reactive Systems
        Martin Tappler, Edi Muškardin, Bernhard K. Aichernig and Ingo Pill
14:20-14:40 Mixed-Neighborhood, Multi-Speed Cellular Automata for Safety-Aware Pedestrian Prediction
        Sebastian Vom Dorff, Chih-Hong Cheng, Hasan Esen and Martin Fränzle

14:40-15:00 Break

15:00-16:00 Keynote 3
      Chair: Corina Pasareanu

15:00-16:00 On Safety, Assurance and Reliability: A Software Engineering Perspective
        Marsha Chechik, University of Toronto, Canada

16:00-16:20 Best Paper Awards and Closing Remarks