16 citations · 42 across the 9 of their papers we have counts for
9 papers
Efficient CTL Verification via Horn Constraints Solving
Tewodros A. Beyene, Corneliu Popeea, Andrey Rybalchenko
The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the proble…
Proceedings First Workshop on Horn Clauses for Verification and Synthesis
Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko +1
This volume contains the proceedings of HCVS 2014, the First Workshop on Horn Clauses for Verification and Synthesis which was held on July 17, 2014 in Vienna, Austria as a satelli…
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
Expressing program correctness often requires relating program data throughout (different branches of) an execution. Such properties can be represented using CTL+FO, a logic that a…
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
Andrey Rybalchenko
We show how automatic tools for the verification of linear and branching time properties of procedural, multi-threaded, and functional programs as well as program synthesis can be…
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.…