Program
The conference will take place in-person-only at Humboldt-University in Berlin-Adlershof.
DAY 1 Wednesday 28 September 2022
09:00-09:45 Invited Talk: Distributed Process Calculi with Local States
Uwe Nestmann
10:00-12:00 Session 1: Software Verification
10:00-10:40
A Unifying Approach for Control-Flow-Based Loop Approximation
Dirk Beyer, Marian Lingsch and Martin Spiessl
10:40-11:20
Auto-active Verification of Floating-point Programs via Nonlinear Real Provers
Junaid Rasheed and Michal Konečný
11:20-12:00
Runtime Verification of Autonomous Systems with Imperfect Information (moved from Session 8)
Angelo Ferrando and Vadim Malvone
12:00-13:00 Break
13:00-15:00 Session 2: Program Analysis
13:00-13:40
A Query Language for Language Analysis
Matteo Cimini
13:40-14:20
Field-Sensitive Program Slicing
Carlos Galindo, Jens Krinke, Josep Silva and Sergio Perez Rubio
14:20-15:00
SPouT: Symbolic Path Recording during Testing - a Concolic Executor for the JVM
Malte Mues, Falk Howar and Simon Dierl
15:00-15:30 Break
15:30-17:30 Session 3: Verifier Technology
15:30-16:10
Cooperation between Automatic and Interactive Software Verifiers
Dirk Beyer, Martin Spiessl and Sven Umbricht
16:10-16:50
Strategy Switching: Smart Fault-tolerance for Weakly-hard Resource-constraint Real-time Applications
Lukas Miedema and Clemens Grelck
16:50-17:30
A Java Program Slicer (System demo - Tool paper)
Carlos Galindo, Sergio Perez Rubio and Josep Silva
DAY 2 Thursday 29 September
09:00-09:45 Invited Talk: Maintenance Meets Model Checking: Predictive Maintenance via Fault Trees and Formal Methods
Mariëlle Stoelinga
10:00-12:00 Session 4: Formal Methods for Intelligent and Learning Systems
10:00-10:40
Constrained Training of Recurrent Neural Networks for Automata Learning
Bernhard K. Aichernig, Sandra König, Cristinel Mateis, Andrea Pferscher, Dominik Schmidt and Martin Tappler
10:40-11:20
Neural Network Verification using Residual Reasoning
Yizhak Elboher, Elazar Cohen and Guy Katz
11:20-12:00
Training Agents to Satisfy Timed and Untimed Signal Temporal Logic Specifications with Reinforcement Learning
Nathaniel Hamilton, Preston K Robinette and Taylor T Johnson
12:00-13:00 Break
13:00-15:00 Session 5: Specification and Contracts
13:00-13:40
Information Flow Control-by-Construction for an Object-Oriented Language
Tobias Runge, Alexander Kittelmann, Marco Servetto, Alex Potanin and Ina Schaefer
13:40-14:20
Specification is Law: Safe Deployment of Ethereum Smart Contracts
Pedro Antonino, Juliandson Ferreira, Augusto Sampaio and Bill Roscoe
14:20-15:00
SKLEE: A Dynamic Symbolic Analysis Tool for Ethereum Smart Contracts
Namrata Jain, Kosuke Kaneko and Subodh Sharma
15:30-17:00 Excursion
DAY 3 Friday 30 September
09:00-09:45 Invited Talk: Towards Verifying Neural-symbolic Multi-agent Systems
Alessio Lomuscio
10:00-12:00 Session 6: Program Synthesis
10:00-10:30
Weighted Games for User Journeys
Paul Kobialka, Silvia Lizeth Tapia Tarifa, Gunnar Rye Bergersen and Einar Broch Johnsen
10:40-11:20
Safety Controller Synthesis for a Mobile Manufacturing Cobot
Ioannis Stefanakos, Radu Calinescu, James Douthwaite, Jonathan Aitken and James Law
11:20-12:00
Timely specification repair for Alloy 6
Jorge Cerqueira, Alcino Cunha and Nuno Macedo
12:00-13:00 Break
13:00-14:20 Session 7: Temporal Logic
13:00-13:40
BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees
Bernard Serbinowski and Taylor T Johnson
13:40-14:20
CHA: Supporting SVA-like Assertions in Formal Verification of Chisel Programs
Shizhen Yu, Yifan Dong, Jiuyang Liu, Yong Li, Zhilin Wu, David N. Jansen and Lijun Zhang
14:20-14:50 Break
14:50-16:10 Session 8: Runtime Methods
14:50-15:30
Information Exchange between Over- and Underapproximating Software Analyses (moved from Session 1)
Jan Haltermann and Heike Wehrheim
15:30-16:10
Runtime Enforcement of IEC 61499 Applications
Irman Faqrizal, Gwen Salaün and Yliès Falcone