3 papers
cs.SE2020
Formal specification of a security framework for smart contracts
Mikhail Mandrykin, Jake O'Shannessy, Jacob Payne +1
As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mista…
cs.SE2018
Lemma Functions for Frama-C: C Programs as Proofs
Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov
This paper describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL ext…
cs.SE2018
Deductive Verification of Unmodified Linux Kernel Library Functions
Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conven…