Skip to main content


Journal of Automated Reasoning

Journal of Automated Reasoning 1-4/2018

Issue 1-4/2018

Special Issue: Milestones in Interactive Theorem Proving

Table of Contents ( 14 Articles )

11-05-2018 | Issue 1-4/2018

Introduction to Milestones in Interactive Theorem Proving

Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu, Gregor Snelting

25-11-2017 | Issue 1-4/2018 Open Access

The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk

20-12-2017 | Issue 1-4/2018

Distant Decimals of : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

Yves Bertot, Laurence Rideau, Laurent Théry

22-01-2018 | Issue 1-4/2018 Open Access

A Verified ODE Solver and the Lorenz Attractor

Fabian Immler

02-12-2017 | Issue 1-4/2018

CoSMed: A Confidentiality-Verified Social Media Platform

Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi

23-12-2017 | Issue 1-4/2018

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu

03-01-2018 | Issue 1-4/2018 Open Access

Verified iptables Firewall Analysis and Verification

Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian Haslbeck, Georg Carle

08-02-2018 | Issue 1-4/2018

Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler

Andreas Lochbihler

12-03-2018 | Issue 1-4/2018 Open Access

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach

21-02-2018 | Issue 1-4/2018

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel

27-02-2018 | Issue 1-4/2018 Open Access

Hammer for Coq: Automation for Dependent Type Theory

Łukasz Czajka, Cezary Kaliszyk

20-01-2018 | Issue 1-4/2018

Formalization of the Resolution Calculus for First-Order Logic

Anders Schlichtkrull

03-02-2018 | Issue 1-4/2018

Formally Verified Algorithms for Upper-Bounding State Space Diameters

Mohammad Abdulaziz, Michael Norrish, Charles Gretton

10-03-2018 | Issue 1-4/2018

Regular Language Representations in the Constructive Type Theory of Coq

Christian Doczkal, Gert Smolka

Current Publications

Premium Partner

    Image Credits