---
title: "Journal of Automated Reasoning 2018 — all accepted papers"
description: "All 59 papers of Journal of Automated Reasoning 2018, the most cited first; those with our summary link to it."
canonical: "https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/papers/"
---
Elamur: [Mova](https://md.mova.elamur.ai/free/en/) · [Dictionary](https://md.dictionary.elamur.ai/free/en/) · **Research** · [Groupants](https://md.groupants.elamur.ai/free/en/)

[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/papers/)

[home](https://md.research.elamur.ai/free/en/) / [venues](https://md.research.elamur.ai/free/en/venues/) / [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/) / [2018](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/) / papers

# Journal of Automated Reasoning 2018: all accepted papers

59 papers · the most cited first · [← Journal of Automated Reasoning 2018](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/)

1. **[Hammer for Coq: Automation for Dependent Type Theory ↗](https://doi.org/10.1007/s10817-018-9458-4)**Łukasz Czajka, Cezary Kaliszyk*115 citations*
2. **[VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs ↗](https://doi.org/10.1007/s10817-018-9457-5)**Qinxiang Cao, Lennart Beringer, Samuel Gruetter et al.*96 citations*
3. **[OptiMathSAT: A Tool for Optimization Modulo Theories ↗](https://doi.org/10.1007/s10817-018-09508-6)**Roberto Sebastiani, Patrick Trentin*49 citations*
4. **[A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ↗](https://doi.org/10.1007/s10817-018-9455-7)**Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich et al.*44 citations*
5. **[Efficient Active Automata Learning via Mutation Testing ↗](https://doi.org/10.1007/s10817-018-9486-0)**Bernhard K. Aichernig, Martin Tappler*27 citations*
6. **[A Verified ODE Solver and the Lorenz Attractor ↗](https://doi.org/10.1007/s10817-017-9448-y)**Fabian Immler*26 citations*
7. **[Canonicity for Cubical Type Theory ↗](https://doi.org/10.1007/s10817-018-9469-1)**Simon Huber*22 citations*
8. **[Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae ↗](https://doi.org/10.1007/s10817-018-9499-8)**Susmit Jha, Tuhin Sahai, Vasumathi Raman et al.*21 citations*
9. **[The Flow of ODEs: Formalization of Variational Equation and Poincaré Map ↗](https://doi.org/10.1007/s10817-018-9449-5)**Fabian Immler, Christoph Traut*20 citations*
10. **[The Univalence Axiom in Cubical Sets ↗](https://doi.org/10.1007/s10817-018-9472-6)**Marc Bezem, Thierry Coquand, Simon Huber*20 citations*
11. **[Verified iptables Firewall Analysis and Verification ↗](https://doi.org/10.1007/s10817-017-9445-1)**Cornelius Diekmann, Lars Hupel, Julius Michaelis et al.*19 citations*
12. **[A Consistent Foundation for Isabelle/HOL ↗](https://doi.org/10.1007/s10817-018-9454-8)**Ondřej Kunčar, Andrei Popescu*18 citations*
13. **[From Types to Sets by Local Type Definition in Higher-Order Logic ↗](https://doi.org/10.1007/s10817-018-9464-6)**Ondřej Kunčar, Andrei Popescu*18 citations*
14. **[CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics ↗](https://doi.org/10.1007/s10817-018-9496-y)**Frédéric Besson, Sandrine Blazy, Pierre Wilke*16 citations*
15. **[A Resolution-Based Theorem Prover for {\textsf {K}}_{n}^{}Kn: Architecture, Refinements, Strategies and Experiments ↗](https://doi.org/10.1007/s10817-018-09503-x)**Cláudia Nalon, Ullrich Hustadt, Clare Dixon*15 citations*
16. **[Guarded Cubical Type Theory ↗](https://doi.org/10.1007/s10817-018-9471-7)**Lars Birkedal, Aleš Bizjak, Ranald Clouston et al.*15 citations*
17. **[A Formal Proof of the Expressiveness of Deep Learning ↗](https://doi.org/10.1007/s10817-018-9481-5)**Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow*14 citations*
18. **[Formalization of the Resolution Calculus for First-Order Logic ↗](https://doi.org/10.1007/s10817-017-9447-z)**Anders Schlichtkrull*14 citations*
19. **[Formally Verifying the Solution to the Boolean Pythagorean Triples Problem ↗](https://doi.org/10.1007/s10817-018-9490-4)**Luı́s Cruz-Filipe, João P. Marques-Silva, Peter Schneider–Kamp*14 citations*
20. **[A Proof Theory for Model Checking ↗](https://doi.org/10.1007/s10817-018-9475-3)**Quentin Heath, Dale Miller*12 citations*
21. **[A Verified Generational Garbage Collector for CakeML ↗](https://doi.org/10.1007/s10817-018-9487-z)**Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola*12 citations*
22. **[Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches ↗](https://doi.org/10.1007/s10817-018-9461-9)**Peter Lammich, Andreas Lochbihler*11 citations*
23. **[On the Generation of Quantified Lemmas ↗](https://doi.org/10.1007/s10817-018-9462-8)**Gabriel Ebner, Stefan Hetzl, Alexander Leitsch et al.*11 citations*
24. **[Long-Distance Q-Resolution with Dependency Schemes ↗](https://doi.org/10.1007/s10817-018-9467-3)**Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider*10 citations*
25. **[Formally Verified Algorithms for Upper-Bounding State Space Diameters ↗](https://doi.org/10.1007/s10817-018-9450-z)**Mohammad Abdulaziz, Michael Norrish, Charles Gretton*9 citations*
26. **[Semantics of Mizar as an Isabelle Object Logic ↗](https://doi.org/10.1007/s10817-018-9479-z)**Cezary Kaliszyk, Karol Pąk*9 citations*
27. **[Formally Verified Approximations of Definite Integrals ↗](https://doi.org/10.1007/s10817-018-9463-7)**Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote*8 citations*
28. **[Mechanized Metatheory Revisited ↗](https://doi.org/10.1007/s10817-018-9483-3)**Dale Miller*8 citations*
29. **[An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains ↗](https://doi.org/10.1007/s10817-018-9494-0)**Hadar Frenkel, Orna Grümberg, Sarai Sheinvald*7 citations*
30. **[Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory ↗](https://doi.org/10.1007/s10817-018-9480-6)**Dominik Kirst, Gert Smolka*7 citations*
31. **[Extraction of Expansion Trees ↗](https://doi.org/10.1007/s10817-018-9453-9)**Alexander Leitsch, Anela Lolić*7 citations*
32. **[Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler ↗](https://doi.org/10.1007/s10817-018-9452-x)**Andreas Lochbihler*7 citations*
33. **[Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF ↗](https://doi.org/10.1007/s10817-018-9482-4)**Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew et al.*7 citations*
34. **[Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation ↗](https://doi.org/10.1007/s10817-018-9493-1)**Wenxi Wang, Harald Søndergaard, Peter J. Stuckey*7 citations*
35. **[An Isabelle/HOL Formalisation of Green’s Theorem ↗](https://doi.org/10.1007/s10817-018-9495-z)**Mohammad Abdulaziz, Lawrence Charles Paulson*6 citations*
36. **[From Signatures to Monads in UniMath ↗](https://doi.org/10.1007/s10817-018-9474-4)**Benedikt Ahrens, Ralph Matthes, Anders Mörtberg*6 citations*
37. **[Regular Language Representations in the Constructive Type Theory of Coq ↗](https://doi.org/10.1007/s10817-018-9460-x)**Christian Doczkal, Gert Smolka*6 citations*
38. **[Call-by-Value Lambda Calculus as a Model of Computation in Coq ↗](https://doi.org/10.1007/s10817-018-9484-2)**Yannick Forster, Gert Smolka*5 citations*
39. **[Introduction to Milestones in Interactive Theorem Proving ↗](https://doi.org/10.1007/s10817-018-9465-5)**Jeremy D. Avigad, Jasmin Christian Blanchette, Gerwin Klein et al.*5 citations*
40. **[Limited Second-Order Functionality in a First-Order Setting ↗](https://doi.org/10.1007/s10817-018-09505-9)**Matt Kaufmann, J Strother Moore*5 citations*
41. **[The James Construction and \pi _4(\mathbb {S}^{3}) in Homotopy Type Theory ↗](https://doi.org/10.1007/s10817-018-9468-2)**Guillaume Brunerie*5 citations*
42. **[Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics ↗](https://doi.org/10.1007/s10817-018-9466-4)**Matteo Acclavio*4 citations*
43. **[Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants ↗](https://doi.org/10.1007/s10817-018-9497-x)**Andrew Sogokon, Paul B. Jackson, Taylor Thomas Johnson*4 citations*
44. **[Effect Polymorphism in Higher-Order Logic (Proof Pearl) ↗](https://doi.org/10.1007/s10817-018-9476-2)**Andreas Lochbihler*3 citations*
45. **[Formalization of Geometric Algebra in HOL Light ↗](https://doi.org/10.1007/s10817-018-9498-9)**Liming Li, Zhiping Shi, Yong Guan et al.*3 citations*
46. **[Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra ↗](https://doi.org/10.1007/s10817-018-9492-2)**Sylvain Boulmé, Alexandre Maréchal*3 citations*
47. **[Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology ↗](https://doi.org/10.1007/s10817-018-9489-x)**Yannick Zakowski, David Cachera, Delphine Demange et al.*3 citations*
48. **[A Verified Implementation of Algebraic Numbers in Isabelle/HOL ↗](https://doi.org/10.1007/s10817-018-09504-w)**Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada*2 citations*
49. **[ExpTime Tableaux with Global Caching for Hybrid PDL ↗](https://doi.org/10.1007/s10817-018-09506-8)**Linh Anh Nguyen*2 citations*
50. **[Linear Numeral Systems ↗](https://doi.org/10.1007/s10817-018-9456-6)**Ian Mackie*2 citations*
51. **[Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms ↗](https://doi.org/10.1007/s10817-018-9451-y)**Thomas Grégoire, Adam J. Chlipala*2 citations*
52. **[A Conflict-Driven Solving Procedure for Poly-Power Constraints ↗](https://doi.org/10.1007/s10817-018-09501-z)**Cheng-Chao Huang, Ming Xu, Zhibin Li*1 citation*
53. **[A PSpace Algorithm for Acyclic Epistemic DL \mathcal {ALCS}5_m ALCS 5 m ↗](https://doi.org/10.1007/s10817-018-9473-5)**Jia Tao*1 citation*
54. **[Classification of Finite Fields with Applications ↗](https://doi.org/10.1007/s10817-018-9485-1)**Hing-Lun Chan, Michael Norrish*1 citation*
55. **[Formalization of the Fundamental Group in Untyped Set Theory Using Auto2 ↗](https://doi.org/10.1007/s10817-018-9478-0)**Bohua Zhan*1 citation*
56. **[Selected Extended Papers of NFM 2017: Preface ↗](https://doi.org/10.1007/s10817-018-9488-y)**Clark Barrett, Temesghen Kahsai*1 citation*
57. **[Preface: Special Issue on Homotopy Type Theory and Univalent Foundations ↗](https://doi.org/10.1007/s10817-018-9491-3)**Peter LeFanu Lumsdaine, Nicolas Tabareau
58. **[Selected Extended Papers of ITP 2016: Preface ↗](https://doi.org/10.1007/s10817-018-9470-8)**Jasmin Christian Blanchette, Stephan Merz
59. **[Selected Extended Papers of ITP 2017 ↗](https://doi.org/10.1007/s10817-018-09500-0)**Maurício Ayala-Rincón, Cesar A. Munoz
- [← back to](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/) — Journal of Automated Reasoning 2018