---
title: "Journal of Automated Reasoning 2018 — papers"
description: "Journal of Automated Reasoning 2018 — papers: 1 paper in the Elamur Research library, with our summaries, ranked by citations."
canonical: "https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/"
---
[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/)

[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

# Journal of Automated Reasoning 2018 — papers

The works of Journal of Automated Reasoning published in 2018 that our library holds (publisher: Springer Science+Business Media): 1 work, listed below with the most cited first; each has a page with our summary, its key points and its references.

[**59** works that year](#all) · [**1** work in our library](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/#works) · [**57** citations of these works](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/#works)

## Most cited papers

By their OpenAlex citations; a paper with our summary links to its page here, the others to the original.

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*

## All works of the year (59)

The most cited first; 1 with our summary link to their page here, the others to the original.

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*

[See all 59 papers in Journal of Automated Reasoning 2018 — papers →](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/papers/)

## Works with our summary in our library (1)

The most cited first (OpenAlex citations plus our library's).

1. **[TacticToe: Learning to Prove with Tactics](https://md.research.elamur.ai/free/en/papers/gauthier-2018-tactictoe-learning-prove-tactics/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Thibault Gauthier, Cezary Kaliszyk, Josef Urban, et al.*2018 · 57 citations*

## Top topics

Topics of its works in our library, with the number of works on each.

[Reasoning (1)](https://md.research.elamur.ai/free/en/topics/reasoning/)

## Fields

[Computer Science (1)](https://md.research.elamur.ai/free/en/shelves/computer-science/)

## Top authors

Authors with a page who published here most often: their works here, and the citations of those works.

[🧑‍🔬**Cezary Kaliszyk**1 work here · 57 citations](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) · [🧑‍🔬**Josef Urban**1 work here · 57 citations](https://md.research.elamur.ai/free/en/authors/josef-urban/) · [🧑‍🔬**Michael Norrish**1 work here · 57 citations](https://md.research.elamur.ai/free/en/authors/michael-norrish/) · [🧑‍🔬**Ramana Kumar**1 work here · 57 citations](https://md.research.elamur.ai/free/en/authors/ramana-kumar/) · [🧑‍🔬**Thibault Gauthier**1 work here · 57 citations](https://md.research.elamur.ai/free/en/authors/thibault-gauthier/)

## Top institutions

Institutions on the bylines of its works here, by the number of works.

[🎓**Universität Innsbruck** Innsbruck · Austria 1 work here](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/) · [🔬**Data61** Sydney · Australia 1 work here](https://md.research.elamur.ai/free/en/labs/data61/) · [🎓**Czech Technical University in Prague** Prague · Czechia 1 work here](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/)

works and citations from OpenAlex and our library.

- [← previous Journal of Automated Reasoning 2013](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/)
- [↑ back to Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)