TACAS: Proof Checking
Chair: Marijn Heule
Room: Hollenfels
14:00
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Hanna Lachnitt, Cesare Tinelli, Andrew Reynolds, Andres Noetzli, Haniel Barbosa, Leni Aniva, Clark Barrett and Mathias Fleury
14:30
Automate where Automation Fails: Proof Strategies for Frama-C/WP
Loïc Correnson, Allan Blanchard, Adel Djoudi and Nikolai Kosmatov
14:45
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification
Mertcan Temel
15:00
A State-of-the-Art Karp-Miller Algorithm Certified in Coq
Thibault Hilaire, David Ilcinkas and Jérôme Leroux
15:30
A Logical Treatment of Finite Automata
Nishant Rodrigues, Mircea Sebe, Xiaohong Chen and Grigore Rosu
FASE: System Comprehension
Chair: Andrzej Wąsowski
Room: Schengen II
14:00
Monitoring the Future of Smart Contracts
Margarita Capretto, Martin Ceresa, and Cesar Sanchez
14:30
Comprehending Object State via Dynamic Class Invariant Learning
Jan H. Boockmann, and Gerald Luettgen
15:00
Smart Issue Detection for Large-Scale Online Service Systems Using Multi-Channel Data*
Liushan Chen, Yu Pei, Mingyang Wan, Zhihui Fei, Tao Liang, and Guojun Ma
15:30
Refinement Verification of OS Services based on a Verified Preemptive Microkernel
Ximeng Li, Shanyan Chen, Yong Guan, Qianying Zhang, Guohui Wang, and Zhiping Shi
14:00
Verifiying a Concurrent Memory Allocator with Verus
Travis Hance
14:30
Efficiently Verifying Rust Traits with SMT Solvers
Chris Hawblitzel
15:00
OxiDD: Verification Challenge
Nils Husung, Clemens Dubslaff and Maximilian Alexander Köhl
15:30
Rust Verification Workshop Proposal: Crowdsourcing the Rust standard library verification
Celina G. Val and Rahul Kumar
Competition of Software Verification (SV-COMP)
Chair: Dirk Beyer
Room: Diekirch-Echternach-Fischbach
14:00
Introduction to SV-COMP
Dirk Beyer
14:25
Bubaak (Marek Chalupa), Bubaak-SpLit (Cedric Richter), ConcurrentWitness2Test (Levente Bajczi), CPAchecker (Daniel Baier), CPV (Po-Chun Chien)
14:45
EmergenTheta (Zsófia Ádám), ESBMC (Rafael Sá Menezes), Goblint (Michael Schwarz), Goblint Validator (Simmo Saan)
15:00
Korn (Gidon Ernst), LIV (Marian Lingsch-Rosenfeld), Mopsa (Raphaël Monat), PredatorHP (Veronika Šoková), PROTON (Ravindra Metta), SWAT (Nils Loose), Symbiotic (Jan Strejček), Theta (Csanád Telbisz)
15:30
UAutomizer (Matthias Heizmann), UGemCutter (Dominik Klumpp), UKojak (Frank Schüssele), VeriAbsL (Priyanka Darke), Witch 3 (Paulína Ayaziová), WitnessLint (Marian Lingsch-Rosenfeld)
Diversity & Inclusion
Chair: Peter Roenne
Room: Europe A
14:00
Why do we talk about Equality and Diversity in research?
Inês Crisóstomo
14:10
The Computer Girls: Exploring Herstory
Valérie Schafer
14:50
Building an Inclusive Researcher Journey
Véronique Schlick
15:00
Interactive session and discussion