Seminars

The Seminar of the Software Engineering Group

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.

Management of Data and Information Systems

This seminar is devoted to the various aspects of data management and information systems.

Kernel ThreadSanitizer: race detection tool in the Linux kernel

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

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

Methods and software of macromodule programming

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.

Model of Dynamic Assessment of Cost, Time and Functional Parameters of Design and Development of Programs and Software Systems

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

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

Static-Dynamic Verification of Linux Kernel File System Drivers

Methods of Modular Verification of Linux Kernel

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

System to Detect Race Conditions in Linux Kernel Modules

Finding All Bugs in the Linux Kernel Modules in a Single Checker Run

Generation of Test Data for Paths Cover in Formal Specification of System of Commands

MicroTESK: Test Program Generation Environment for Microprocessors, Based on Formal Specification of the System of Commands

Building of EFSM-models Based on Static Analysis of HDL -Descriptions

Construction and Using of SMT-Formulas with Uninterpreted Functions to Specify the Predicate Abstraction in the CPAchecker

Search of Race Conditions Using Static Analysis Methods

Reusing Precisions for Efficient Regression Verification (and beyond)

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

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

The High-Level Specification of Microprocessors Memory Hierarchy: Application for Test Programs Generation

MicroTESK Test Programs Generator: Tools for Modeling of the Microprocessor Instruction Code

Dynamic Detection of Races in Java-Programs

Search of the Race Conditions Using Static Analysis Methods

Static and Dynamic Verification of Linux Kernel File Systems Drivers

Diagnostics of the Error of Behavior of Equipment for Dynamic Model-Based Verification

Generation of Test Programs for Microprocessors Based on Their Architecture Models

Combinatorial Generation of OS Software Configuration

Tools for Dynamic Analysis of the Modules and Drivers of the Linux Kernel

Memory Modeling in Software Verification Using Method CEGAR

Modelling of the Environment of Linux Operating System Drivers for Their Static Verification

System for Race Conditions Detecting in the Linux Kernel

Automated Process Testing

Methods of Instrumentation of C-programs for Bugs Search Using Static Code Analysis

Testing of the Tools for Analysis of Coverage Using Metric MC/DC for Compliance with DO-178B Standard and Comments for It

Test Automation of Equipment Models Based on Static Analysis of HDL-Descriptions

Development, Implementation and Performance Analysis of the Modified Transport Protocol

Methods of Synthesis of Homing and Distinguishing experiments with nondeterministic automaton

Verification of the Linux Operating System Drivers Using Predicate Abstraction

Dynamic Verification of Digital Equipment Based on Formal Specification