default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 64
Volume 64, Number 1, January 2020
- Cheng-Chao Huang, Ming Xu
, Zhi-Bin Li:
A Conflict-Driven Solving Procedure for Poly-Power Constraints. 1-20 - Linh Anh Nguyen:
ExpTime Tableaux with Global Caching for Hybrid PDL. 21-52 - Christoph Benzmüller, Dana S. Scott:
Automating Free Logic in HOL, with an Experimental Application in Category Theory. 53-72 - Xingyuan Zhang, Christian Urban, Chunhan Wu:
Priority Inheritance Protocol Proved Correct. 73-95 - Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen:
Politeness and Combination Methods for Theories with Bridging Functions. 97-134 - Marta Cialdea Mayer:
A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies. 135-165
Volume 64, Number 2, February 2020
- Salvador Lucas:
Using Well-Founded Relations for Proving Operational Termination. 167-195 - Peter Baumgartner, Renate A. Schmidt:
Blocking and Other Enhancements for Bottom-Up Model Generation Methods. 197-251 - Mnacho Echenim, Nicolas Peltier:
Combining Induction and Saturation-Based Theorem Proving. 253-294 - Maximiliano Cristiá, Gianfranco Rossi:
Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations. 295-330 - Wenda Li, Lawrence C. Paulson:
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. 331-360
Volume 64, Number 3, March 2020
- Armin Biere, Cesare Tinelli, Christoph Weidenbach:
Preface to the Special Issue on Automated Reasoning Systems. 361-362 - Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. 363-389 - Matt Kaufmann, J Strother Moore:
Limited Second-Order Functionality in a First-Order Setting. 391-422 - Roberto Sebastiani, Patrick Trentin:
OptiMathSAT: A Tool for Optimization Modulo Theories. 423-460 - Cláudia Nalon, Ullrich Hustadt, Clare Dixon:
sf Kn : Architecture, Refinements, Strategies and Experiments. 461-484 - Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. 485-510 - Leonardo de Moura:
Preface: Selected Extended Papers of CADE 2017. 511 - Peter Lammich:
Efficient Verified (UN)SAT Certificate Checking. 513-532 - Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Strong Extension-Free Proof Systems. 533-554 - Gadi Tellez, James Brotherston:
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. 555-578 - Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar:
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. 579-609 - Andreas Teucke, Christoph Weidenbach:
SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment. 611-640
Volume 64, Number 4, April 2020
- Lorenzo Gheri, Andrei Popescu:
A Formalized General Theory of Syntax with Bindings: Extended Version. 641-675 - Siddhartha Gadgil:
Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs. 677-688 - G. I. Moghaddam, Ranganathan Padmanabhan, Yang Zhang:
Automated Reasoning with Power Maps. 689-697 - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. 699-735 - Mnacho Echenim, Hervé Guiol, Nicolas Peltier:
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. 737-765 - Ricardo Peña:
An Assertional Proof of Red-Black Trees Using Dafny. 767-791
Volume 64, Number 5, June 2020
- Jeremy Avigad, Assia Mahboubi:
Preface: Selected Extended Papers from Interactive Theorem Proving 2018. 793-794 - Christian Doczkal, Damien Pous:
Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. 795-825 - René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada:
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. 827-856 - Matthew L. Daggitt, Ran Zmigrod, Timothy G. Griffin:
A Relaxation of Üresin and Dubois' Asynchronous Fixed-Point Theory in Agda. 857-877 - Manuel Eberl, Max W. Haslbeck, Tobias Nipkow:
Verified Analysis of Random Binary Tree Structures. 879-910 - Hira Taqdees Syeda, Gerwin Klein:
Formal Reasoning Under Cached Address Translation. 911-945 - Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter:
The MetaCoq Project. 947-999
Volume 64, Number 6, August 2020
- Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant:
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. 1001-1050 - Ákos Hajdu, Zoltán Micskei:
Efficient Strategies for CEGAR-Based Model Checking. 1051-1091 - Clemens Ballarin:
Exploring the Structure of an Algebra Text with Locales. 1093-1121 - Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa:
A Library for Formalization of Linear Error-Correcting Codes. 1123-1164
Volume 64, Number 7, October 2020
- Didier Galmiche, Stephan Schulz, Roberto Sebastiani:
Preface: Special Issue of Selected Extended Papers from IJCAR 2018. 1165-1167 - Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann:
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. 1169-1195 - Dominique Larchey-Wendling:
Constructive Decision via Redundancy-Free Proof-Search. 1197-1219 - Anupam Das:
From QBFs to MALL and Back via Focussing. 1221-1245 - Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere:
Simulating Strong Practical Proof Systems with Extended Resolution. 1247-1267 - Marcelo Finger, Sandro Preto:
Probably Partially True: Satisfiability for Łukasiewicz Infinitely-Valued Probabilistic Logic and Related Topics. 1269-1286 - Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan:
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. 1287-1306 - Sylvain Conchon, David Declerck, Fatiha Zaïdi:
Parameterized Model Checking on the TSO Weak Memory Model. 1307-1330 - Dirk Beyer, Marieke Huisman:
Selected and Extended Papers from TACAS 2018: Preface. 1331-1332 - Kshitij Bansal, Eric Koskinen, Omer Tripp:
Synthesizing Precise and Useful Commutativity Conditions. 1333-1359 - Randal E. Bryant:
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams. 1361-1391 - Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato:
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. 1393-1418 - Peter Chini, Roland Meyer, Prakash Saivasan:
Fine-Grained Complexity of Safety Verification. 1419-1444 - Gabriele Costa, Letterio Galletta, Pierpaolo Degano, David A. Basin, Chiara Bodei:
Natural Projection as Partial Model Checking. 1445-1481 - Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann:
Multi-cost Bounded Tradeoff Analysis in MDP. 1483-1522 - Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park:
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines. 1523-1552
Volume 64, Number 8, December 2020
- Ullrich Hustadt, Ana Ozaki, Clare Dixon:
Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations. 1553-1610 - Salvador Lucas, José Meseguer, Raúl Gutiérrez:
The 2D Dependency Pair Framework for Conditional Rewrite Systems - Part II: Advanced Processors and Implementation Techniques. 1611-1662 - Romas Alonderis, Regimantas Pliuskevicius, Aida Pliuskeviciene, Haroldas Giedra:
Loop-Type Sequent Calculi for Temporal Logic. 1663-1684 - Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie:
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. 1685-1729
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-01-24 02:18 CET 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 and maintained by:
the dblp computer science bibliography is funded and supported by:
