Abstract is missing.
- Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability TestingChia-Hsuan Lu, Tony Tan, Michael Benedikt. 3-22 [doi]
- Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCamlJoão Madeira Pereira, Filipe Marques, Pedro Adão, Hichem Rami Ait El Hara, Léo Andrès, Arthur Carcano, Pierre Chambart, Petar Maksimovic 0001, Nuno Santos 0001, José Fragoso Santos. 23-44 [doi]
- Syntactically Convex Model-Based Projection for Linear Real ArithmeticAnna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson. 45-65 [doi]
- Bit-Precise Interpolation in BitwuzlaAina Niemetz, Mathias Preiner. 66-88 [doi]
- Orbitopal Fixing in SATMarkus Anders, Cayden R. Codel, Marijn J. H. Heule. 89-109 [doi]
- Automatically Tightening Access Control Policies with RestricterKa Lok Wu, Christa Jenkins, Scott D. Stoller, Omar Chowdhury. 110-129 [doi]
- Parallel SMT Solving via Iterative Tree PartitioningTomás Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh, Natasha Sharygina. 130-149 [doi]
- Exploring the SMT-LIB Benchmark LibraryHans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli. 150-169 [doi]
- Massively Parallel Bit-Precise Verification with Bitwuzla and MallobDominik Schreiber 0001, Aina Niemetz, Mathias Preiner. 170-191 [doi]
- SMT(LIA) Sampling with High DiversityYong Lai 0001, Junjie Li, Chuan Luo 0002. 192-212 [doi]
- BDD-Based Formula Approximations for Quantified Bit-Vector SatisfiabilityJakub Horák, Martin Jonás. 213-232 [doi]
- SMTScope: Automated and Efficient Analysis of SMT TracesJonás Fiala, Peter Müller 0001. 233-251 [doi]
- Hint-Based SMT Proof ReconstructionJoshua Clune, Haniel Barbosa, Jeremy Avigad. 255-275 [doi]
- Incremental Forward Reasoning for White-Box Proof SearchXavier Généreux, Jannis Limperg. 276-294 [doi]
- Enumerating Choice Terms in Model-Based Quantifier InstantiationLydia Kondylidou, Andrew Reynolds 0001, Jasmin Blanchette, Cesare Tinelli. 295-314 [doi]
- Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)Kilian Lichtner, Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche. 315-323 [doi]
- QSOLE: Automatic QBF Equivalence CheckingPeter Pfeiffer, Mark Peyrer, Daniel Große, Martina Seidl. 324-332 [doi]
- Real-time Proof Checking for Distributed Incremental SAT SolvingDominik Schreiber 0001, Mathias Fleury, Katalin Fazekas, Armin Biere. 333-352 [doi]
- Quantifier Elimination Meets TreewidthHao Wu 0085, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An 0001, Bican Xia, Naijun Zhan. 353-373 [doi]
- Concurrent Permissive Strategy TemplatesAshwani Anand, Christel Baier, Calvin Chau, Sascha Klüppelholz, Ali Mirzaei, Satya Prakash Nayak, Anne-Kathrin Schmuck. 377-397 [doi]
- Modular Attractor Acceleration in Infinite-State GamesPhilippe Heim, Rayna Dimitrova. 398-418 [doi]
- A Myhill-Nerode Characterization and Active Learning for One-Clock Timed AutomataKyveli Doveri, Pierre Ganty, B. Srivathsan. 419-437 [doi]
- Faster Signature Refinement for Branching Bisimilarity MinimizationJan Martens 0001, Maurice Laveaux. 438-456 [doi]
- MightyPPL: Model Checking MITL with Past and Pnueli ModalitiesHsi-Ming Ho, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh K. Pandya. 457-479 [doi]
- f Learning Meets Boolean Set CoverGabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon, Pierre Vandenhove. 480-501 [doi]
- Robust Verification of Concurrent Stochastic GamesAngel Y. He, David Parker. 505-525 [doi]
- Multiple Long-Run and ømega-Regular Objectives in MDPsJulius Ide, Joost-Pieter Katoen, Hannah Mertens, Tim Quatmann. 526-546 [doi]
- Computing Fixpoints of Learned Functions: Chaotic Iteration and Simple Stochastic GamesPaolo Baldan, Sebastian Gurke, Barbara König 0001, Florian Wittbold. 547-565 [doi]
- DeGAS: Gradient-Based Optimization of Probabilistic Programs without SamplingFrancesca Randone, Romina Doz, Mirco Tribastone, Luca Bortolussi. 566-585 [doi]
- AKR: A Model Checker for an Adaptative Probabilistic Knowing-How LogicValentin Cassano, Pablo F. Castro, Pedro R. D'Argenio, Raul Fervari. 586-593 [doi]
- Driving by Disproof: A Practical Model Checking Approach to Fleet CoordinationLukas König, Christian Schildwächter, Michaela Klauck, Christian Heinzemann. 597-619 [doi]
- VeriLHyS: a Framework for LTL Specification and Verification of Hybrid SystemsLudovico Battista, Stefano Tonetta, Gianni Zampedri. 620-639 [doi]
- TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise SemanticsS. Akshay 0001, Prerak Contractor, Paul Gastin, R. Govind 0001, B. Srivathsan. 640-659 [doi]
- Trace Repair for Temporal Behavior TreesSebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner, Sriram Sankaranarayanan 0001. 660-679 [doi]