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
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 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.
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.
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.