ru-STEP - English version

 

Russian online seminar on
fundamental issues of software engineering, theory and experimental programming:
ru-STEP = russian seminar on Software Engineering, Theory and Experimental Programming

(Seminar' test web-page in English, please proceed to the web-page in Russian in need.)

Steering Committee:

  • Igor Anureev (Institute of Informatics Systems - Novosibirsk, anureev "at" iis.nsk.su)
  • Dmitry Kondratyev (Institute of Informatics Systems - Novosibirsk, apple-66 "at" mail.ru)
  • Aleksandr Naumchev (Innopolis University - Innopolis, a.naumchev "at" innopolis.ru)
  • Denis Ponomaryov (Institute of Informatics Systems and Novosibirsk State University - Novosibirsk, ponom "at" iis.nsk.su)
  • Alexei Promsky (Institute of Informatics Systems - Novosibirsk, promsky "at" iis.nsk.su)
  • Andrey Sadovykh (Innopolis University - Innopolis, a.sadovykh "at" innopolis.ru)
  • Nikolay Shilov (Innopolis University - Innopolis, shiloviis "at" mail.ru)

Seminar Description:

How to participate, discuss, and/or suggest a talk:

  • Volunteers to give a talk are invited to write by e-mail to any/several/all member(s) of the Steering Committee (with the subject line "ru-STEP talk proposal").
  • Those who wish to receive a reminder (notification) about the next meeting on the eve of the seminar (topic, speaker, technical environment, date and time) can fill-in Google-form at https://forms.gle/earZy3hFJKmHQLoZ7.
  • Participants of the seminar are welcome to join our special discussion (Google-) group to discuss issues related to the seminar, past talks, etc.

Upcoming Seminar(s):

Dmitry A. Kondratyev (Institute of Informatics Systems, Novosibirsk): Automated error localization for C programs using deductive verification Abstract: The C-lightVer system is developed in A.P. Ershov Institute of Informatics Systems SB RAS. It is a system of C-program automatic deductive verification. The task of deductive verification automation includes error localization problem. Classical deductive verification results to unproven or false verification conditions in the case of input program with errors. Verification system user needs in detailed explanations of unproven or false verification conditions. Significant modification of semantic labeling method is implemented in the C-lightVer system to solve this challenge. Original method is based on supplementing verification condition subformulas with semantic labels. Semantic label stores information about correspondence between verification condition subformula and source code of input program. This information is converted into text written in natural language. Explanation of verification condition is resulted from union of texts generated for each semantic label. Semantic labeling method extension implemented in the C-lightVer system allows using not only standard kinds of semantic labels but also user-defined kinds of semantic labels. Another extension allows generating detailed explanations in the case of input programs with such loops as definite iterations over data structures. Symbolic method of verification of definite iterations allows us to avoid defining invariants in the case of such loops. This method is based on symbolic replacement of definite iterations by special recursive functions. But obtained verification conditions contain applications of these recursive functions. Semantic labeling method extension allows supplementing definitions of these functions with special semantic labels. Obtained explanation contains text about correspondence between definite iteration and definition of these functions. Day, date, and time: Thursday September 23, 2021, 14:00-15:40 Moscow /18:00-19:40 Novosibirsk Join us on Zoom using link (id 895 5652 6897, pass 435770).

Past meetings (Last-In - First-Out):

Anton A. Zavyalov (Novosibirsk State University): Designing a visual functional language with recursion optimization capabilities Abstract: The talk is about the design and development of an integrated programming environment in a visual functional language with the ability to optimize recursion. Features discussed: (i) design of a visual functional programming language, (ii) developing an integrated visual programming environment using a previously designed language, (iii) designing and developing an optimizing compiler for programs in a previously designed language with a translator into JavaScript code as the target platform. Day and date: Thursday September 9, 2021. Video on IIS Youtube Channel. (Presentation and chat log are available.)
Antonina Nepeivoda (The Program Systems Institute, Pereslavl Zaleskii, Russia): Experiments with Supercompilation on Refal Abstract: This presentation continues the talk by Alexander V. Konovalov on the Refal language at the ruSTEP seminar on June 11, 2021. The supercompilation method as applied to this language will be briefly considered. On the one hand, the associativity of Refal's built-in data complicates the development of algorithms for analyzing his programs, on the other hand, it makes it possible to prove properties naturally derived from programs written in Refal, and to flexibly describe the models of structures that have associativity. In particular, we show how some algorithms for solving equations in words are modeled by supercompilation methods. Day and date: Friday July 9, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Joseph Alexander Brown (Head of the Lab of Artificial Intelligence in Game Development, Innopolis University, Russia): Affordance Theory in Game Design - A Guide Toward Understanding Players A monograph Affordance Theory in Game Design. A Guide Toward Understanding Players by Hamna Aslam (Innopolis University) and Joseph Alexander Brown was published in 2020 by Morgan & Claypool Publishers.
Abstract: Games, whether educational or recreational, are meant to be fun. How do we ensure that the game delivers its intent?
The answer to this question is playtesting. However, a haphazard playtest process cannot discover play experience from various dimensions. Players' perceptions, affordances, age, gender, culture, and many more human factors influence play experience. A playtest requires an intensive experimental process and scientific protocols to ensure that the outcomes seen are reliable for the designer.
Playtesting and players' affordances are the focus of this book. This book is not just about the playtest procedures but also demonstrates how they lead to the conclusions obtained when considering data sets. The playtest process or playtest stories differ according to the hypothesis under investigation. We cover examples of playtesting to identify the impact of human factors, such as age and gender, to examine a player's preferences for game objects' design and colors. The book details topics to reflect on possible emotional outcomes of the player at the early stages of game design as well as the methodology for presenting questions to players in such a way as to elicit authentic feedback.
This book is intended mainly for game designers, researchers, and developers. However, it provides a general understanding of affordances and human factors that can be informative for readers working in any domain.
Please follow the links for the table of contents and authors' information.
Day and date: Friday June 25, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Alexander V. Konovalov (Bauman Moscow State Technical University): Introduction to the Refal programming language Abstract: The primary goals of the introductory talk are to sketch Refal programming language history, syntax, semantics and to prepare the audience to talks (expected in July-August) on the features of Refal's supercompilation.. Day and date: Friday June 11, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Discussion comments on the talk by Andrey V Klimov. - Please join and write your comments to our special discussion (Google-) group.
XI SYRCoSE invited (plenary) talks:
  • Dmitry A. Mordvinov (SPbSU, JetBrains Research, Russia): Property Directed Symbolic Execution
  • Anton V. Podkopaev (High School of Economics, JetBrains Research, Russia): Programming Language Memory Models: Problems, Solutions, and Directions
  • Holger Schlingloff (Fraunhofer FOKUS, Germany): Formal Methods for Reliable Autonomous Systems
Summary: SYRCoSE (Spring/Summer Young Researchers' Colloquium on Software Engineering) was launched in 2007 by Alexander K. Petrenko (Institute for System Programming of RAS, Russia) and Andrey N. Terekhov (Saint-Petersburg State University, Russia).
In year 2021 the Colloquium was hosted by HSE University and was held May 27-28 in a hybrid format at HSE University at Pokrovsky Bulvar and on Zoom.
Please read the abstracts of the invited talks.
Days and dates:
  • Dmitry A. Mordvinov - Thursday May 27, 2021
  • Anton V. Podkopaev - Friday May 28, 2021
  • Holger Schlingloff - Friday May 28, 2021
Reordings of the both days of SYRCoSE-2021 are provided by Ivannikov Institute for System Programming of the RAS and can be found in the following repositories:
Artem S. Burmyakov (Innopolis University): The Introduction to the Consensus Problem and Its Application to the Development of Non-Blocking Concurrent Algorithms Abstract: Consensus problem is a fundamental theoretical problem for distributed and concurrent programming. The problem has an enormous influence on various application areas, such as the development of non-blocking concurrent algorithms, blockchain systems, clock synchronization algorithms in distributed systems, and concurrent systems with failures. The talk introduces the consensus problem and discuss the available solutions. In particular, it demonstrates the application of the consensus problem to compare the synchronization power of various concurrent data structures (e.g. a FIFO queue) and CPU synchronization primitives for the development of concurrent non-blocking algorithms, by means of "consensus numbers". Day and date: Friday May 14, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Dmitry V. Koznov (Sankt Petersburg State University and JetBrains): Visual modeling in the development of a family of telecommunication systems Abstract: Visual modeling (model-based approach) has been a subject of intense research and interest from the industry for many years. The peak of popularity of the approach was the Unified Modelling Language. However, the enthusiasm has cooled down due to the lack of tangible, meaningful practical results.
The talk puts forward the following thesis: visual modeling can be successful, firstly, within the framework of a domain-specific approach, secondly, with seamless integration with development tools (IDEs), and thirdly, when used in the development of families of systems ...
The talk presents a pilot domain-specific solution for a hardware-software family of telecommunication systems aimed at automating the development of drivers for hardware and created on the basis of a model-based Eclipse technology stack.
Day and date: Friday April 30, 2021. Video on IIS Youtube Channel.
Andrey M. Raygorodsky (Moscow Institute of Physics and Technology, Yandex): Actual Problems of Graph Theory Summary: The lecture was the second event of the Annual Ershov Memorial Lecture Series. The series was launched in 2007 by Andrey Baehrs to commemorate Academician Andrey Ershov contribution to Computer Science, Theory of Programming, and Software Engineering.
In 2021 A.P. Ershov Institute of Informatics Systems hosted 2 Ershov Lectures. The second lecture was given by Andrey M. Raygorodsky. (More information in Russian at XVI Ершовская лекция по информатике.)
Day and date: Friday April 23, 2021. Video in the playlist of Annual Ershov Memorial Lecture Series.
Viktor N. Kasyanov (Institute of Informatics Systems, Novosibirsk): Academician Andrey P. Ershov and graphs in programming Summary: The lecture was the first event of the Annual Ershov Memorial Lecture Series. The series was launched in 2007 by Andrey Baehrs to commemorate Academician Andrey Ershov contribution to Computer Science, Theory of Programming, and Software Engineering.
In 2021 A.P. Ershov Institute of Informatics Systems hosted 2 Ershov Lectures. The first lecture was given by Viktor N. Kasyanov. (More information in Russian at XV Ершовская лекция по информатике.)
Day and date: Friday April 16, 2021. Video on the playlist of Annual Ershov Memorial Lecture Series.
The first VeriDevOps Open Research Workshop "Meet Security Requirements in DevOps Environments" Summary: VeriDevOps is an European project that aims at providing a faster feedback loop for verifying security requirements i.e. confidentiality, integrity, availability, authentication, authorization and other functional and extra-functional attributes of large scale DevOps environments in industrial systems.
VeriDevOps project has just finished the state of the art review stage on methods for addressing software security vulnerabilities starting from requirements to verification and testing at development and reactive protection at runtime. We would like to briefly share our findings and start a dialogue with you on possible collaboration at this open research workshop.
Based on this workshop we plan to publish a set of lecture notes with Springer, we would love to invite prospective authors from this area.
Day and date: Friday April 16, 2021. Video on Youtube Channel of Andrey Sadovykh.
Andrey Sadovykh (Innopolis University): Hackathons in Software Engineering education. Experience report. Abstract: When teaching software development, we face several problems: (1) many students lack the experience to understand the importance of theoretical material in practical application, which leads to a lack of motivation and low involvement; (2) educators and researchers need regular contact with the industry, which is difficult to implement in the framework of classical courses; (3) companies have difficult access to research results in the field of software development, as well as the ability to convey to teachers and students the pressing development problems. We offer educational hackathons as a way to improve the educational and research process through short but intense meetings where companies, researchers and students work together to solve small problems from the industry. In the report, we discuss one of the hackathon recipes, summarize the feedback from the participants and discuss the development of this idea. Day and date: Friday April 2, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Alexander Semenov (Institute for System Dynamics and Control Theory, Irkutsk): Using SAT solvers to invert discrete functions (with application to cryptanalysis) Abstract: In the talk, a short review of the recent achievements in algebraic cryptanalysis, and concretely, in SAT-based cryptanalysis, was presented. In SAT-based cryptanalysis, the state-of-the-art SAT solvers are used to solve the system of algebraic equations that specifies the considered cipher. In the first part of the talk, we discussed the main techniques of translation of algorithms specifying discrete functions to SAT. In the second part, we gave the precise notion of SAT-immunity of an arbitrary discrete function and use this notion to demonstrate how one can reduce the problem of constructing a guess-and-determine attack on a considered cipher to the problem of pseudo-Boolean optimization. Also, we presented the results of a number of computational experiments. Day and date: Friday March 19, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Lidiya Gorodnyaya (Institute of Informatics Systems, Novosibirsk): Do not offend girls and women! The talk was a key part of "a generalized March 8" event (joint with the Mathematical Club of the Innopolis University).
Abstract of the talk: The talk is mainly based on factography around the term von Neumann architecture, the conflict over the patent for the ENIAC design, the peculiarities of anniversary events and the history of computers in Russia. In addition to the documents themselves, some strokes are the author's reconstruction based on understanding the mechanisms of behavior.
The talk will be followed by an open discussion. Highly recommended to watch in advance movies The Gifted and Hidden Figures.
Day and date: Monday March 8, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Alex Dekhtyar (California Polytechnic State University, San Luis Obispo): In-concert teaching for Software Engineering For All courses Abstract: Today, teaching software engineering principles in higher education is reserved to students pursuing computational degrees (i.e., degrees in fields like Computer Science, Software Engineering, Computer Engineering, Information Systems). At the same time, these days, the barrier to entry into the world of software development as a stakeholder, subject matter expert, user, quality assurance specialist, or product manager for professionals with non-computing education is getting lower and lower. As such, software developers interact with many non-software developers as part of their work on software products. But in a given software development process, typically only the software developers were educated on what the software development lifecycle is. In this talk we discuss our preliminary effort to rectify this issue, by developing and teaching an undergraduate course "Software Engineering Without Programming" directed at the students pursuing non-computing degrees. To teach this course in line with Cal Poly's "learn by doing" motto we have partnered with an Introduction to Software Engineering course for Cal Poly''s Software Engineering majors in an approach called "in-concert teaching" - a teaching technique where two courses in related topics are taught to two separate student bodies, who are then brought together for joint laboratory assignments and projects. For the "SE without Programming" course, the ability of students to communicate directly with software developers and work on a joint project provided a clear benefit. In the talk we will discuss the in-concert teaching approach, its application to teaching the "SE without Programming" course, and the lessons learned.
The talk is based o a joint work with Bruno da Silva (Cal Poly, CSSE), Anya Goodman (Cal Poly, Chemistry).
Day and date: Friday March 5, 2021. Video on IIS Youtube Channel.
Sergey M. Staroletov (Altai State Technical University): Model checking games and a genome sequence search Abstract: The presentation considers a concept of model checking games to solve algorithmic puzzles. I described current approaches in this field and move to a game between a user and a software model checker with the goal to provide a solution to a problem, encoded in a transition system and an LTL formula with a requirement. I shown how to encode and solve some problems using this approach. Then I moved to the problem of searching a pattern in a genome sequence. I discussed implementation of the Z-function search method in Promela, construction of the model, provided the input of real viral data, and then played a model checking game with SPIN verifier. Based on experiments, I discussed that the problem to find a pattern with some deviations is only solvable using the swarm verification and hash compact method. Day and date: Friday February 19, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Nikolay V. Shilov (Innopolis University): Recursion elimination in Dynamic Programming Abstract: Transformation-based program verification was a very important topic in early years of theory of programming. Great computer scientists contributed to these studies: John McCarthy, Amir Pnueli, Donald Knuth ... Many fascinating examples were examined and resulted in recursion elimination techniques known as tail-recursion and co-recursion. In the talk we examine several (new) examples of recursion elimination via program manipulations and problem analysis. Day and date: Friday February 5, 2021. Video on IIS Youtube Channel. (Presentation is available.)
Meeting in occasion of the World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) The session was a joint event with the Mathematical Club of the Innopolis University. Presenters and titles: (1) Zakhar Yagudin (Undergraduate student of Innopolis University) - "0-1 Laws for Graphs and Logics", (2) Dmitry Kondratyev (Institute of Informatics Systems) - "ACL2 proof that sqrt(2) is not a (rational) number", (3) Boris Faifel (State Technical University of Saratov) - "How to program logic puzzles in imperative languages", (4) Andrei Klimov (Keldysh Institute of Applied Mathematics) - "Using supercompilation for extracting efficient solutions for N-Queen Puzzle". Day and date: Friday January 15, 2021. Video on IIS Youtube Channel.
Problems' Day Presenters: (1) Dmitry Kondratyev (Institute of Informatics Systems, Novosibirsk), (2) Andrei Klimov (Keldysh Institute of Applied Mathematics, Moscow), (3) Arkadiy Klimov (Institute for Design Problems in Microelectronics, Moscow), (4) Nikolay Shilov (Innopolis University, Innopolis), (5) Lidia Gorodnyaya (Institute of Informatics Systems, Novosibirsk). Day and Date: Wednesday December 30, 2020.
Bertrand Meyer (Politecnico di Milano, Innopolis University, and Eiffel Software): The four PEGS of requirements engineering Abstract: Bad software requirements can jeopardize projects., but requirements as commonly practiced remain a weak link in software engineering. What passes for requirements in industry usually consists of a few use cases or user stories, which fail to capture many essential aspects of systems. There is a considerable literature on requirements, including some excellent textbooks, but their lessons are rarely heeded; many projects, in particular, fail to take into account the Jackson-Zave distinction between system and environment. The standard IEEE plan for requirements dates back to 1998 and does not meet the demands of today’s ambitious developments. I will present ongoing work intended to help industry produce more useful requirements. It includes precise definitions of requirements concepts and a standard plan for requirements specifications. The plan contains four books covering the four “PEGS” of requirements engineering: Project, Environment, Goals and System. The talk does not attempt to introduce radical new concepts but rather builds on existing knowledge to define a solid basis for requirements engineering and provide projects with precise and helpful guidelines. Day and Date: Wednesday December 16, 2020
Stanislav Kikot (London Metropolitan University): Graduate Programs in Computer Science in Great Britain. Day and Date: Wednesday December 2, 2020
Dmitry Kondratyev (Institute of Informatics Systems, Novosibirsk): Methods and tools for formal verification of Cloud Sisal programs. Abstract: A cloud-based parallel programming system (CPPS) is being developed at IIS. The CPPS input language is Cloud Sisal. It is a functional programming language based on looping expressions. The main feature of CPPS is implicit parallelism, which is achieved through the vectorization of looped expressions. The CPPS includes the CSV1 and CSV2 subsystems for deductive verification of Cloud Sisal programs. Consider the similarities between both subsystems: first, the input argument to both subsystems is a Cloud Sisal program annotated in the ACL2 language; second, in order to avoid specifying loop invariants in both subsystems, a symbolic method of verifying finite iterations is used. This method is based on replacing the loop action with a recursive function. Remark that in both subsystems the ACL2 system is used to prove correctness conditions. Let's consider the main difference between both subsystems. The CSV1 subsystem is based on the translation of Cloud Sisal programs into C programs. A deductive verification system (C-lightVer, previously developed at IIS) is applied to the translation result.Therefore, the symbolic method for verifying finite iterations is applied to C loops obtained as a result of the translation of Cloud Sisal loops. The ACL2 system is used to prove the correctness conditions for the received C programs. Unlike the CSV1 subsystem, the CSV2 subsystem is based on deductive verification of the original Cloud Sisal programs. Therefore, the symbolic method for verifying finite iterations is applied to Cloud Sisal cycles. The ACL2 system is used to prove the conditions of correctness of the original Cloud Sisal programs. Days and Dates: the first part - Wednesday November 18, the second part - Wednesday November 25, 2020.
Aleksandr Naumchev (Innopolis University): Seamless Requirements and specifications. Day and Date: Wednesday October 28, 2020.
Natalia Garanina (Institute of Informatics Systems, Novosibirsk): An Ontology-based Approach to Support Formal Verification of Concurrent Systems. Abstract: Formal verification ensures the absence of design errors in a system with respect to system's requirements. This is especially important for the control software of critical systems, ranging from automatic components of avionics and spacecrafts to modules of distributed banking transactions. We present a verification support framework that enables automatic extraction of a concurrent system's requirements from the technical documentation and formal verification of the system design using an external or built-in verification tool that checks whether the system meets the extracted requirements. Our support approach also provides visualization and editing options for both the system model and requirements. The key data components of our framework are ontological descriptions of the verified system and its requirements. We describe the methods used in our support framework and we illustrate their work for the use case of an automatic control system. Day and Date: Wednesday October 21, 2020.