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 A Denotational Semantics of Solidity in Isabelle/HOL
Diego Marmsoler and Achim D. Brucker
12:20-12:40 Lightweight Nontermination Inference with CHCs
Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. Stuckey
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