62 citations
- Moscow Institute of Physics and TechnologyRU21 papers
- Lomonosov Moscow State UniversityRU11 papers
- Russian Academy of SciencesRU11 papers
- Innopolis UniversityRU8 papers
- Steklov Mathematical InstituteRU6 papers
- Centre National de la Recherche ScientifiqueFR4 papers
- Institute of Physics and TechnologyKZ4 papers
- Moscow Aviation InstituteRU4 papers
- Moscow Power Engineering InstituteRU4 papers
- National Research University Higher School of EconomicsRU4 papers
- École Normale Supérieure de LyonFR3 papers
- Institute for Information Transmission ProblemsRU3 papers
4 papers · 1 filter
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…
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…
Scale effects in internal wave attractors
C. Brouzet, I. N. Sibgatullin, E. V. Ermanyuk +2
As a necessary preliminary step toward geophysically significant extrapolations, we study the scale effects in internal wave attractors in the linear and nonlinear regimes. We use…
Source Code Optimization using Equivalent Mutants
Jorge López, Natalia Kushik, Nina Yevtushenko
A mutant is a program obtained by syntactically modifying a program's source code; an equivalent mutant is a mutant, which is functionally equivalent to the original program. Mutan…