Abstract is missing.
- Formalization of Algebraic Theorems in PVS (Invited Talk)Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Andréia B. Avelar, André Luiz Galdino. 1-10 [doi]
- An Interactive SMT Tactic in Coq using Abductive ReasoningHaniel Barbosa, Chantal Keller, Andrew Reynolds 0001, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett. 11-22 [doi]
- Model Checking Omega-Regular Hyperproperties with AutoHyperQRaven Beutner, Bernd Finkbeiner. 23-35 [doi]
- Refining Unification with AbstractionAhmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl. 36-47 [doi]
- Exploring Partial Models with SCLMartin Bromberger, Simon Schwarz, Christoph Weidenbach. 48-72 [doi]
- Trace-based Deductive VerificationRichard Bubel, Dilian Gurov, Reiner Hähnle, Marco Scaletta. 73-95 [doi]
- How Much Should This Symbol Weigh? A GNN-Advised Clause SelectionFilip Bártek, Martin Suda 0001. 96-111 [doi]
- Guiding an Instantiation Prover with Graph Neural NetworksKarel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban. 112-123 [doi]
- Tighter Abstract Queries in Neural Network VerificationElazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz. 124-143 [doi]
- Keep me out of the loop: a more flexible choreographic projectionLuís Cruz-Filipe, Fabrizio Montesi, Robert R. Rasmussen. 144-163 [doi]
- Syntactic computation of Fagin-Halpern conditioning in possibility theoryOmar Ettarguy, Ahlame Begdouri, Salem Benferhat, Carole Delenne. 164-180 [doi]
- Counterfactuals Modulo Temporal LogicsBernd Finkbeiner, Julian Siber. 181-204 [doi]
- An excursion to the border of decidability: between two- and three-variable logicOskar Fiuk, Emanuel Kieronski. 205-223 [doi]
- A Mathematical Benchmark for Inductive Theorem ProversThibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban. 224-237 [doi]
- SMT Solving over Finite Field ArithmeticThomas Hader, Daniela Ritirc, Laura Kovács. 238-256 [doi]
- Overapproximation of Non-Linear Integer Arithmetic for Smart Contract VerificationPetra Hozzová, Jaroslav Bendík, Alexander Nutz, Yoav Rodeh. 257-269 [doi]
- A Fast and Accurate ASP Counting Based Network Reliability EstimatorMohimenul Kabir, Kuldeep S. Meel. 270-287 [doi]
- Collaborative Inference of Combined InvariantsYurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich. 288-305 [doi]
- Analyzing Multiple Conflicts in SAT: An Experimental EvaluationAlbert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao. 306-316 [doi]
- Experiments on Infinite Model Finding in SMT SolvingJulian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk. 317-328 [doi]
- Embedding Intuitionistic into Classical LogicAlexander Pluska, Florian Zuleger. 329-349 [doi]
- On the Complexity of Convex and Reverse Convex Prequadratic ConstraintsRodrigo Raya, Jad Hamza, Viktor Kuncak. 350-368 [doi]
- Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order LogicAlexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown. 369-385 [doi]
- Toward Optimal Radio Colorings of Hypercubes via SAT-solvingBernardo Subercaseaux, Marijn Heule. 386-404 [doi]
- Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety PropertiesJan Tusil, Traian Serbanuta, Jan Obdrzálek. 405-456 [doi]
- Scalable Probabilistic RoutesSuwei Yang, Victor C. Liang, Kuldeep S. Meel. 457-472 [doi]
- Logic of Differentiable Logics: Towards a Uniform Semantics of DLNatalia Slusarz, Ekaterina Komendantskaya, Matthew L. Daggitt, Robert J. Stewart 0001, Kathrin Stark. 473-493 [doi]