Colloquium Program


May 28, 2020

09:45-10:00

Welcome Speech

10:00-11:40

Compiler Technologies and Formal Verification

10:00-10:20

Modeling of Library Functions in the Industrial Static Code Analyzer
Mikhail Belyaev (ISP RAS), Egor Romanenkov (Moscow State University), Valery Ignatyev (ISP RAS, MSU)
(slides)

10:20-10:40

Static Analyzer Debugging and Quality Assurance Approaches
Maxim Menshikov (St. Petersburg State University)
(slides)

10:40-11:00

Code Generation for Real Arithmetic in Architecture MIPS
Ivan Arkhipov (St. Petersburg State University)
(slides)

11:00-11:20

Architecture of Machine Code Deductive Verification System
Pavel Putro (ISP RAS, Higher School of Economics), Alexander Kamkin, Alexey Khoroshilov, Artem Kotsynyak (ISP RAS)

11:20-11:40

Verified Isabelle/HOL Tactic for the Theory of Bounded Linear Integer Arithmetic Based on Quantifier Instantiation and SMT
Rafael Sadykov (Moscow State University), Mikhail Mandrykin (ISP RAS)
(slides)

11:40-12:00

Coffee Break / Discussion

12:00-12:40

Requirements Management and Lifecycle Support

12:00-12:20

Analysis of Russian Software Supporting Onboard Systems Development Lifecycle in Context of Import Substitution Policy
Natalia Gorelits, Aleksandra Gukova (GosNIIAS)
(slides)

12:20-12:40

Assessing the Quality of the Requirements Specification by Applying GQM Approach and Using NLP Tools
Evgenii Timoshchuk

12:40-14:00

Lunch

14:00-15:20

Software Models and Modeling Languages

14:00-14:20

On Reduced Forms of Initialized Finite State Machines with Timeouts
Aleksandr Tvardovskii (Tomsk State University), Nina Yevtushenko (ISP RAS)
(slides)

14:20-14:40

Techniques for Implementation of Symbolically Interpretable Haskell EDSLs
Grigoriy Volkov (ISP RAS, Higher School of Economics)
(slides)

14:40-15:00

Formal Rules for Producing Object Notation by EXPRESS Schema
Georgii Semenov (ITMO University)
(slides)

15:00-15:20

HP-Graph as a Basis of a DSM Platform Visual Model Editor
Nikolay Suvorov, Lyudmila Lyadova (Higher School of Economics)
(slides)

15:20-15:40

Coffee Break / Discussion

15:40-17:20

Application-Specific Methods and Tools (1)

15:40-16:00

Application of Machine Learning Technology to Analyze the Probability of Winning a Tender for a Project
Roman Bauer, Nikita Kultin, Danila Kultin (Peter the Great St. Petersburg Polytechnic University)
(slides)

16:00-16:20

Development of a Software for Computer-Aided Adjustment of Automatics for Elimination of Asynchronous Operation with Trapezoidal Characteristic
Dmitry Bukharov, Roman Gusev (System Operator of the United Power System), Mikhail Kondrashov (Peter The Great St. Petersburg Polytechnic University)

16:20-16:40

Creating Shoe Lasts Through 3D Feet Scans Clusterization and Building Middle Foot for Each Population
Evgeniy Pavlov, Ivan Selin, Pavel Drobintsev (Peter the Great St. Petersburg Polytechnic University)
(slides)

16:40-17:00

Analysis of Students Activity on E-learning Course Based on OpenEdu Platform Logs
Nikita Barsukov, Igor Nikiforov, Ivan Sysoev, Alina Pereskokova, Denis Posmetnijs (Peter the Great St. Petersburg Polytechnic University)
(slides)

17:00-17:20

An Approach to Semantic Search on Technical Documentation Based on Machine Learning Algorithm for Customer Request Resolution Automation
Artem Kovalev, Igor Nikiforov, Pavel Drobintsev (Peter the Great St. Petersburg Polytechnic University)
(slides)


May 29, 2020

10:00-11:20

Multiprocessing Systems and Networks

10:00-10:20

