📰 Journal of Automated Reasoning 2018: all accepted papers

59 papers · the most cited first · ← Journal of Automated Reasoning 2018

1. Hammer for Coq: Automation for Dependent Type Theory ↗Łukasz Czajka, Cezary Kaliszyk115 citations
2. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs ↗Qinxiang Cao, Lennart Beringer, Samuel Gruetter et al.96 citations
3. OptiMathSAT: A Tool for Optimization Modulo Theories ↗Roberto Sebastiani, Patrick Trentin49 citations
4. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ↗Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich et al.44 citations
5. Efficient Active Automata Learning via Mutation Testing ↗Bernhard K. Aichernig, Martin Tappler27 citations
6. A Verified ODE Solver and the Lorenz Attractor ↗Fabian Immler26 citations
7. Canonicity for Cubical Type Theory ↗Simon Huber22 citations
8. Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae ↗Susmit Jha, Tuhin Sahai, Vasumathi Raman et al.21 citations
9. The Flow of ODEs: Formalization of Variational Equation and Poincaré Map ↗Fabian Immler, Christoph Traut20 citations
10. The Univalence Axiom in Cubical Sets ↗Marc Bezem, Thierry Coquand, Simon Huber20 citations
11. Verified iptables Firewall Analysis and Verification ↗Cornelius Diekmann, Lars Hupel, Julius Michaelis et al.19 citations
12. A Consistent Foundation for Isabelle/HOL ↗Ondřej Kunčar, Andrei Popescu18 citations
13. From Types to Sets by Local Type Definition in Higher-Order Logic ↗Ondřej Kunčar, Andrei Popescu18 citations
14. CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics ↗Frédéric Besson, Sandrine Blazy, Pierre Wilke16 citations
15. A Resolution-Based Theorem Prover for {\textsf {K}}_{n}^{}Kn: Architecture, Refinements, Strategies and Experiments ↗Cláudia Nalon, Ullrich Hustadt, Clare Dixon15 citations
16. Guarded Cubical Type Theory ↗Lars Birkedal, Aleš Bizjak, Ranald Clouston et al.15 citations
17. A Formal Proof of the Expressiveness of Deep Learning ↗Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow14 citations
18. Formalization of the Resolution Calculus for First-Order Logic ↗Anders Schlichtkrull14 citations
19. Formally Verifying the Solution to the Boolean Pythagorean Triples Problem ↗Luı́s Cruz-Filipe, João P. Marques-Silva, Peter Schneider–Kamp14 citations
20. A Proof Theory for Model Checking ↗Quentin Heath, Dale Miller12 citations
21. A Verified Generational Garbage Collector for CakeML ↗Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola12 citations
22. Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches ↗Peter Lammich, Andreas Lochbihler11 citations
23. On the Generation of Quantified Lemmas ↗Gabriel Ebner, Stefan Hetzl, Alexander Leitsch et al.11 citations
24. Long-Distance Q-Resolution with Dependency Schemes ↗Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider10 citations
25. Formally Verified Algorithms for Upper-Bounding State Space Diameters ↗Mohammad Abdulaziz, Michael Norrish, Charles Gretton9 citations
26. Semantics of Mizar as an Isabelle Object Logic ↗Cezary Kaliszyk, Karol Pąk9 citations
27. Formally Verified Approximations of Definite Integrals ↗Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote8 citations
28. Mechanized Metatheory Revisited ↗Dale Miller8 citations
29. An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains ↗Hadar Frenkel, Orna Grümberg, Sarai Sheinvald7 citations
30. Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory ↗Dominik Kirst, Gert Smolka7 citations
31. Extraction of Expansion Trees ↗Alexander Leitsch, Anela Lolić7 citations
32. Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler ↗Andreas Lochbihler7 citations
33. Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF ↗Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew et al.7 citations
34. Wombit: A Portfolio Bit-Vector Solver Using Word-Level Propagation ↗Wenxi Wang, Harald Søndergaard, Peter J. Stuckey7 citations
35. An Isabelle/HOL Formalisation of Green’s Theorem ↗Mohammad Abdulaziz, Lawrence Charles Paulson6 citations
36. From Signatures to Monads in UniMath ↗Benedikt Ahrens, Ralph Matthes, Anders Mörtberg6 citations
37. Regular Language Representations in the Constructive Type Theory of Coq ↗Christian Doczkal, Gert Smolka6 citations
38. Call-by-Value Lambda Calculus as a Model of Computation in Coq ↗Yannick Forster, Gert Smolka5 citations
39. Introduction to Milestones in Interactive Theorem Proving ↗Jeremy D. Avigad, Jasmin Christian Blanchette, Gerwin Klein et al.5 citations
40. Limited Second-Order Functionality in a First-Order Setting ↗Matt Kaufmann, J Strother Moore5 citations
41. The James Construction and \pi _4(\mathbb {S}^{3}) in Homotopy Type Theory ↗Guillaume Brunerie5 citations
42. Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics ↗Matteo Acclavio4 citations
43. Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants ↗Andrew Sogokon, Paul B. Jackson, Taylor Thomas Johnson4 citations
44. Effect Polymorphism in Higher-Order Logic (Proof Pearl) ↗Andreas Lochbihler3 citations
45. Formalization of Geometric Algebra in HOL Light ↗Liming Li, Zhiping Shi, Yong Guan et al.3 citations
46. Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra ↗Sylvain Boulmé, Alexandre Maréchal3 citations
47. Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology ↗Yannick Zakowski, David Cachera, Delphine Demange et al.3 citations
48. A Verified Implementation of Algebraic Numbers in Isabelle/HOL ↗Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada2 citations
49. ExpTime Tableaux with Global Caching for Hybrid PDL ↗Linh Anh Nguyen2 citations
50. Linear Numeral Systems ↗Ian Mackie2 citations
51. Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms ↗Thomas Grégoire, Adam J. Chlipala2 citations
52. A Conflict-Driven Solving Procedure for Poly-Power Constraints ↗Cheng-Chao Huang, Ming Xu, Zhibin Li1 citation
53. A PSpace Algorithm for Acyclic Epistemic DL \mathcal {ALCS}5_m ALCS 5 m ↗Jia Tao1 citation
54. Classification of Finite Fields with Applications ↗Hing-Lun Chan, Michael Norrish1 citation
55. Formalization of the Fundamental Group in Untyped Set Theory Using Auto2 ↗Bohua Zhan1 citation
56. Selected Extended Papers of NFM 2017: Preface ↗Clark Barrett, Temesghen Kahsai1 citation
57. Preface: Special Issue on Homotopy Type Theory and Univalent Foundations ↗Peter LeFanu Lumsdaine, Nicolas Tabareau
58. Selected Extended Papers of ITP 2016: Preface ↗Jasmin Christian Blanchette, Stephan Merz
59. Selected Extended Papers of ITP 2017 ↗Maurício Ayala-Rincón, Cesar A. Munoz

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2018/papers/