Abstract is missing.
- PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDPChaitanya Agarwal, Shibashis Guha, Jan Kretínský, Pazhamalai Muruganandham. 3-25 [doi]
- Sampling-Based Verification of CTMCs with Uncertain RatesThom S. Badings, Nils Jansen 0001, Sebastian Junges, Mariëlle Stoelinga, Matthias Volk 0001. 26-47 [doi]
- Playing Against Fair Adversaries in Stochastic Games with Total RewardsPablo F. Castro, Pedro R. D'Argenio, Ramiro Demasi, Luciano Putruele. 48-69 [doi]
- Automated Expected Amortised Cost Analysis of Probabilistic Data StructuresLorenz Leutgeb, Georg Moser, Florian Zuleger. 70-91 [doi]
- Murxla: A Modular and Highly Extensible API Fuzzer for SMT SolversAina Niemetz, Mathias Preiner, Clark W. Barrett. 92-106 [doi]
- FORQ-Based Language Inclusion Formal TestingKyveli Doveri, Pierre Ganty, Nicolas Mazzocchi. 109-129 [doi]
- Sound Automation of Magic WandsThibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller 0001, Alexander J. Summers. 130-151 [doi]
- Divide-and-Conquer Determinization of Büchi Automata Based on SCC DecompositionYong Li 0031, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang 0001. 152-173 [doi]
- From Spot 2.0 to Spot 2.10: What's New?Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko. 174-187 [doi]
- Complementing Büchi Automata with RankerVojtech Havlena, Ondrej Lengál, Barbora Smahlíková. 188-201 [doi]
- Even Faster Conflicts and Lazier Reductions for String SolversAndres Nötzli, Andrew Reynolds 0001, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli. 205-226 [doi]
- Local Search for SMT on Linear Integer ArithmeticShaowei Cai, Bohan Li, Xindi Zhang. 227-248 [doi]
- Reasoning About Data Trees Using CHCsMarco Faella, Gennaro Parlato. 249-271 [doi]
- Verified Erasure Correction in Coq with MathComp and VSTJoshua M. Cohen, Qinshi Wang, Andrew W. Appel. 272-292 [doi]
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllersShenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli. 293-316 [doi]
- Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence ProtocolsJoonwon Choi, Adam Chlipala, Arvind. 317-339 [doi]
- Specification-Guided Learning of Nash Equilibria with High Social WelfareKishor Jothimurugan, Suguman Bansal, Osbert Bastani, Rajeev Alur. 343-363 [doi]
- Synthesizing Fair Decision Trees via Iterative Constraint SolvingJingbo Wang, Yannan Li, Chao Wang. 364-385 [doi]
- SMT-Based Translation Validation for Machine Learning CompilerSeongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, Juneyoung Lee. 386-407 [doi]
- Verifying Fairness in Quantum Machine LearningJi Guan, Wang Fang, Mingsheng Ying. 408-429 [doi]
- MoGym: Using Formal Models for Training and Verifying Decision-making AgentsTimo P. Gros, Holger Hermanns, Jörg Hoffmann 0001, Michaela Klauck, Maximilian A. Köhl, Verena Wolf. 430-443 [doi]
- Synthesis and Analysis of Petri Nets from Causal SpecificationsMateus de Oliveira Oliveira. 447-467 [doi]
- Verifying Generalised and Structural Soundness of Workflow Nets via RelaxationsMichael Blondin, Filip Mazowiecki, Philip Offtermatt. 468-489 [doi]
- Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRETAndreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger, Johann Schumann. 490-504 [doi]
- Information Flow Guided SynthesisBernd Finkbeiner, Niklas Metzger, Yoram Moses. 505-525 [doi]
- Randomized Synthesis for Diversity and Cost Constraints with Control ImprovisationAndreas Gittis, Eric Vin, Daniel J. Fremont. 526-546 [doi]