Accepted Papers

– Multi-perspective correctness of programs
Eduard Kamburjan (IT University of Copenhagen, Denmark) and Dilian Gurov (KTH Royal Institute of Technology, Sweden)

– A rely-guarantee-based simulation for cooperative semantics
Kevin Tran (UNSW Sydney, Australia), Johannes Åman Pohjola (University of Gothenburg, Sweden), Rob Sison (UNSW Sydney, Australia), and Gerwin Klein (Proofcraft & UNSW Sydney, Australia)

– PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems
Ben Wooding (Newcastle University, United Kingdom), Viacheslav Horbanov (Newcastle University, United Kingdom), and Abolfazl Lavaei (Newcastle University, United Kingdom)

– Graphical Quadratic Algebra
Dario Stein (Radboud University Nijmegen, Netherlands), Fabio Zanasi (University College London, United Kingdom), Robin Piedeleu (University College London, United Kingdom), and Richard Samuelson (University of Florida, United States)

– Compositional Interface Refinement Through Subtyping in Probabilistic Session Types
Paula Blechschmidt (TU Berlin, Germany), Kirstin Peters (Universität Augsburg, Germany), and Uwe Nestmann (TU Berlin, Germany)

– Efficient Interpolation Beyond Cut-Free Proofs: Admissible Cuts and Optimized Extraction
Anela Lolic (TU Wien, Austria) and Simon Corbard (ENS Paris Saclay – Université Paris Saclay, France)

– Lean4Less: Eliminating Definitional Equalities in Lean via an Extensional-to-Intensional Translation
Rishikesh Vaishnav (Deducteam, ENS Paris-Saclay, Inria, France)

– The Spiral of Silence in Multi-Agent Models for Opinion Formation
David Gaona (Universidad del Valle, Colombia), Juan Francisco Díaz (Universidad del Valle, Colombia), Jesús Alexander Aranda (Universidad del Valle, Colombia), and Frank Valencia (CNRS-LIX, École Polytechnique de Paris, France)

– Weighted Automata for Exact Inference in Discrete Probabilistic Programs
Dominik Geißler (Technische Universität Berlin, Germany) and Tobias Winkler (RWTH Aachen University, Germany)

– On Asynchronous Multiparty Session Types for Federated Learning
Ivan Prokic (University of Novi Sad, Serbia), Simona Prokic (University of Novi Sad, Serbia), Silvia Ghilezan (University of Novi Sad, Mathematical Institute SASA, Serbia), Alceste Scalas (Technical University of Denmark, Denmark), and Nobuko Yoshida (University of Oxford, United Kingdom)

– Forward and Backward Simulations for Partially Observable Probability
Chris Chen (Macquarie University, Australia), Annabelle McIver (Macquarie University, Australia), and Carroll Morgan (The University of New South Wales, Australia)

– Efficient AND Protocols Resistant to Maliciously Revealing a Single Card
Koichi Koizumi (National Institute of Technology, Fukushima College, Japan), Minato Abe (National Institute of Technology, Fukushima College, Japan), Eikoh Chida (National Institute of Technology, Ichinoseki College, Japan), and Takaaki Mizuki (Tohoku University, Japan)

– Iteratively Synthesizing ϵ-robust Barrier Certificates for Neural Network Controlled Systems
Luo Yi (NanJing University, China), Chen Xin (NanJing University, China), Dai Jin (NanJing University, China), Tang Enyi (Nanjing University, China), and Li Xuandong (NanJing University, China)

– Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets (Tool Paper)
Kira Stæhr Pedersen (Aalborg University, Denmark) and Jiri Srba (Aalborg University, Denmark)

– Pomsets for Process Management: a Healthcare Case Study
Roberto Guanciale (KTH, Sweden), Sourabh Pal (Universita di Bologna, Italy), Emilio Tuosto (Gran Sasso Science Institute, Italy), Ivan Lanese (Universita di Bologna, Italy), and Massimo Clo (Direzione Generale Cura della Persona, Salute e Welfare, Emilia Romagna, Italy)

– From Program Logics towards Language Logics
Matteo Cimini (University of Massachusetts Lowell, United States)

– Ulam’s metric in higher dimensions
Andrzej Kozik (Institute of Computer Science, Opole University, Poland) and Sebastian Bala (Institute of Computer Science, Opole University, Poland)

– Verification of the Release-Acquire Semantics
Elli Anastasiadi (Aalborg University, Greece), Parosh Aziz Abdulla (Uppsala University, Sweden), Mohamed Faouzi Atig (Uppsala University, Sweden), and Samuel Grahn (Uppsala University, Sweden)

– A Variety of Request-Response Specifications
Daichi Aiba (National Institute of Informatics, Japan), Masaki Waga (Kyoto University, Japan), Hiroya Fujinami (National Institute of Informatics, Japan), Koko Muroya (Ochanomizu University, Japan), Shuntaro Ouchi (Mitsubishi Electric Corporation, Japan), Naoki Ueda (Mitsubishi Electric Corporation, Japan), Yosuke Yokoyama (Mitsubishi Electric Corporation, Japan), Yuta Wada (Mitsubishi Electric Corporation, Japan), and Ichiro Hasuo (National Institute of Informatics, Japan)

– On Computational Aspects of Ordered Matching Problems (Short paper)
Jaroslav Nešetřil (Computer Science Institute, Faculty of Mathematics and Physics, Charles University, Prague, Czechia), Paweł Rzążewski (Warsaw University of Technology, Poland), Andreas Emil Feldmann (University of Sheffield, United Kingdom), and Michal Certik (Charles University, Prague, Czechia)

– AP-Observation Automata for Abstraction-based Verification of Continuous-time Systems
Sasinee Pruekprasert (The University of Tokyo, Japan) and Clovis Eberhart (Tohoku University, Japan)

– Active Learning of Symbolic Mealy Automata
Kengo Irie (Kyoto University, Japan), Masaki Waga (Kyoto University, Japan), and Kohei Suenaga (Kyoto University, Japan)

– Safe Multi-Agent Reinforcement Learning using Formal Runtime Enforcement: A Case Study (Short paper)
Vedanta Mohapatra (Indian Institute of Technology Bhubaneswar, India), Ayush Anand (Indian Institute of Technology Bhubaneswar, India), and Srinivas Pinisetty (Indian Institute of Technology Bhubaneswar, India)