default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 69
Volume 69, Number 1, March 2025
- Anne Baanen
:
Use and Abuse of Instance Parameters in the Lean Mathematical Library. 1 - Grigory Devadze, Victor Magron, Stefan Streif:
Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis. 2 - Enrico Lipparini, Stefan Ratschan:
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem. 3 - Shuhao Song, Bowen Yao:
Formalization of the Prime Number Theorem with a Remainder Term. 4 - Dirk Beyer, Nian-Ze Lee, Philipp Wendler:
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. 5 - Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho:
Correction to: Certified First-Order AC-Unification and Applications. 6 - Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola:
Fast, Verified Computation for HOL ITPs. 7 - Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, Théo Zimmermann:
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. 8
Volume 69, Number 2, June 2025
- Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman:
A Proof-Producing Compiler for Blockchain Applications. 9 - Mnacho Echenim, Nicolas Peltier:
A Direct Procedure to Test Entailment in a Separation Logic of Relations. 10 - Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, K. C. Sivaramakrishnan:
A Mechanically Verified Garbage Collector for OCaml. 11 - Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen:
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. 12 - Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier:
The QSMA Algorithm for Quantifiers in SMT. 13 - Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone:
A Sound and Complete Projection for Global Types. 14 - Ocan Sankur:
Timed Automata Verification and Synthesis Via Finite Automata Learning. 15
Volume 69, Number 3, September 2025
- Tobias Fuchs, Jakob Bach, Ashlin Iser:
Active Learning for SAT Solver Benchmarking. 16 - Mohit Garg, N. Raja, Suneel Sarswat, Abhishek Kr Singh:
Double Auctions: Formalization and Automated Checkers. 17 - Richard Schmoetten, Jacques D. Fleuriot:
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL. 18 - Lawrence Dunn, Val Tannen, Steve Zdancewic:
Structured Monads for Generic First-Order Syntax Metatheory. 22 - Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler:
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate. 23 - Mrudula Balachander, Emmanuel Filiot, Jean-François Raskin:
LTL Reactive Synthesis with a Few Hints. 24 - Christoph Walther:
Reasoning About Incompletely Defined Programs. 25 - Alexei Lisitsa, Zipei Nie, Alexei Vernitski:
Automated reasoning for proving non-orderability of groups. 19 - Jirí Blazek, Pavel Pech:
Solving a problem with GeoGebra current possibilities and limits of CAS tools. 20 - Louis Cheung, Alistair Moffat, Christine Rizkallah:
Formally Verified Suffix Array Construction. 21
Volume 69, Number 4, December 2025
- Frank S. de Boer, Hans-Dieter A. Hiep:
First-order Hybrid Separation Logic. 26 - Zoltán Kovács:
A simple proof of correctness of folding the regular heptagon. 27 - Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, Zaiwen Wen:
Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization. 28 - Predrag Janicic:
Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols. 29 - Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan:
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. 30 - John Derrick, Brijesh Dongol, Chelsea Edmonds, Matt Griffin, Andrei Popescu, Jamie Wright:
Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL. 31 - Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell:
Candle: A Verified Implementation of HOL Light (Extended Version). 32
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-09-02 00:58 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated, funded, and maintained by:
Schloss Dagstuhl - Leibniz Center for Informatics is a member of the Leibniz Association and is funded by the federal government of Germany and the states of Germany, especially Saarland and Rhineland‑Palatinate.
