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):

Ivan Glazunov and Konstantin Dyachenko (founders of Deep Foundation): Associative data models and the legacy of the ideas of Simon Williams and Edgar Codd. Project Deep.Foundation Abstract (provided by authors): The Deep.Foundation project is an end-to-end architecture for the production of compatible IT solutions, associative storage as a metalanguage, an interface for spatial data perception, a unified information theory of everything. Day, date, and time: Thursday January 27, 2022, from 14:00 to 25:30 Moscow time (18:00-19:30 at Novosibirsk) Online in Zoom (conference ID 895 5652 6897, acces code 435770).
Special meeting in occasion of the World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) Short description: This year our seminar will continue the tradition to celebrate the World Logic Day" started a year ago. The official World Logic Day is celebrated on January 14. But the official list of events mentions events from January 11 to (mostly) January 17 and even until 23 January.
We reschedule our meeting on Friday January 21 28, 2022 in hybrid format: online (in Zoom) and offline (in Innopolis University). Those wishing to take part in our event, discuss and receive updates on the fly, we invite you to join the Telegram chat Logic Day in Innopolis .
Preliminary agenda of the meeting:
Day, date, and time: Friday January 21 28, 2022, from 18:00 to 20:30 Moscow time (22:00-24:30 at Novosibirsk) Offline - in room 321 of Innopolis University and online on Zoom (conference ID 895 5652 6897, acces code 435770).

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

Andrei V. Klimov (Keldysh Institute of Applied Mathematics RAS, Moscow, Russia): Why are partial evaluation and supercompilation still not widely used in practice? Reflections in light of Russian work on metacomputation Abstract: The problem turned out to be more difficult than the founding fathers of this scientific direction dreamed of — Valentin Turchin, Andrey Ershov and, probably, Yoshihiko Futamura and Neil Jones too. The "great program optimizer" working by pressing a button was not created. Nevertheless, approaches to the construction of metacomputation systems that are useful in practice do exist, but so far they have not been given sufficient attention. Having discarded hopes for the ease of the task, we will discuss what to do next. As a material for conclusions, we use the Russian experience of work on supercompilation and partial evaluation and only point to Western works that are most significant for us, since it is difficult to extract negative experience from papers of others, as such results are usually not published, while we know about our own work where we aspired, what happened and where we stumbled.
This presentation is a preliminary version of the talk on January 17, 2022 at PEPM'22.
Day and date: Thursdays January 13, 2022 Video on IIS Youtube Channel. ( Presentation and chat are available.)
Problems' Day In the year 2021 ruStep continues a tradition launched in the year 2020 - to have Problems' Day. Presenters: (1) Andrei Klimov (Keldysh Institute of Applied Mathematics, Moscow) Theories of the names of A. Pitts and M. Gabbai and semantics of references in programming languages, (2) Arkadiy Klimov (Institute for Design Problems in Microelectronics, Moscow) Modelling of Turing machines by Petri nets, (3) Dmitry Kondratyev (Institute of Informatics Systems, Novosibirsk) Small program which demonstrates difficulties with deductive verification automation,https://persons.iis.nsk.su/files/persons/pages/rustep30dec21fa (4) Boris Faifel (Saratov State Techical University) Calculation of Fibonacci numbers using the Binet formula without using floating arithmetic, (5) Nikolay Shilov (Innopolis University, Innopolis) How to “integrate” software engineering into math courses for programmers? Day and Date: Thursday December 30, 2021. Video on IIS Youtube Channel. (Presentations (links are in the tab left to this one) and chat are available.)
Vitaly Romanov (Innopolis University, Russia): Type Prediction in Source Code with Graph Neural Network Embeddings Abstract: Current state-of-the-art results for source code analysis with Neural Networks are achieved using famous Transformer architecture. One example of pre-trained model for source code is CodeBERT. Graph Neural Networks (GNNs) provide an alternative technique for pre-training source code embeddings. However, the strengths and weaknesses of GNN embeddings are not well studied on downstream tasks. In this work, we consider the problem of pre-training GNN embeddings for source code. We evaluate pre-trained embeddings using the task of variable type prediction for dynamically typed programming language Python. Our experiments show that GNN embeddings pre-trained with Name Prediction objective achieve performance comparable to CodeBERT embeddings. Moreover, combining CodeBERT and GNN embeddings into a Hybrid Type Prediction model allows to further improve type prediction accuracy by more than 10%. These improvements are achieved just after training GNN embeddings for one epoch – a fraction of time that is needed to pre-train CodeBERT embeddings. Day and date: Thursdays December 23, 2021 Video on IIS Youtube Channel. (Presentation is available.)
Vladislav Perepelkin (Institute of Computational Mathematics and Mathematical Geophysics SB RAS, Novosibirsk, Russia): Language and System LuNA for Automatic Construction of Numerical Distributed Programs Abstract: System LuNA is capable of automatic construction and execution of numerical distributed programs. As input the system takes a high-level specification of a parallel program to construct in LuNA language. LuNA-program is a description of a set of data and computational fragments, which allows the system to automatically schedule and perform computations in distributed environments, dynamically balance workload over computing nodes, perform necessary communications and take care of a number of other low-level parallel programming tasks. The programmer, thus, does not have to care about that himself. In the talk LuNA language is presented, as well as key system algorithms to translate and execute LuNA programs. The system LuNA, and its performance investigations are introduced. Day and date: Thursdays December 16, 2021 Video on IIS Youtube Channel. ( Presentation and chat are available.)
Alexander Kogtenkov ( Schaffhausen Institute of Technology, Switzerland): A sound formalization of void safety Abstract: One of the principal source of program crashes and security attacks is the null-pointer (or void-reference) dereferencing, which results from an attempt to use a non-existing object. Mainstream languages, object-oriented or not, are subject to this risk. A number of languages, most notably Eiffel, pioneered "void-safety", which provides a guarantee that no such events will occur. Formal proofs are required, however, to guarantee the soundness of such schemes. This talk examines one of the published approaches, "Freedom before commitment" by Summers and Müller, shows through a formalization in Isabelle/HOL that it contains errors, and corrects them.  Day and date: Thursdays December 2, 2021 Video on IIS Youtube Channel. (Presentation is available.)
Swati Megha (Innopolis University, Russia): Design Patterns Detection Using Machine Learning Model Abstract: Design patterns are used to address common design problems in software systems. Several Machine learning models have been proposed for detecting and recommending design patterns for a software system. However, lesser research is done on using Machine learning models for establishing a correlation between design patterns and code quality. In this paper, firstly, we created a data set of 378 open-source software projects primarily from GitHub and GitLab to train models. Secondly, we compared several pattern detection machine learning models based on the most popular classifier families for three categories of design patterns, namely Creational, Structural, and Behavioral. We then compared five standard performance matrix namely, Precision, Recall, Accuracy, and FI-Score for eight different classifier families. The proposed model showed noticeable improvement in Precision and Accuracy, while the identified improvements in Recall and FI-Score were moderate.  Day and date: Thursdays November 25, 2021 Video on IIS Youtube Channel. (Presentation is available.)
XII Workshop on Program Semantics, Specification, and Verification
List of invited talks:
  • Alexander K. Petrenko: The position of formal methods in nowadays software industrial development
  • Victor V. Kuliamin: Formal Security Models
  • Alexander S. Kamkin: High-Level Synthesis of Computing Systems: Motivation, Challenges, and Existing Solutions
  • Alexey V. Khoroshilov: Verification of operating systems
  • Nikolai D. Kudasov: Nameless and scope-safe (de Bruijn notation as a nested datatype)ms: Sound, Expressive, Fast
  • Alexandr V. Naumchev: Security audit of code using contracts and program proving
  • Nataliya O. Garanina: The Optimization Problem with Model Checking
  • Dmitry A. Kondratyev: Automatic deductive verification of C programs using the C-lightVer system
