| Day 1: May 4, 2023 |
|
IRST
|
CEST
| |
|
10:45 - 11
|
9:15 - 9:30
|
Welcome:
Pejman Lotfi-Kamran (Head of the School of Computer Science)
|
|
11 - 12
|
9:30 - 10:30
|
(Keynote Chair: Erika Ábrahám)
Invited talk: Dynamic Logics for Practical Software Verification
Wolfgang Ahrendt, Chalmers University of Technology, Sweden
|
|
12 - 12:30
|
10:30 - 11
|
Coffee Break
|
|
12:30 - 13:30
|
11 - 12
|
(Keynote Chair: Martin Wirsing)
Invited Talk: View-Based Semantics and Logics for Weak Memory
Heike Wehrheim, University of Oldenburg, Germany
|
|
13:30 - 14:30
|
12 - 13
|
Lunch Break
|
| |
Session 1:
Modeling, Specification and Synthesis (Session Chair: Fatemeh Ghassemi)
|
|
14:30 - 15
|
13 - 13:30
|
Juliana Cunha, Alexandre Madeira and Luís Soares Barbosa:
Structured Specification of Paraconsistent Transition Systems
|
|
15 - 15:30
|
13:30 - 14
|
Yutaka Nagashima:
Genetic Algorithm for Program Synthesis
|
|
15:30 - 16
|
14 - 14:30
|
Andrea Domenici:
Towards a Basic Theory for Partial Differentiation in the Prototype Verification System
|
|
16 - 16:30
|
14:30 - 15
|
Coffee Break
|
| |
Session 2:
Verification (Session Chair: Georgiana Caltais)
|
|
16:30 - 17
|
15 - 15:30
|
Ehsan Khamespanah, Marjan Sirjani and Ramtin Khosravi:
Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models
|
|
17 - 17:30
|
15:30 - 16
|
Xiaoyong Xue, Xiyue Zhang and Meng Sun:
kProp: Multi-Neuron Relaxation Method for Neural Network Robustness Verification
|
|
17:30 - 18
|
16 - 16:30
|
Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc and James Bang:
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
|
| Day 2: May 5, 2023 |
|
IRST
|
CEST
| |
|
11 - 12
|
9:30 - 10:30
|
(Keynote Chair: Farhad Arbab)
Invited talk: Pipelines: A Domain Science & Engineering Description
(Cancelled)
Dines Bjørner, Technical University of Denmark, Denmark
|
|
12 - 12:30
|
10:30 - 11
|
Coffee Break
|
| |
Session 3:
Distributed Systems (Session Chair: Mieke Massink)
|
|
12:30 - 13
|
11 - 11:30
|
Flip van Spaendonck:
Verification of the Busy-Forbidden Protocol
|
|
13 - 13:30
|
11:30 - 12
|
Erwan Mahe, Boutheina Bannour, Christophe Gaston, Arnault Lapitre and Pascale Le Gall:
Interaction-Based Offline Runtime Verification of Distributed Systems
|
|
13:30 - 14:30
|
12 - 13
|
Lunch Break
|
| |
Session 4:
Testing and Case Studies (Session Chair: Ebru Aydin Gol)
|
|
14:30 - 15
|
13 - 13:30
|
Ebrahim Fazli and Ali Ebnenasir:
TPGen: A Self-Stabilizing GPU-Based Method for Test and Prime Paths Generation
|
|
15 - 15:30
|
13:30 - 14
|
Wen-Ling Huang, Niklas Krafczyk and Jan Peleska:
An Optimised Complete Strategy for Testing Symbolic Finite State Machines
|
|
15:30 - 16
|
14 - 14:30
|
João Faria and Rui Abreu:
Case Studies of Development of Verified Programs with Dafny for Accessibility Assessment
|
|
16 - 16:30
|
14:30 - 15
|
Coffee Break
|
|
16:30 - 17:30
|
15 - 16
|
(Keynote Chair: Hossein Hojjat)
Invited talk: Automata Learning for Evolving and Concurrent Systems
Mohammad Reza Mousavi, King's College London, UK
|
|
17:30 - 18
|
16 - 16:30
|
Closing:
Marjan Sirjani (Steering Committee Chair)
|