3 papers
cs.PL2021
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…
cs.PL2021
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…
cs.PL2019
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…