|
08:45
|
ETAPS Opening
Room: MDCL 1305
|
|
09:00
|
Ina Schaefer: Correctness-by-Construction—Past, Present and Future (unifying speaker)
Room: MDCL 1305
Chair: Delia Kesner
|
|
10:00
|
Coffee Break
Room: MDCL
|
|
10:30
10:45
11:00
11:30
12:00
|
FASE: AI and Software Quality
Chair: Gordon Fraser
Room: MDCL 1309
Welcome to FASE 2025
Gordon Fraser, Artur Boronat
Towards Large Language Model Guided Kernel Direct Fuzzing
Xie Li, Zhaoyue Yuan, Zhenduo Zhang, Youcheng Sun and Lijun Zhang
DeepCRCEval: Revisiting the Evaluation of Code Review Comment Generation
Junyi Lu, Xiaojia Li, Zihan Hua, Lei Yu, Shiqi Chen, Li Yang, Fengjun Zhang and Chun Zuo
VOCE: A Virtual On-Call Engineer for Automated Alert Incident Analysis Using a Large Language Model
Jia Chen, Xiao Lei Chen, Jie Shi, Peng Wang and Wei Wang
Hybridize Functions: A Tool for Automatically Refactoring Imperative Deep Learning Programs to Graph Execution
Raffi Khatchadourian, Tatiana Castro Vélez, Mehdi Bagherzadeh, Nan Jia and Anita Raja
|
TACAS: Program Analysis
Chair: Dirk Beyer
Room: MDCL 1102
Inferring Incorrectness Specifications for Object-Oriented Programs
Wenhua Li, Quang Loc Le, Yahui Song and Wei-Ngan Chin
On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)
Levente Bajczi, Csanád Telbisz, Dániel Szekeres and András Vörös
Performance Heuristics for GR(1) Realizability Checking and Related Analyses
Roy Yatskan, Ilia Shevrin and Shahar Maoz
Stream-Based Monitoring of Algorithmic Fairness
Jan Baumeister, Bernd Finkbeiner, Frederik Scheerer, Julian Siber and Tobias Wagenpfeil
|
FOSSACS: Games and Logics
Chair: Lutz Schröder
Room: MDCL 1105
Complementation of Emerson-Lei Automata
Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková
Fair Quantitative Games (Quantitative Games)
Ashwani Anand, Satya Prakash Nayak, Ritam Raha, Irmak Saglam and Anne-Kathrin Schmuck
Quantifier Elimination and Craig Interpolation: The Quantitative Way
Kevin Batz, Joost-Pieter Katoen and Nora Orhan
On the cut-elimination of the modal mu-calculus: Linear Logic to the rescue (Logic)
Esaïe Bauer and Alexis Saurin
|
RUST WORKSHOP
Room: MDCL 1009
Charon: An Analysis Framework for Rust
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz and Jonathan Protzenko
BorrowSanitizer
Ian McCormack, Oliver Braunsdorf, Johannes Kinder, Jonathan Aldrich and Joshua Sunshine
Tool Demo: Toward Unbounded Proof with Kani Loop Contracts
Qinheping Hu, Michael Tautschnig, Remi Delmas and Celina Val
Bounded Model Checking for Rust
Siddharth Priya, Joseph Tafese and Arie Gurfinkel
|
|
12:30
|
Lunch
Room: CIBC Hall & Foyer
|
|
14:00
14:30
15:00
15:30
|
TACAS: ATP & Rewriting
Chair: Xujie Si
Room: MDCL 1102
Augmenting Model-Based Instantiation with Fast Enumeration
Lydia Kondylidou, Andrew Reynolds and Jasmin Blanchette
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett and Sanmi Koyejo
Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf and Aart Middeldorp
Multiparty Session Typing, Embedded
Sung-Shik Jongmans
|
FOSSACS: Bisimulations
Chair: César Sánchez
Room: MDCL 1105
A General Completeness Theorem for Skip-free Star Algebras
Tobias Kappé and Todd Schmid
A behavioural pseudometric for continuous-time Markov processes
Linan Chen, Florence Clerc and Prakash Panangaden
Alternative Characterizations of Hereditary History-Preserving Bisimilarity via Backward Ready Multisets
Marco Bernardo, Andrea Esposito and Claudio Antares Mezzina
Relational Connectors and Heterogeneous Simulations
Pedro Nora, Jurriaan Rot, Lutz Schröder and Paul Wild
|
SV-COMP
Chair: Dirk Beyer
Room: MDCL 1008
SV-COMP Presentations
|
Diversity & Inclusion
Chair: Mark Lawford
Room: MDCL 1016
Embedding EDI in Research—and in Ourselves: Lessons in Leadership and Belonging
Prof. Sarah Dickson-Anderson, Associate Dean (Undergraduate), Faculty of Engineering, McMaster University
Innovation Needs All Perspectives: Why Diversity Matters in the Future of Mobility
Sahar Kokaly, Ph.D., P.Eng., Software Engineering Manager ADAS Software Safety, CTC Academic and Scientific Partnerships Manager, General Motors
The Art of Saying Nothing: Mastering the Empty Diversity & Inclusion Statement – A Reviewer's Perspective
Sébastien Mosser, PEng, PhD, Associate Chair, Dept. of Computing and Software, McMaster University
Panel Discussion and Q&A
|
RUST WORKSHOP
Room: MDCL 1009
Writing safe specifications for unsafe implementations in Verus
Travis Hance
Give your Rust a Koat - Towards Symbolic Execution of Rust code via Stable MIR
Jost Berthold and Daniel Cumming
Transitioning Production Software Verification to Verus: An Experience Report
Daniel Schoepe and Marianna Rapoport
|
|
16:00
|
Coffee Break
Room: MDCL
|
|
16:30
17:00
17:30
|
TACAS: Model checking
Chair: Kristin Yvonne Rozier
Room: MDCL 1102
Token Elimination in Model Checking of Petri Nets
Nicolaj Østerby Jensen, Jiri Srba and Kim Guldstrand Larsen
Efficient Evidence Generation for Modal μ-Calculus Model Checking
Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux and Tim A. C. Willemse
Sound Statistical Model Checking for Probabilities and Expected Rewards
Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger and Patrick Wienhöft
|
Suguman Bansal (Invited Tutorial)
Chair: Claudio Menghi
Room: MDCL 1305
Suguman Bansal: Specification-Guided RL
|
SV-COMP
Chair: Dirk Beyer
Room: MDCL 1008
SV-COMP Community Meeting
|
RUST WORKSHOP
Room: MDCL 1009
Lightning Talks
various
|
|
18:30
|
Welcome Reception
Room: Alumni Memorial Hall
|
|
09:00
|
José Meseguer: Capturing System Designs with Formal Executable Specifications (FASE invited speaker)
Room: MDCL 1305
Chair: Artur Boronat
|
|
10:00
|
Coffee Break
Room: MDCL
|
|
10:30
11:00
11:30
12:00
12:15
|
TACAS: LTL
Chair: Sebastian Junges
Room: MDCL 1102
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
Zili Wang, Katherine Kosaian and Kristin Yvonne Rozier
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop and Ashkan Zarkhah
Learning real-time one-counter automata using polynomially many queries
Prince Mathew, Vincent Penelle and A V Sreejith
LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specifications
Shufang Zhu and Marco Favorito
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç
|
ESOP: Types
Chair: Viktor Vafeiadis
Room: MDCL 1305
Stratified Type Theory
Jonathan Chan and Stephanie Weirich
Elucidating Type Conversions in SQL Engines
Wenjia Ye, Matías Toro, Claudio Gutierrez, Bruno C. D. S. Oliveira and Éric Tanter
Named Arguments as Intersections, Optional Arguments as Unions
Yaozhu Sun and Bruno C. D. S. Oliveira
SMT-Boosted Security Types for Low-Level MPC
Christian Skalka and Joseph P. Near
|
FASE: MDE
Chair: Artur Boronat
Room: MDCL 1309
Compositional Learning for Synchronous Parallel Automata
Mahboubeh Samadi, Aryan Bastany and Hossein Hojjat
Symbolic State Partitioning for Reinforcement Learning
Mohsen Ghaffari, Mahsa Varshosaz, Einar Broch Johnsen and Andrzej Wasowski
Formal Architectural Patterns for Adaptive Robotic Software
James Baxter, Bert van Acker, Morten Kristensen, Thomas Wright, Ana Cavalcanti and Cláudio Gomes
RoboScene: Notation for Formal Verification of Human-Robot Interaction
Holly Hendry, Ana Cavalcanti, Cade McCall and Mark Chattington
|
FOSSACS: Semantics
Chair: Petr Jančar
Room: MDCL 1105
Context-Free Languages of String Diagrams
Matt Earnshaw and Mario Román
Complete Test Suites for Automata in Monoidal Closed Categories
Bálint Kocsis and Jurriaan Rot
Idempotent Resources in Separation Logic
Daniel Gratzer, Mathias Adam Møller and Lars Birkedal
A Diagrammatic Algebra for Program Logics
Filippo Bonchi, Alessandro Di Giorgio and Elena Di Lavore
|
RUST WORKSHOP
Room: MDCL 1009
Using Rust and Verus for Development of Verified Operating Systems
Xiangdong Chen, Zhaofeng Li, Jerry Zhang and Anton Burtsev
VTock: Retrofitting automatic verification to a production microcontroller OS
Vivien Rindisbacher, Evan Johnson, Nico Lehmann, Ranjit Jhala and Deian Stefan
Vest: A Case Study of Verifying Performant, Higher-Order Rust Programs in Verus
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich and Bryan Parno
Verification of Cryptographic Implementations in Lean with Aeneas
Son Ho, Aymeric Fromherz and Jonathan Protzenko
|
|
12:30
|
Lunch
Room: CIBC Hall & Foyer
|
|
14:00
14:30
15:00
15:30
|
TACAS: Verification I
Chair: Florian Zuleger
Room: MDCL 1102
Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs
Daniela Kaufmann and Jérémy Berthomieu
Cyclone: A Heterogeneous Tool for Verifying Infinite Descent
Liron Cohen, Reuben Rowe and Matan Shaked
Implicit Rankings for Verifying Liveness Properties in First-Order Logic
Raz Lotan and Sharon Shoham
Neural Network Verification with Branch-and-Bound for General Nonlinearities
Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh and Huan Zhang
|
ESOP: Static Analysis
Chair: Ori Lahav
Room: MDCL 1305
Formal Verification of WTO-based Dataflow Solvers
Roméo La Spina, Delphine Demange and Sandrine Blazy
Efficient Synthesis of Tight Polynomial Upper-bounds for Systems of Conditional Polynomial Recurrences
Amir Goharshady, S. Hitarth and Sergei Novozhilov
Context-Sensitive Demand-Driven Control-Flow Analysis
Tim Whiting and Kimball Germane
Abstraction of memory block manipulations by symbolic loop folding
Jérôme Boillot and Jérôme Feret
|
FASE: Fundamentals
Chair: Mahsa Varshosaz
Room: MDCL 1309
Stochastic Timed Graph Transformation Systems
Sven Schneider, Maria Maximova and Holger Giese
Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor
Axel Ferréol, Laurent Corbin and Nikolai Kosmatov
Reasoning about Substitutability at the Level of Bytecode
Marco Paganoni and Carlo A. Furia
|
RUST WORKSHOP
Room: MDCL 1009
Verifying the Rust Standard Library
Carolyn Zech, Celina Val and Rahul Kumar
Initial Steps Toward Verifying the Rust Standard Library Using Verus
Elanor Tang, Travis Hance and Bryan Parno
Open Discussion
|
Ask-me-anything
Room: MDCL 1008
The Future of Conferences with Laura Kovacs and Marie Farrell
Host: Sebastian Junges
Software Liability, Legislation, AI Act, What Does It Mean For Us with Holger Hermanns and Tiziana Margaria
Host: Elizabeth Polgreen
|
|
16:00
|
Coffee Break
Room: MDCL
|
|
16:30
17:00
17:30
|
TACAS: SAT/SMT
Chair: Clark Barrett
Room: MDCL 1102
D-Painless: A Framework for Distributed Portfolio SAT Solving
Mazigh Saoudi, Souheib Baarir, Julien Sopena and Thibault Lejemble
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
David Chocholatý, Vojtěch Havlena, Lukáš Holík, Jan Hranička, Ondrej Lengal and Juraj Síč
Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
Daimy Van Caudenberg, Bart Bogaerts and Leandro Vendramin
|
Arun Ross (Invited Tutorial)
Chair: Marieke Huisman
Room: MDCL 1305
Arun Ross: Unlocking You: The Impact of AI on Biometrics
|
RUST WORKSHOP
Room: MDCL 1009
Discussion
|
|
09:00
|
Amal Ahmed: Prose No More: Formally Specifying ABIs using Realistic Realizability (ESOP invited speaker)
Room: MDCL 1305
Chair: Viktor Vafeiadis
|
|
10:00
|
Coffee Break
Room: MDCL
|
|
10:30
11:00
11:15
11:30
12:00
|
TACAS: Proofs and certificates
Chair: Daniela Kaufmann
Room: MDCL 1102
Unsatisfiability Proofs for Horn Solving
Rodrigo Otoni, Martin Blicha, Matias Barandiaran Rivera, Patrick Eugster, Jan Kofroň and Natasha Sharygina
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler and Daniel Zilken
Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
Christoph Jabs, Jeremias Berg, Bart Bogaerts and Matti Järvisalo.
Revisiting DRUP-based Interpolants with CaDiCaL 2.0
Yakir Vizel and Basel Khouri
|
ESOP: Semantics
Chair: Marieke Huisman
Room: MDCL 1305
Coverage Semantics for Dependent Pattern Matching
Joseph Eremondi and Ohad Kammar
An abstract, certified account of operational game semantics
Peio Borthelle, Guilhem Jaber, Tom Hirschowitz and Yannick Zakowski
Context-Dependent Effects in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany and Lars Birkedal
On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic
Risa Yamada, Naoki Kobayashi, Ken Sakayori and Ryosuke Sato
|
FOSSACS: Time and Concurrency
Chair: Eduardo Bonelli
Room: MDCL 1105
Model-checking real-time systems: revisiting the alternating automaton route
Patricia Bouyer, B Srivathsan and Vaishnavi Vishwanath
Temporal Hyperproperties for Population Protocols
Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty and César Sánchez
Structural Liveness of Conservative Petri Nets (Complexity, petri nets, structural liveness)
Petr Jancar, Jérôme Leroux and Jiri Valusek
Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics (Models, axiomatization, effects)
Yotam Dvir, Ohad Kammar, Ori Lahav and Gordon Plotkin
|
SPIN
Room: MDCL 1009
Developments in Symbolic Model Checking
Orna Grumberg
Accelerating CAR-based Model-Checking with Multiple Unsatisfiable Cores
Yibo Dong, Xiwei Wu, Jianwen Li, Geguang Pu and Ofer Strichman
Efficient Model Checking for the Alternating-Time µ-Calculus via Effectivity Frames
Daniel Hausmann, Merlin Humml, Simon Prucker and Lutz Schröder
|
INDUSTRY DAY
Room: MDCL 1110
Weathering the Weather: The Storms Gathering Around the Development of Safety-Critical Systems
Chris Hobbs (Consultant)
Safe Agile: A Safety Strategy for Agile Development Strategy for Spacecrafts or Space robots
Thomas Chowdhury (MDA Space)
Temporal specification languages in industrial hardware verification
Simon Jantsch (Siemens EDA)
|
|
12:30
|
Lunch
Room: CIBC Hall & Foyer
|
|
13:00
|
ETAPS General Assembly
Room: MDCL 1305
|
|
14:00
14:30
14:45
15:00
15:30
|
TACAS: Synthesis
Chair: Elizabeth Polgreen
Room: MDCL 1102
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Derek Egolf and Stavros Tripakis
Synthesis of Universal Safety Controllers
Bernd Finkbeiner, Niklas Metzger, Satya Prakash Nayak and Anne-Kathrin Schmuck
Synthesis with Guided Environments
Orna Kupferman and Ofer Leshkowitz
Value Iteration with Guessing for Markov Chains and Markov Decision Processes
Krishnendu Chatterjee, Mahdi Jafariraviz, Raimundo Saona Urmeneta and Jakub Svoboda
|
ESOP: Concurrency 1
Chair: Viktor Vafeiadis
Room: MDCL 1305
Iso-Recursive Multiparty Sessions and their Automated Verification
Marco Giunti and Nobuko Yoshida
Multiparty Session Types with a Bang!
Matthew Alan Le Brun, Simon Fowler and Ornela Dardha
First-Person Choreographic Programming with Continuation-Passing Communications
Sung-Shik Jongmans
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
Felix Stutz and Emanuele D'Osualdo
|
SPIN
Room: MDCL 1009
MoXI session
|
INDUSTRY DAY
Room: MDCL 1110
Challenges & Opportunities in Assurance of Software Defined Vehicles
Mark Lawford (McMaster University)
Using lightweight formal methods to check correctness of production code for Amazon S3
Rajeev Joshi (Amazon Web Services)
Abstract Interpretation of Floating-Point Digital Filters in Nuclear Plant Software.
Pierre-Yves Piriou (EDF), Maxime Jacquemin (CEA) and Franck Védrine (CEA)
|
Tool Demo Session
Chair:
Room: MDCL 1008, MCDL 1016
|
|
16:00
|
Coffee Break
Room: MDCL
|
|
16:30
17:00
17:30
|
TACAS: Equivalence checking
Chair: Anton Wijs
Room: MDCL 1102
Refuting Equivalence in Probabilistic Programs with Conditioning
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić
Revisiting Differential Verification: Equivalence Verification with Confidence
Samuel Teuber, Philipp Kern, Marvin Janzen and Bernhard Beckert
Equivalence Checking of a libm Port
Mark S. Baranowski, Zvonimir Rakamaric and Ganesh Gopalakrishnan.
|
ESOP: Fresh Perspectives
Chair: Peter Müller
Room: MDCL 1305
Neural Network Verification is a Programming Language Challenge
Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Šinkarovs and Haoze Wu
Formal Autograding in a Classroom
Dragana Milovančević, Mario Bucev, Marcin Wojnarowski, Samuel Chassot and Viktor Kunčak
The Vanilla Sequent Calculus is Call-by-Value
Beniamino Accattoli
|
FOSSACS: Programs
Chair: Naoki Kobayashi
Room: MDCL 1105
Sharing and Linear Logic with Restricted Access
Pablo Barenbaum and Eduardo Bonelli
Combining quantum and classical control: syntax, semantics and adequacy
Kinnari Dave, Louis Lemonnier, Romain Péchoux and Vladimir Zamdzhiev
BiGKAT: an algebraic framework for relational verification of probabilistic programs
Leandro Gomes, Patrick Baillot and Marco Gaboardi
|
SPIN
Room: MDCL 1009
0-1 Laws for LTL and CTL over Random Transition Systems
Yanni Dong, Milan Lopuhaä-Zwakenberg and Marielle Stoelinga
A Modular Program-Transformation Framework for Reducing Specifications to Reachability
Dirk Beyer, Marek Jankola, Marian Lingsch-Rosenfeld, Tian Xia and Xiyue Zheng
(Asynchronous) Temporal Logics for Hyperproperties on Finite Traces
Alberto Bombardelli, Laura Bozzelli, Cesar Sanchez and Stefano Tonetta
|
INDUSTRY DAY
Room: MDCL 1110
Advancing software solutions for CAR-T therapy manufacturing and standardization.
Ethan Dhanraj (OmniaBio) and Hanene Ben Yedder (OmniaBio)
Agile Development: Ensuring Safety in Rapid Iteration Cycles
Mehrnoosh Askarpour (General Motors Canada), Sahar Kokaly (General Motors Canada) and Ramesh S (General Motors R&D)
Networking and informal discussions
|
|
18:30
|
Banquet
Room: LIUNA Station
|
|
09:00
|
Matt Dwyer: Leveraging Abstractions for Validation of Machine Learning Models (unifying speaker)
Room: MDCL 1305
Chair: Marijn Heule
|
|
10:00
|
Coffee Break
Room: MDCL
|
|
10:30
11:00
11:30
12:00
|
TACAS: Games
Chair: Jie-Hong Roland Jiang
Room: MDCL 1102
Reachability for Nonsmooth Systems with Lexicographic Jacobians
Chenxi Ji, Huan Zhang and Sayan Mitra
Non-Zero-Sum Games with Multiple Weighted Objectives
Yoav Feisntein, Orna Kupferman and Noam Shenwald
Fast value iteration: A uniform approach to efficient algorithms for energy games
Michaël Cadilhac, Antonio Casares and Pierre Ohlmann
Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming
Rafael Gonçalves, Filipe Gouveia, Inês Lynce and José Fragoso Santos
|
ESOP: Probabilistic Programming
Chair: Viktor Vafeiadis
Room: MDCL 1305
Verifying Algorithmic Versions of the Lovász Local Lemma
Rongen Lin, Hongjin Liang and Xinyu Feng
A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model
Weijie Fan, Hongjin Liang, Xinyu Feng and Hanru Jiang
Variable Elimination as Rewriting in a Linear Lambda Calculus
Claudia Faggian, Thomas Ehrhard and Michele Pagani
A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming
Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva and Fabio Zanasi
|
SPIN
Room: MDCL 1009
Growing an ω-automata library
Alexandre Duret-Lutz
Resilience through Automated Adaptive Configuration for Distribution and Replication
Scott Stoller, Balaji Jayasankar and Yanhong A. Liu
An Efficient and Versatile Approach to Shortest Path Problems in Interprocedural Programs
Theo De Castro Pinto, Antoine Rollet and Grégoire Sutre
|
|
12:30
|
Lunch
Room: CIBC Hall & Foyer
|
|
14:00
14:30
15:00
15:30
|
TACAS: Verification II
Chair: Marijn Heule
Room: MDCL 1102
Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM
Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym and Jan Midtgaard
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu and David Basin
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza and Jakob Schulz
Certifiably Robust Policies for Uncertain Parametric Environments
Yannik Schnitzer, Alessandro Abate and David Parker
|
ESOP: Verification
Chair: Viktor Vafeiadis
Room: MDCL 1305
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
Florian Sextl, Adam Rogalewicz, Tomáš Vojnar and Florian Zuleger.
CUTECat: Concolic Execution for Computational Law
Pierre Goutagny, Aymeric Fromherz and Raphaël Monat
Coma, an Intermediate Verification Language with Explicit Abstraction Barriers
Andrei Paskevich, Paul Patault and Jean-Christophe Filliâtre
Cognacy Queries over Dependence Graphs for Transparent Visualisations
Joseph Bond, Cristina David, Minh Nguyen, Dominic Orchard and Roly Perera
|
SPIN
Room: MDCL 1009
On-the-fly Cone-of-Influence Reduction for Model Checking Concurrent Software
Csanád Telbisz, Levente Bajczi, Dániel Szekeres and András Vörös
Locating Concurrency Errors in Windows .NET Applications by Fuzzing over Thread Schedules
Filip Kliber and Pavel Parizek
Presentation of the results of CHC-COMP
Gidon Ernst and Jose F. Morales
|
Award Winner Presentations
Chair: Marieke Huisman
Room: MDCL 1105
Doctoral Dissertation Award
Kevin Batz: Automated Deductive Verification of Probabilistic Programs
Test Of Time Award
K. Rustan M. Leino and Peter Müller: A Basis for Verifying Multi-threaded Programs
Test-Of-Time Tool Award
Daniel Kroening, Peter Schrammel, and Michael Tautschnig: CBMC
Artifact Evaluation Report & Awards
Daniela Kaufmann ad Arnd Hartmanns
|
|
16:00
|
Coffee Break
Room: MDCL
|
|
16:30
16:45
17:00
17:30
|
TACAS: Quantum & GPU
Chair: Arie Gurfinkel
Room: MDCL 1102
GPUexplore-prob: Markov Chain State Space Construction and Verification with GPUs
Jan Heemstra and Anton Wijs
SliQSim: A Quantum Circuit Simulator and Property Checker
Tian-Fu Chen and Jie-Hong Roland Jiang
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs
Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengal, Jyun-Ao Lin and Wei-Lun Tsai
Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs
Muhammad Osama, Dimitrios Thanos and Alfons Laarman
|
ESOP: Concurrency 2
Chair: Nobuko Yoshida
Room: MDCL 1305
Sufficient Conditions for Robustness of RDMA Programs
Guillaume Ambal, Ori Lahav and Azalea Raad
Formulas as Processes, Deadlock-freedom as Choreographies
Matteo Acclavio, Giulia Manara and Fabrizio Montesi
Constructive characterisations of the must-preorder for asynchrony
Giovanni Bernardi, Ilaria Castellani, Paul Laforgue and Léo Stefanesco
|
Test-Comp
Chair: Dirk Beyer
Room: MDCL 1008
|