3 citations · 4 across the 4 of their papers we have counts for
4 papers
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…
HMC: Verifying Functional Programs Using Abstract Interpreters
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
We present Hindley-Milner-Cousots (HMC), an algorithm that allows any interprocedural analysis for first-order imperative programs to be used to verify safety properties of typed h…