Volume 61, Issue 1-4

Search all Journal of Automated Reasoning articles

June 2018

Special Issue: Milestones in Interactive Theorem Proving

Issue Editors:

Jeremy Avigad,
Gerwin Klein,
Lawrence Paulson

14 articles in this issue

Introduction to Milestones in Interactive Theorem Proving
Jeremy Avigad
Jasmin Christian Blanchette
Gregor Snelting
EditorialNotes 11 May 2018 Pages: 1 - 8
The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
Grzegorz Bancerek
Czesław Byliński
Karol Pąk
OriginalPaper Open access 25 November 2017 Pages: 9 - 32
Distant Decimals of \(\pi \): Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation
Yves Bertot
Laurence Rideau
Laurent Théry
OriginalPaper 20 December 2017 Pages: 33 - 71
A Verified ODE Solver and the Lorenz Attractor
Fabian Immler
OriginalPaper Open access 22 January 2018 Pages: 73 - 111
CoSMed: A Confidentiality-Verified Social Media Platform
Thomas Bauereiß
Armando Pesenti Gritti
Franco Raimondi
OriginalPaper 02 December 2017 Pages: 113 - 139
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Hao Chen
Xiongnan Wu
Ronghui Gu
OriginalPaper 23 December 2017 Pages: 141 - 189
Verified iptables Firewall Analysis and Verification
Cornelius Diekmann
Lars Hupel
Georg Carle
OriginalPaper Open access 03 January 2018 Pages: 191 - 242
Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler
Andreas Lochbihler
OriginalPaper 08 February 2018 Pages: 243 - 332
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Jasmin Christian Blanchette
Mathias Fleury
Christoph Weidenbach
OriginalPaper Open access 12 March 2018 Pages: 333 - 365
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
Qinxiang Cao
Lennart Beringer
Andrew W. Appel
OriginalPaper 21 February 2018 Pages: 367 - 422
Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka
Cezary Kaliszyk
OriginalPaper Open access 27 February 2018 Pages: 423 - 453
Formalization of the Resolution Calculus for First-Order Logic
Anders Schlichtkrull
OriginalPaper 20 January 2018 Pages: 455 - 484
Formally Verified Algorithms for Upper-Bounding State Space Diameters
Mohammad Abdulaziz
Michael Norrish
Charles Gretton
OriginalPaper 03 February 2018 Pages: 485 - 520
Regular Language Representations in the Constructive Type Theory of Coq
Christian Doczkal
Gert Smolka
OriginalPaper 10 March 2018 Pages: 521 - 553

Volume 61, Issue 1-4

Introduction to Milestones in Interactive Theorem Proving

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

Distant Decimals of \(\pi \): Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

A Verified ODE Solver and the Lorenz Attractor

CoSMed: A Confidentiality-Verified Social Media Platform

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

Verified iptables Firewall Analysis and Verification

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

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

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

Hammer for Coq: Automation for Dependent Type Theory

Formalization of the Resolution Calculus for First-Order Logic

Formally Verified Algorithms for Upper-Bounding State Space Diameters

Regular Language Representations in the Constructive Type Theory of Coq

Navigation