7 citations · 7 across the 3 of their papers we have counts for
4 papers
Solving Constrained Horn Clauses over ADTs by Finite Model Finding
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
First-order logic is a natural way of expressing the properties of computation, traditionally used in various program logics for expressing the correctness properties and certifica…
Beyond the Elementary Representations of Program Invariants over Algebraic Data Types
Yurii Kostyukov, Dmitry Mordvinov, Grigory Fedyukovich
First-order logic is a natural way of expressing properties of computation. It is traditionally used in various program logics for expressing the correctness properties and certifi…
Automatic verification of heap-manipulating programs
Yurii Kostyukov, Konstantin Batoev, Dmitry Mordvinov +2
Theoretical foundations of compositional reasoning about heaps in imperative programming languages are investigated. We introduce a novel concept of compositional symbolic memory a…
Verifying Safety of Functional Programs with Rosette/Unbound
Dmitry Mordvinov, Grigory Fedyukovich
The goal of unbounded program verification is to discover an inductive invariant that safely over-approximates all possible program behaviors. Functional languages featuring higher…