Software Engineering


The Seminar of the Software Engineering Group

Dr. Alexander K. Petrenko.

The seminar of the Software Engineering Group is held on Wednesday at 15:15 in the Institute for System Programming of the Russian Academy of Sciences.

Reports of invited participants

Kernel ThreadSanitizer: race detection tool in the Linux kernel

Andrey Konovalov. Starts at November 23, 2015.

Motivation and Design of Concepts with Subtype Restriction for C# Programming Language

Yuliya Belyakova (postgraduate student of Southern Federal University). Starts at January 21, 2015.

Formal Models and Verification of Properties of Programs Using Object-Oriented Languages

Maksim Krivchikov (Mechanics and Mathematics Faculty and Research Institute of Mechanics, Lomonosov Moscow State University). Starts at December 24, 2014.

Methods and software of macromodule programming

Alexey Sidnev. Starts at December 17, 2014.

One of the open issues in modular approach to programming is the lack of module interfaces standards. The library developer himself defines comfortable data storage structures and data processing functions interfaces. As a result, each library is unique and complications rise related to changing existing modules (libraries) or supporting several libraries.

Development and Research of Methods and Algorithms for Organization of Multi-Client Database Clusters

Evgeny Bottsov (Theoretical computer science of Yaroslavl State University postgraduate student, scientific adviser V.A. Sokolov). Starts at September 18, 2014.

The construction, modeling and verification of PLC programs with LTL-specifications

Riabukhin Dmitry (Theoretical computer science of Yaroslavl State University postgraduate student, scientific adviser E. V. Kuzmin). Starts at September 18, 2014.

Methods of Modular Verification of Linux Kernel

Ilya Zakharov. Starts at May 7, 2014.

The LDV verification system is aimed at the checking of Linux core interfaces usage consistency rules by dynamically loadable modules through statistical verification tools. Simultaneous analysis of both module source code and the rest of the core code is difficult for existing verification tools due to large volume and complexity of such system’s code. Therefore, in LVD system an environment model is generated for target module, and the source code is checked by verification tools along with it. At present, it is possible to build an environment model for each individual module in the LDV system, but such model includes only interaction of module and the core. In this report we will address the problem of module interaction modeling and propose a method of solving it under the LDV system.

Verification of Changes in Code of Linux Kernel Modules

Vladimir Gratinskiy. Starts at April 23, 2014.

System to Detect Race Conditions in Linux Kernel Modules

Nikita Komarov. Starts at April 16, 2014.

Search of Race Conditions Using Static Analysis Methods

Pavel Andrianov. Starts at February 12, 2014.

Reusing Precisions for Efficient Regression Verification (and beyond)

Andreas Stahlbauer. Starts at June 21, 2013.

Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions.

Distributing Verification Tasks with VerifierCloud

Peter Häring. Starts at June 21, 2013.

Software verification of real-world programs is still a time- and resource-consuming process, dependent on sophisticated tools that often require expert knowledge. We present VerifierCloud, a job distribution tool that allows optimal hardware utilization. It is integrated with the CPAchecker framework and can be used to run competitive benchmarks. A web front-end for registration-based software verification is under development to make verification technology more accessible for non-experts.

Dynamic Analysis of Expanded AADL-Models

Denis Buzdalov. Starts at May 15, 2013.

Dynamic Detection of Races in Java-Programs

Vitaly Trifanov, Ph. D. student at St .Petersburg State University. Starts at April 09, 2013.

Search of the Race Conditions Using Static Analysis Methods

Pavel Andrianov. Starts at April 02, 2013.

Combinatorial Generation of OS Software Configuration

Victor Kuliamin. Starts at February 19, 2013.

Memory Modeling in Software Verification Using Method CEGAR

Michail Mandrykin . Starts at January 29, 2013.

System for Race Conditions Detecting in the Linux Kernel

Nikita Komarov. Starts at January 15, 2013.

Automated Process Testing

Vladimir Fedotov. Starts at December 25, 2012.

Development, Implementation and Performance Analysis of the Modified Transport Protocol

Anatoly Sivov (Yaroslavl University postgraduate student). Starts at November 21, 2012.

Methods of Synthesis of Homing and Distinguishing experiments with nondeterministic automaton

Natalia Kushik (Tomsk State University postgraduate student). Starts at November 20, 2012.