Flow Algorithm for Scheduling in Multiprocessing Heterogeneous Systems with Integrated Modular Architecture
Aleksandr Smirnov, Valery Kostenko (Moscow State University)

10:00-10:20

Implementation of Memory Subsystem of Cycle-Accurate Application-Level Simulator of the Elbrus Microprocessors
Pavel Poroshin (INEUM), Aleksey Meshkov (MCST, INEUM), Dmitriy Znamenskiy (MCST)
(slides)

10:20-10:40

Test Environment for Verification of Multi-processor Interrupt System with Virtualization Support
Dmitriy Lebedev, Vitaliy Kutsevol (MCST)
(slides)

10:40-11:00

An Approach to the Translation of Software-Defined Network Switch Flow Table into Network Processing Unit Assembly Language
Andrei Markoborodov, Yuliya Skobtsova, Dmitry Volkanov (Moscow State University)
(slides)

11:00-11:20

Tracing Network Packets in Linux Kernel using eBPF
Mark Kovalev (St. Petersburg State University)
(slides)

11:20-11:40

Coffee Break / Discussion

11:40-12:40

Software Safety and Security

11:40-12:00

Testing of Cryptographic Protocols Based on Formal Specifications
Mikhail Krichanov, Alexey Karnov, Grigoriy Volkov (ISP RAS)

12:00-12:20

Comparative Analysis of Homomorphic Encryption Algorithms Based on Learning with Errors
Mikhail Babenko, Elena Golimblevskaia, Egor Shiriaev (North-Caucasus Federal University)
(slides)

12:20-12:40

Machine Learning-Based Malicious Users Detection in Social Network vKontakte
Denis Samokhvalov (Higher School of Economics)
(slides)

12:40-14:00

Lunch

14:00-15:00

Data Storage and Processing

14:00-14:20

Hard Drives Monitoring Automation Approach for Kubernetes Container Orchestration System
Anastasia Shemyakinskaya, Igor Nikiforov (Peter the Great St. Petersburg Polytechnic University)
(slides)

14:20-14:40

Implementation of Cross-Platform Mounting Remote File Systems
Maksim Elkin, Nikita Voinov (Peter the Great Saint-Petersburg Polytechnic University)

14:40-15:00

Hardware and Software Data Processing System for Research and Scientific Purposes Based on Raspberry Pi 3 Microcomputer
Pavel Pankov, Igor Nikiforov, Dmitry Drobintsev (Peter the Great St. Petersburg Polytechnic University)
(slides)

15:00-16:20

Application-Specific Methods and Tools (2)

15:00-15:20

Application of the Non-Invasive Carbohydrate Metabolism Disorders Detection Method for Population Screening
Andrey Berezin, Roman Novikov, Maxim Novopashin, Boris Pozin, Alexander Shmid (EC Leasing)
(slides)

15:20-15:40

Development of Automated Computer Vision Methods for Medical Images Processing
Daniel Sergeev, Nikola Kukavica, Slobodanka Cenevska, Pavel Drobintsev (Peter the Great St. Petersburg Polytechnic University), Anna Drobintseva, Alexander Andreev (St. Petersburg State Pediatric Medical University)
(slides)

15:40-16:00

Hybrid Algorithm Combining Content and Collaborative Filtering Approaches for Image Recommendation
Kirill Kobyshev, Nikita Voinov (Peter the Great St. Petersburg Polytechnic University)
(slides)

16:00-16:20

Recommendation System Based on User Actions in the Social Network
Vitaly Monastyrev, Pavel Drobintsev (Peter the Great St. Petersburg Polytechnic University)
(slides)

16:20-16:40

Technological Features of Development of the Receipts and Promotions Service for the Russian National Payment Card System
Vladislav Belovitskiy (Higher School of Economics) (slides)

16:40-17:00

Coffee Break / Discussion / Closing Speech

Виртуальный стенд демонстрации результатов проекта «Исследование и разработка технологий производства и сертификации программного обеспечения с повышенными требованиями к надежности и безопасности на основе формальных методов моделирования и верификации», поддержан грантом Минобрнауки РФ RFMEFI60719X0295 (slides)