Skip to main content

Journal of Automated Reasoning OnlineFirst articles

11.11.2019 Open Access

Efficient Strategies for CEGAR-Based Model Checking

Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for …

Ákos Hajdu, Zoltán Micskei


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 …

Ricardo Peña


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 …

Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant


Preface to the Special Issue on Automated Reasoning Systems

Armin Biere, Cesare Tinelli, Christoph Weidenbach

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 …

Gadi Tellez, James Brotherston


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 …

Mnacho Echenim, Hervé Guiol, Nicolas Peltier

17.06.2019 Open Access

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide …

Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada

04.06.2019 Open Access

Efficient Verified (UN)SAT Certificate Checking

SAT solvers decide the satisfiability of Boolean formulas in conjunctive normal form. They are commonly used for software and hardware verification. Modern SAT solvers are highly complex and optimized programs. As a single bug in the solver may …

Peter Lammich


Automated Reasoning with Power Maps

In this paper, we employ automated deduction techniques to prove and generalize some well-known theorems in group theory that involve power maps $$ x^n$$ x n . The difficulty lies in the fact that the term $$x^n$$ x n cannot be expressed in the …

G. I. Moghaddam, R. Padmanabhan, Yang Zhang


Homogeneous Length Functions on Groups: Intertwined Computer and Human Proofs

We describe a case of an interplay between human and computer proving which played a role in the discovery of an interesting mathematical result (Fritz et al. in Algebra Number Theory 12:1773–1786, 2018). The unusual feature of the use of …

Siddhartha Gadgil


A Formalized General Theory of Syntax with Bindings: Extended Version

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying numbers …

Lorenzo Gheri, Andrei Popescu


Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations

In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped …

Maximiliano Cristiá, Gianfranco Rossi

03.04.2019 Open Access

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and …

Wenda Li, Lawrence C. Paulson


Combining Induction and Saturation-Based Theorem Proving

A method is devised to integrate reasoning by mathematical induction into saturation-based proof procedures based on resolution or superposition. The obtained calculi are capable of handling formulas in which some of the quantified variables range …

M. Echenim, N. Peltier

01.03.2019 Open Access

Blocking and Other Enhancements for Bottom-Up Model Generation Methods

Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several …

Peter Baumgartner, Renate A. Schmidt

22.02.2019 Open Access

Strong Extension-Free Proof Systems

We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not …

Marijn J. H. Heule, Benjamin Kiesl, Armin Biere

12.02.2019 Open Access

Priority Inheritance Protocol Proved Correct

In real-time systems with threads, resource locking and priority scheduling, one faces the problem of Priority Inversion. This problem can make the behaviour of threads unpredictable and the resulting bugs can be hard to find. The Priority …

Xingyuan Zhang, Christian Urban, Chunhan Wu


A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

This work describes the Sibyl prover, an implementation of a tableau based proof procedure for multi-modal hybrid logic with the converse, graded and global modalities, and enriched with features largely used in description logics: transitivity …

Marta Cialdea Mayer


Using Well-Founded Relations for Proving Operational Termination

In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded …

Salvador Lucas


Politeness and Combination Methods for Theories with Bridging Functions

The Nelson–Oppen combination method is ubiquitous in Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to …

Paula Chocron, Pascal Fontaine, Christophe Ringeissen