![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Journal of Automated Reasoning, Volume 62
Volume 62, Number 1, January 2019
- Pierre Boutry, Charly Gries, Julien Narboux
, Pascal Schreck:
Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq. 1-68 - Wenda Li
, Grant Olney Passmore, Lawrence C. Paulson
:
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. 69-91 - Stijn de Gouw
, Frank S. de Boer, Richard Bubel, Reiner Hähnle
, Jurriaan Rot, Dominic Steinhöfel
:
Verifying OpenJDK's Sort Method for Generic Collections. 93-126 - Mauro Ferrari
, Camillo Fiorentini
:
Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic. 127-167
Volume 62, Number 2, February 2019
- Jasmin Christian Blanchette
, Stephan Merz:
Selected Extended Papers of ITP 2016: Preface. 169-170 - Hing-Lun Chan
, Michael Norrish
:
Proof Pearl: Bounding Least Common Multiples with Triangles. 171-192 - Thomas Grégoire, Adam Chlipala:
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. 193-213 - Fabian Immler
, Christoph Traut:
The Flow of ODEs: Formalization of Variational Equation and Poincaré Map. 215-236 - Ondrej Kuncar
, Andrei Popescu:
From Types to Sets by Local Type Definition in Higher-Order Logic. 237-260 - Peter Lammich
, S. Reza Sefidgar:
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. 261-280 - Assia Mahboubi, Guillaume Melquiond
, Thomas Sibut-Pinote
:
Formally Verified Approximations of Definite Integrals. 281-300
Volume 62, Number 3, March 2019
- Filip Maric
:
Fast Formal Proof of the Erdős-Szekeres Conjecture for Convex Polygons with at Most 6 Points. 301-329 - Arthur Charguéraud
, François Pottier:
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. 331-365 - Tobias Nipkow
, Hauke Brinkop
:
Amortized Complexity Verified. 367-391 - Alexander Leitsch, Anela Lolic
:
Extraction of Expansion Trees. 393-430
Volume 62, Number 4, April 2019
- Xingyuan Zhang, Christian Urban
:
Selected Extended Papers of ITP 2015: Preface. 431-432 - Frédéric Besson
, Sandrine Blazy
, Pierre Wilke
:
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. 433-480 - Peter Lammich
:
Refinement to Imperative HOL. 481-503 - Sylvain Boulmé
, Alexandre Maréchal:
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. 505-530 - Ondrej Kuncar, Andrei Popescu:
A Consistent Foundation for Isabelle/HOL. 531-555
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.