16 citations · 42 across the 9 of their papers we have counts for
4 papers · 1 filter
Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types
Nikolaj Bjorner, Ken McMillan, Andrey Rybalchenko
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs di…
An Epistemic Perspective on Consistency of Concurrent Computations
Klaus v. Gleissenthall, Andrey Rybalchenko
Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms.…
Separation Logic Modulo Theories
Juan Antonio Navarro-Pérez, Andrey Rybalchenko
Logical reasoning about program data often requires dealing with heap structures as well as scalar data types. Recent advances in Satisfiability Modular Theory (SMT) already offer…
Generalised Interpolation by Solving Recursion-Free Horn Clauses
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
In this paper we present InterHorn, a solver for recursion-free Horn clauses. The main application domain of InterHorn lies in solving interpolation problems arising in software ve…