Seminars
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.
Analysis and optimization programs
Management of Data and Information Systems
This seminar is devoted to the various aspects of data management and information systems.
Technologies of Databases and Distributed object-oriented systems
Seminar for 3rd year bachelour students. The seminar is devoted to modern technologies of data management and their applications.
Reports of invited participants
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.
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
Building of EFSM-models Based on Static Analysis of HDL -Descriptions
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
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
Methods of Instrumentation of C-programs for Bugs Search Using Static Code Analysis
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