Skip to main content
main-content
Top

Journal

Journal of Automated Reasoning

Journal of Automated Reasoning OnlineFirst articles

03-10-2019

An Assertional Proof of Red–Black Trees Using Dafny

Red–black trees are convenient data structures for inserting, searching, and deleting keys with logarithmic costs. However, keeping them balanced requires careful programming, and sometimes to deal with a high number of cases. In this paper, we …

23-09-2019

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice

We discuss the practical results obtained by the first generation of automated theorem provers based on Deduction modulo theory. In particular, we demonstrate the concrete improvements such a framework can bring to first-order theorem provers with …

13-08-2019

Preface to the Special Issue on Automated Reasoning Systems

09-08-2019 Open Access

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

In this article, we investigate the automated verification of temporal properties of heap-aware programs. We propose a deductive reasoning approach based on cyclic proof. Judgements in our proof system assert that a program has a certain temporal …

04-07-2019

Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL

We formalize in the proof assistant Isabelle essential basic notions and results in financial mathematics. We provide generic formal definitions of concepts such as markets, portfolios, derivative products, arbitrages or fair prices, and we show …

Current Publications

About this journal

The interdisciplinary Journal of Automated Reasoning balances theory, implementation and application. The spectrum of coverage ranges from the presentation of a new inference rule with proof of its logical properties to a detailed account of a computer program designed to solve various problems in industry. Topics include automated theorem proving, logic programming, expert systems, program synthesis and validation, artificial intelligence, computational logic, robotics, and various industrial applications. The contents focus on several aspects of automated reasoning, a field whose objective is the design and implementation of a computer program that serves as an assistant in solving problems and in answering questions that require reasoning.

The Journal of Automated Reasoning provides a forum and a means for exchanging information for those interested purely in theory, those interested primarily in implementation, and those interested in specific research and industrial applications.

Proof Pearls

In addition to regular research articles, the Journal of Automated Reasoning offers the special article type Proof Pearls. The goal is to disseminate insights gleaned from the growing body of machine-checked formalizations and proofs, obtained using both interactive and automated methods. Application areas include the full range from pure mathematics and logic to software and hardware verification. Proof Pearls should be short communications that focus on a few central ideas rather than extended research reports.

Contributions may include: a short, elegant proof of a self-standing result; a novel way of defining a fundamental concept; a notable approach to proving a key lemma in a larger development; a snippet of verified code, carefully engineered to balance efficiency with ease of verification; or a clever or impressive application of automated tools in a particular domain.

Proof Pearls adapt Jon Bentley's notion of a "programming pearl" to the verification paradigm. Proof Pearls should thus encapsulate fundamental insights that are adaptable and reusable, while being elegant and satisfying in their own right. Typical examples could be a verification of Huffman's algorithm, a perspicuous proof of the fundamental theorem of algebra, or a novel axiomatization of a particular algebraic system that was discovered using automated methods.

Submissions will undergo the usual refereeing process, and will be evaluated according to expository and theoretical merit. Systems and formalizations should be made available online.

Additional information

Premium Partner

    Image Credits