|
8:45
|
Opening
Room: Auditorium
|
|
9:00
|
Thomas Henzinger: A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems (unifying talk)
Room: Auditorium
Chair: Natasha Sharygina
|
|
10:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
10:30
11:00
11:30
12:00
|
TACAS: Model Checking I
Chair: Natasha Sharygina
Room: Auditorium
Bounded Model Checking for Asynchronous Hyperproperties
T. Hsu, B. Bonakdarpour, B. Finkbeiner, C. Sanchez
Model Checking Linear Dynamical Systems under Floating-point Rounding
E. Lefaucheux, J. Ouaknine, D. Purser, M. Sharifi
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
T. Hsu, C. Sanchez, S. Sheinvald, B. Bonakdarpour
Reconciling Preemption Bounding with DPOR
Iason Marmanis, Michalis Kokologiannakis and Viktor Vafeiadis
|
TACAS: Machine Learning/Neural Networks
Chair: Roderick Bloem
Room: 44-45/108
Feature Necessity & Relevancy in ML Classifier Explanations
X. Huang, M. Cooper, A. Morgado, J. Planes, J. Marques-Silva
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
Shahaf Bassan and Guy Katz
OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
X. Guo, Z. Zhou, Y. Zhang, G. Katz, M. Zhang
Neural Network-Guided Synthesis of Recursive Functions
Naoki Kobayashi and Minchao Wu
|
ESOP: Static Analysis
Chair: Thomas Wies
Room: 44-54/109
Logics for extensional, locally complete analysis via domain refinements
Flavio Ascari, Roberto Bruni and Roberta Gori
Clustered Relational Thread-Modular Abstract Interpretation with Local Traces
Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard and Vesal Vojdani
Adversarial Reachability for Program-level Security Analysis
Soline Ducousso, Sébastien Bardin and Marie-Laure Potet
Automated Grading of Regular Expressions
Su-Hyeon Kim, Youngwook Kim, Yo-Sub Han, Hyeonseung Im and Sang-Ki Ko
|
FoSSaCS: Programming Languages
Chair:
Room: 44-45/106
When programs have to watch the paint dry
Danel Ahman
Deciding contextual equivalence of nu- calculus with effectful contexts
Daniel Hirschkoff, Guilhem Jaber and Enguerrand Prebet
Kantorovich Functors and Characteristic Logics for Behavioural Distances
Pedro Nora, Sergey Goncharov, Dirk Hofmann, Lutz Schröder and Paul Wild
A Logical Framework with Higher-Order Rational (Circular) Terms
Zhibo Chen and Frank Pfenning
|
|
12:30
|
Lunch
Room: Patio + Foyer
|
|
14:00
14:30
15:00
15:30
|
TACAS: Automata
Chair: Sriram Sankaranarayanan
Room: Auditorium
Modular Mix-and-Match Complementation of Büchi automata
V. Havlena, O. Lengal, Y. Li, B. Šmahlíková, A. Turrini
Validating Streaming JSON Documents With Learned VPAs
V. Bruyère, G. Perez, G. Staquet
Antichains Algorithms for the Inclusion Problem Between ω-VPL
K. Doveri, P. Ganty, L. Hadzi-Djokic
Stack-Aware Hyperproperties
A. Bajwa, M. Zhang, R. Chadha, M. Viswanathan
|
TACAS: SV-COMP
Chair: Dirk Beyer
Room: 24-25/405
Organization
Dirk Beyer
2LS
František Nečas
CPAchecker
Henrik Wachowitz
EBF
Fatimah Aljaafari
GDart-LLVM
Simon Dierl
Goblint
Simmo Saan
JBMC
Peter Schrammel
Korn
Gidon Ernst
LF-checker
Tong Wu
Mopsa
Raphaël Monat
Symbiotic-Witch 2
Paulína Ayaziová
Ultimate Automizer
Matthias Heizmann
Ultimate GemCutter
Dominik Klumpp
Ultimate Taipan
Frank Schüssele
VeriAbsL
Priyanka Darke
VeriFuzz
M. Raveemdra Kumar
|
ESOP: Type Systems
Chair: Sandrine Blazy
Room: 44-45/106
Pragmatic Gradual Polymorphism with References
Wenjia Ye and Bruno Oliveira
Gradual Tensor Shape Checking
Momoko Hattori, Naoki Kobayashi and Ryosuke Sato
Modal crash types for intermittent computing
Farzaneh Derakhshan, Myra Dotzel, Milijana Surbatovich and Limin Jia
Builtin Types viewed as Inductive Families
Guillaume Allais
|
FoSSaCS: Semantics
Chair:
Room: 44-45/108
A Higher-Order Language for Markov Kernels and Linear Operators
Pedro H Azevedo de Amorim
A Formal Logic for Formal Category Theory
Max New and Daniel R. Licata
A Strict Constrained Superposition Calculus for Graphs
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla and Nicolas Peltier
A programming language characterizing quantum polynomial time
Emmanuel Hainry, Romain Péchoux and Mário Silva
|
|
16:00
|
Coffee Break
Room: Foyer + 44 lobby
|
|
16:30
16:30
17:00
17:30
|
TACAS: Proofs
Chair: David Monniaux
Room: 44-45/108
Propositional Proof Skeletons
J. Reeves, B. Kiesl-Reiter, M. Heule
Unsatisfiability Proofs for Distributed Clause Sharing SAT Solvers
D. Michaelson, D. Schreiber, M. Heule, B. Kiesl-Reiter, M. Whalen
Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format
B. Andreotti, H. Lachnitt, H. Barbosa
|
TACAS: SV-COMP
Chair: Dirk Beyer
Room: 24-25/405
SV-COMP Community Meeting
Dirk Beyer
|
Invited tutorial
Chair: Marieke Huisman
Room: Auditorium
Ana-Lucia Varbanescu: Heterogeneous Computing: What, Why, How, and Whereto?
|
|
18:00
|
Welcome Reception
|
|
9:00
|
Mooly Sagiv: Scaling Formal Verification to Realistic Code with Applications to DeFi Verification (ESOP invited talk)
Room: Auditorium
Chair: Thomas Wies
|
|
10:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
10:30
10:30
11:00
11:30
12:00
|
TACAS: Constraint Solving/Blockchain
Chair: Sriram Sankaranarayanan
Room: Auditorium
The Packing Chromatic Number of the Infinite Square Grid is 15
B. Subercaseaux, M. Heule
Active Learning for SAT Solver Benchmarking
T. Fuchs, J. Bach, M. Iser
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
M. Heisinger, M. Seidl, Armin Biere
Inferring Needless Write Memory Accesses on Ethereum Bytecode
E. Albert, J. Correas, P. Gordillo, G. Román-Díez, A. Rubio
|
ESOP: Semantics and Type Theory
Chair: Luis Caires
Room: 44-45/106
Interpreting Knowledge-based Programs
Alexander Knapp, Heribert Mühlberger and Bernhard Reus
A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
Todd Schmid, Tobias Kappé and Alexandra Silva
Contextual Modal Type Theory with Polymorphic Contexts
Yuito Murase, Yuichi Nishiwaki and Atsushi Igarashi
A Type System for Effect Handlers and Dynamic Labels
Paulo Emílio de Vilhena and François Pottier
|
FoSSaCS: Counters
Chair:
Room: 44-45/108
On the Existential Arithmetics with Addition and Bitwise Minimum
Mikhail Starchak
Coverability in 2-VASS with One Unary Counter is in NP
Filip Mazowiecki, Henry Sinclair-Banks and Karol Węgrzycki
On History-Deterministic One-Counter Nets
Aditya Prakash and K. S. Thejaswini
Unboundedness problems for machines with reversal-bounded counters
Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze and Georg Zetzsche
|
Ask-Me-Anything
Chair:
Room: 24-25/405
Orna Kupferman: On Her Research
interviewed by Georgiana Caltais
Marieke Huisman: On Conference Organisation And Related Issues
interviewed by Eduard Kamburjan
Dirk Beyer and Andrzej Murawski: On Replicability
interviewed by Benjamin Kaminski
|
|
12:30
|
Lunch
Room: Patio + Foyer
|
|
14:00
14:00
14:30
15:00
15:30
|
TACAS: Markov Chains/Stochastic Control
Chair: Kim Larsen
Room: Auditorium
A Practitioner's Guide to MDP Model Checking Algorithms
Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger
Correct Approximation of Stationary Distribution
Tobias Meggendorfer
Robust Almost-Sure Reachability in Multi-Environment MDPs
Marck van der Vegt, Nils Jansen and Sebastian Junges
Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
E. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, D. Wojtczak
|
TACAS: Verification I
Chair: Haniel Barbosa
Room: 44-45/108
A Formal CHERI-C Semantics for Verification
Seung Hoon Park, Rekha Pai and Tom Melham
Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm
Yahui Song and Wei-Ngan Chin
Parameterized Verification under TSO with Data Types
P. Abdulla, M.. Atig, S. Spengler, S. Krishna, F. Furbach, A. A. Godbole, Y. G. Hendi
Verifying Learning-Based Robotic Navigation Systems
Guy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, Alessandro Farinelli, David Harel and Guy Katz
|
ESOP: Concurrency
Chair: Simon Gay
Room: 44-45/106
Quorum Tree Abstractions of Consensus Protocols
Berk Cirisci, Constantin Enea and Suha Orhun Mutluergil
MAGπ: Types for Failure-Prone Communication
Matthew Alan Le Brun and Ornela Dardha
Safe Session-Based Concurrency with Shared Linear State
Pedro Rocha and Luis Caires
System $F^mu_omega$ with Context-free Session Types
Diana Costa, Andreia Mordido, Diogo Poças and Vasco T. Vasconcelos
|
FoSSaCS: Bisimulation
Chair:
Room: 44-54/109
Reverse Bisimilarity vs. Forward Bisimilarity
Marco Bernardo and Sabina Rossi
Explainability of Probabilistic Bisimilarity Distances for Labelled Markov Chains
Amgad Rady and Franck van Breugel
Weighted and Branching Bisimilarities from Generalized Open Maps
Jérémy Dubut and Thorsten Wißmann
Preservation and Reflection of Bisimilarity via Invertible Steps
Ruben Turkenburg, Clemens Kupke, Jurriaan Rot and Ezra Schoen
|
|
16:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
16:30
16:30
16:45
17:00
17:15
17:30
17:45
|
TACAS: Tool Demos
Chair: Sergio Mover
Room: 44-45/108
EVA: A Tool for the Compositional Verification of AUTOSAR Models
A. Cimatti, S. Corfini, L. Cristoforetti, M. Di Natale, A. Griggio, S. Tonetta, F. Barrau
PyLTA: A Verification Tool for Parameterized Distributed Algorithms
Bastien Thomas and Ocan Sankur
WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification
Wenji Fang and Hongce Zhang
FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
S. Xiao, C. Zhang, J. Li, G. Pu
Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
W. Fokkink, M. Goorden, D. Hendriks, B. Beek, A. Hofkamp, F. Reijnen, P. Etman, L. Moormann, A. Mortel-Fronczak, M. Reniers, K. Rooda, B. Sanden, R. Schiffelers, S. Thuijsman, J. Verbakel, H. Voge
Multiparty Session Typing in Java, Deductively
Jelle Bouma, Stijn de Gouw and Sung-Shik Jongmans
|
Invited Tutorial
Chair: Lenore Zuck
Room: Auditorium
Verifying Probabilistic Programs: From Theory to Automation
Joost-Pieter Katoen
|
Diversity and Inclusion Activities
Chair: Fabrice Kordon
Room: 44-45/106
|
|
9:00
|
Véronique Cortier: Electronic Voting: Design And Formal Verification (unifying talk)
Room: Auditorium
Chair: Orna Kupferman
|
|
10:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
10:30
10:30
11:00
11:30
12:00
|
TACAS: Combinatorial Optimization / Theorem Proving
Chair: Haniel Barbosa
Room: Auditorium
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
J. Cortes, I. Lynce, V. Manquinho
Verified reductions for optimization
A. Bentkamp, R. Fernández Mir, J. Avigad
Specifying and Verifying Higher-order Rust Iterators
X. Denis, J. Jourdan
Extending a High-Performance Prover to Higher-Order Logic
P. Vukmirović, J. Blanchette, S. Schulz
|
TACAS: Tools (Regular Papers)
Chair: Alessandro Cimatti
Room: 44-45/108
The WhyRel Prototype for Relational Verification of Pointer Programs
R. Nagasamudram, A. Banerjee, D. Naumann
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter
D. Beyer, P. Chien, Nian-Ze Lee
CoPTIC: Constraint Programming Translated Into C
Martin Mariusz Lester
Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
Michaël Cadilhac and Guillermo Perez
|
FASE: Requirements, Models and AI
Chair: Facundo Molina
Room: 44-54/109
ACoRe: Automated Goal-Conflict Resolution
Luiz Carvalho, Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon and Mike Papadakis
Democratizing Quality-Based Machine Learning Development through Extended Feature Models
Giordano d'Aloisio, Antinisca Di Marco and Giovanni Stilo
Compositional Automata Learning of Synchronous Systems
Thomas Neele and Matteo Sammartino
Feature-Guided Analysis of Neural Networks (NIER paper)
Divya Gopinath, Luca Lungeanu, Ravi Mangal, Corina Pasareanu, Siqi Xie and Huafeng Yu
Specification and Validation of Normative Rules for Autonomous Agents (Tool paper)
Sinem Getir Yaman, Charlie Burholt, Maddie Jones, Radu Calinescu and Ana Cavalcanti
|
FoSSaCS: Formal Languages
Chair:
Room: 44-45/106
Quantitative Safety and Liveness
Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç
On the Comparison of Discounted-Sum Automata with Multiple Discount Factors
Udi Boker and Guy Hefetz
Fast Matching of Regular Patterns with Synchronizing Counting
Lukáš Holík, Juraj Síč, Lenka Turoňová and Tomas Vojnar
Compositional Learning for Interleaving Parallel Automata
Faezeh Labbaf, Hossein Hojjat, Jan Friso Groote and Mohammadreza Mousavi
|
SPIN (co-located)
Chair: Max Tschaikowski
Room: 25-26/105
Model-Checking Quantum Computing Systems (keynote)
Simon Gay
Efficient Implementation of LIMDDs for Quantum Circuit Simulation
Lieuwe Vinkhuijzen, Thomas Grurl, Stefan Hillmich, Sebastiaan Brand, Robert Wille and Alfons Laarman
ParaGnosis: A Tool for Parallel Knowledge Compilation
Giso Dal, Alfons W. Laarman and Peter J.F. Lucas
|
|
12:30
|
Lunch
Room: Patio + Foyer
|
|
13:00
|
ETAPS General Assembly
Room: Auditorium
|
|
14:00
14:00
14:30
15:00
15:30
|
TACAS: Synthesis I
Chair: Cesar Sanchez
Room: Auditorium
Verification-guided Programmatic Controller Synthesis
Yuning Wang and He Zhu
Computing Adequately Permissive Assumptions for Synthesis
Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak and Anne-Kathrin Schmuck
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
Philippe Heim and Rayna Dimitrova
Lockstep Composition for Unbalanced Loops
Ameer Hamza and Grigory Fedyukovich
|
ESOP: Probabilistic and Quantum Programming
Chair: Benjamin Kaminski
Room: 44-45/108
Type-safe (Variational) Quantum Programming in Idris
Liliane-Joy Dandy, Emmanuel Jeandel and Vladimir Zamdzhiev
Bunched Fuzz: Sensitivity for Vector Metrics
June Wunder, Arthur Azevedo de Amorim, Patrick Baillot and Marco Gaboardi
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing
Basim Khajwal, Luke Ong and Dominik Wagner
Automatic Alignment in Higher-Order Probabilistic Programming Languages
Daniel Lundén, Gizem Çaylak, Fredrik Ronquist and David Broman
|
FASE: Runtime Monitoring & Enforcement
Chair: Heike Wehrheim
Room: 44-54/109
Opportunistic Monitoring of Multithreaded Programs
Chukri Soueidi, Yliès Falcone and Antoine El-Hokayem
VAMOS: Middleware for Best-Effort Third-Party Monitoring
Marek Chalupa, Stefanie Muroya Lei, Fabian Muehlboeck and Thomas Henzinger
Runtime Enforcement Using Knowledge Bases
Eduard Kamburjan and Crystal Chang Din
|
FoSSaCS: Formal methods
Chair:
Room: 44-45/106
Pebble minimization: the last theorems
Gaëtan Douéneau-Tabot
Noetherian topologies defined via fixed-points
Aliaume Lopez
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
Quang Loc Le and Xuan-Bach D. Le
|
SPIN (co-located)
Chair: Arnd Hartmanns
Room: 25-26/105
The Probabilistic Model Checker Storm (keynote)
Joost-Pieter Katoen
Model Checking Futexes
Hugues Evrard and Alastair Donaldson
Sound Concurrent Traces for Online Monitoring
Chukri Soueidi and Yliès Falcone
|
|
16:00
|
Coffee Break
Room: Foyer + 44 lobby
|
|
16:30
16:30
17:00
17:20
|
SPIN (co-located)
Chair: Alfons Laarman
Room: 25-26/105
Elimination of Detached Regions in Dependency Graph Verification
Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiri Srba and Nikolaj Jensen Ulrik
Potency-Based Heuristic Search with Randomness for Explicit Model Checking
Emil G. Henriksen, Alan M. Khorsid, Esben Nielsen, Theodor Risager, Jiri Srba, Adam M. Stuck and Andreas S. Sørensen
GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data
Anton Wijs and Muhammad Osama
|
TOOLympics
Room: Auditorium
Introduction
Dirk Beyer, Fabrice Kordon, Arnd Hartmanns
CHC-COMP
Hossein Hojjat
MCC
Fabrice Kordon
QComp
Arnd Hartmanns
ARCH-COMP
Arnd Hartmanns
RERS
Falk Howar
SL-COMP
Mihaela Sighireanu
SV-COMP
Dirk Beyer
Test-Comp
Dirk Beyer
VerifyThis
Gidon Ernst
VT-LTC
Gidon Ernst
|
|
19:00
|
Banquet
|
|
9:00
|
Sven Apel: Brains on Code: Towards a Neuroscientific Foundation of Program Comprehension (FASE invited talk)
Room: Auditorium
Chair: Leen Lambers
|
|
10:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
10:30
10:30
11:00
11:30
12:00
|
TACAS: Verification II
Chair: Dirk Beyer
Room: Auditorium
Make flows small again: revisiting the flow framework
Roland Meyer, Thomas Wies and Sebastian Wolff
ALASCA: Reasoning in Quantified Linear Arithmetic
Johannes Schoisswohl, Laura Kovacs, Giles Reger, Konstantin Korovin and Andrei Voronkov
A Matrix-Based Approach to Parity Games
Saksham Aggarwal, Alejandro Stuckey de la Banda, Henri Urpani, Luke Yang and Julian Gutierrez
A GPU Tree Database for Many-Core Explicit State Space Exploration
Anton Wijs and Muhammad Osama
|
TACAS: Graphs/Probabilistic Systems
Chair: Natasha Sharygina
Room: 44-45/108
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol and Andreas Pavlogiannis
Transforming quantified boolean formulas using biclique covers
Oliver Kullmann and Ankit Shukla
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
T. Winkler, Joost-Pieter Katoen
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
K. Batz, M. Chen, S. Junges, B. Kaminski, Joost-Pieter Katoen, Christoph Matheja
|
FASE: Analysis & Verification
Chair: Eduard Kamburjan
Room: 44-54/109
Parallel Program Analysis via Range Splitting
Jan Haltermann, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim
Yet Another Model! A Study on Model's Similarities for Defect and Code Smells
Geanderson Santos, Amanda Santana, Gustavo Vale and Eduardo Figueiredo
A Modeling Concept for Formal Verification of OS-Based Compositional Software
Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim Guldstrand Larsen and Marcel Baunach
Towards Log Slicing (NIER paper)
Joshua Dawes, Donghwan Shin and Domenico Bianculli
JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java (Tool paper)
Simon Bliudze, Petra van den Bos, Marieke Huisman, Robert Rubbens and Larisa Safina
|
FoSSaCS: Verification
Chair:
Room: 44-45/106
Just Testing
Rob van Glabbeek
Model and Program Repair via Group Actions
William Cocke and Paul Attie
Subgame optimal strategies in finite concurrent games with prefix-independent objectives
Benjamin Bordais, Patricia Bouyer and Stephane Le Roux.
|
SPIN (co-located)
Chair: Sergio Mover
Room: 25-26/105
Formal Verification of Privacy Policies for Social Networks (keynote)
Raúl Pardo
Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks
Bryant Israelsen, Landon Taylor and Zhen Zhang
Accelerating black box testing with light-weight learning
Roi Fogler, Itay Cohen and Doron Peled
|
|
12:30
|
Lunch
Room: Patio + Foyer
|
|
14:00
14:00
14:30
15:00
|
TACAS: Model Checking II
Chair: Sriram Sankaranarayanan
Room: Auditorium
Optimal Stateless Model Checking for Causal Consistency
Parosh Abdulla, Mohamed Faouzi Atig, Krishna S, Ashutosh Gupta and Omkar Tuppe
Symbolic Model Checking for TLA+ Made Faster
R. Otoni, I. Konnov, J. Kukovec, P. Eugster, N. Sharygina
AutoHyper: Explicit-State Model Checking for HyperLTL
R. Beutner and B. Finkbeiner
|
FASE: Testing
Chair: Andrzej Wąsowski
Room: 44-45/108
Efficient Bounded Exhaustive Input Generation from Program APIs
Mariano Politano, Valeria Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo Frias and Pablo Ponzio
Model-based Player Experience Testing with Emotion Pattern Verification
Saba Gholizadeh Ansari, I. S. W. B. Prasetya, Davide Prandi, Fitsum Meshesha Kifetew, Frank Dignum, Mehdi Dastani and Gabriele Keller
Concolic Testing of Front-end JavaScript
Zhe Li and Fei Xie
|
Awards
Chair: Marieke Huisman
Room: 44-45/106
Test-of-Time Award
Explicit-State Software Model Checking Based on CEGAR and Interpolation, by Dirk Beyer and Stefan Löwe
Dissertation Award
Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems, by Kaushik Mallik
Test-of-Time Tool Award
CADP: Construction and Analysis of Distributed Processes, by Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
|
SPIN (co-located)
Chair: Matthias Heizmann
Room: 25-26/105
Interpretability-Aware Verification of Machine Learning Software (keynote)
Caterina Urban
WikiCoder: Learning to Write Knowledge-Powered Code
Théo Matricon, Nathanaël Fijalkow and Gaëtan Margueritte
Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties
Benedikt Maderbacher, Stefan Schupp, Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Bettina Könighofer
|
|
16:00
|
Coffee break
Room: Foyer + 44 lobby
|
|
16:30
16:30
17:00
17:30
|
TACAS: Monitoring/Program Analysis
Chair: Jan Kofroň
Room: Auditorium
Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote
P. Deligiannis, A. Senthilnathan, F. Nayyar, C. Lovett, A. Lal
Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
Kalmer Apinis and Vesal Vojdani
Explainable Online Monitoring of Metric Temporal Logic
L. Lima, A. Herasimau, M. Raszyk, D. Traytel, S. Yuan
|
TACAS: Synthesis II
Chair: Cesar Sanchez
Room: 44-45/108
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
N. Jaber, C. Wagner, S. Jacobs, M. Kulkarni, R. Samanta
LTL Reactive Synthesis with a Few Hints
M. Balachander, E. Filiot, Jean-Francois Raskin
Timed Automata Verification and Synthesis via Finite Automata Learning
Ocan Sankur
|
FASE: Test-Comp
Chair: Dirk Beyer
Room: 24-25/405
Organization
Dirk Beyer
FuSeBMC_IA
Fedor Shmarov
Legion
Gidon Ernst
VeriFuzz
M. Raveemdra Kumar
Community Meeting
Dirk Beyer
|