Summary: PSSV workshop series was launched in 2010 by Valery A. Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia) and Valery A. Sokolov (Yaroslavl State University, Russia).
In year 2021 the Workshop was hosted (virtually) by Software and Service Engineering Laboratory of Innopolis University and was held November 4-5 online (via Zoom).
Days and dates: Thursdays November 4 and Friday November 5, 2021 Actual Programme of PSSV-2021 (with links to abstracts and recordings of the talks) is available here.
Rene van Bevern (Novosibirsk State University): Randomized Algorithms. How to live with the likelihood of error. The meeting was organized under the auspices of the Computer Science Center.
Abstract: In Computer Science, methods of probability theory are found in various forms. In the lecture, we saw why randomness can be used in algorithm design, that randomized algorithms are often simple, sometimes even extremely simple. On the other hand, we saw that the simplicity of these algorithms is often due to their non-trivial analysis: more complex algorithms would be too difficult to analyze.
Day and date: Thursdays October 21, 2021 https://youtu.be/9v5npQUXhyU"> Video on Youtube Channel of the Computer Science Center.
Nikolay V. Shilov (Innopolis University): Experimenting with Alias Calculi for a Simple Imperative Language with Decidable Pointer Arithmetic Abstract: Alias calculus was proposed by Bertrand Meyer in 2011 for a model programming language with a single data type for abstract pointers. This original calculus is a set-based formalism presented as a set of syntax-driven rules how to compute an upper approximation aft(S, P) for aliasing after the execution of a program P for a given initial aliasing S. In 2014 by N. Shilov, A. Satekbayeva, and A. Vorontsov suggested an alias calculus for a more realistic (but still a model) procedural programming language MoRe that has addressable memory. In the present talk we will report an implementation of an aliasing analysis prototype tool for MoRe. The tool is based on a new light version of the alias calculus designed for memory leak analysis. It had been tested using a number of short snippets of MoRe code that contain various memory leak bugs and has demonstrated its correctness (by finding these bugs).
This is a joint work with Leonid I. Lygin.
Day and date: Thursdays October 7, 2021 Video on IIS Youtube Channel. (Presentation is available.)
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. Days and dates: Thursdays September 23 and 30, 2021 The first part - Thursday September 23 (video on IIS Youtube Channel), the second part - Thursday September 30, 2021 (video on IIS Youtube Channel). (Presentation is available.)
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.