Abstract is missing.
- DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic TheoriesNick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen, Lee Pike, John Backes. 3-23 [doi]
- Z3-Noodler: An Automata-based String SolverYu-Fang Chen 0001, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc. 24-33 [doi]
- TaSSAT: Transfer and Share SATMd. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule. 34-42 [doi]
- Speculative SAT Modulo SATHari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel. 43-60 [doi]
- Happy Ending: An Empty Hexagon in Every Set of 30 PointsMarijn J. H. Heule, Manfred Scheucher. 61-80 [doi]
- Fully Generalized Reactivity(1) SynthesisRüdiger Ehlers, Ayrat Khalimov 0003. 83-102 [doi]
- Knor: reactive synthesis using OinkTom van Dijk, Feije van Abbema, Naum Tomov. 103-122 [doi]
- On Dependent Variables in Reactive SynthesisS. Akshay 0001, Eliyahu Basa, Supratik Chakraborty, Dror Fried. 123-143 [doi]
- CESAR: Control Envelope Synthesis via Angelic RefinementsAditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer. 144-164 [doi]
- Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational DomainsLukas Westhofen 0001, Christian Neurohr, Jean Christoph Jung, Daniel Neider. 167-187 [doi]
- Deciding Boolean Separation Logic via Small ModelsTomás Dacík, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger. 188-206 [doi]
- Asynchronous Subtyping by Trace RelaxationLaura Bocchi, Andy King, Maurizio Murgia 0001. 207-226 [doi]
- SootUp: A Redesign of the Soot Static Analysis FrameworkKadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo, Dongjie He. 229-247 [doi]
- Formally verified asymptotic consensus in robust networksMohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou. 248-267 [doi]
- Formally Verifying an Efficient SorterBernhard Beckert, Peter Sanders 0001, Mattias Ulbrich, Julian Wiesler, Sascha Witt. 268-287 [doi]
- Explainable Online Monitoring of Metric First-Order Temporal LogicLeonardo Lima 0001, Jonathan Julián Huerta y Munive, Dmitriy Traytel. 288-307 [doi]
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOLHanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds 0001, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. 311-330 [doi]
- Automate where Automation Fails: Proof Strategies for Frama-C/WPLoïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov. 331-339 [doi]
- VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier VerificationMertcan Temel. 340-349 [doi]
- A Logical Treatment of Finite AutomataNishant Rodrigues, Mircea Sebe, Xiaohong Chen 0002, Grigore Rosu. 350-369 [doi]
- A State-of-the-Art Karp-Miller Algorithm Certified in CoqThibault Hilaire, David Ilcinkas, Jérôme Leroux. 370-389 [doi]