 |
ru-STEP - English version |
|
|
Archive of Russian hybrid seminar ru-STEP (21.10.2020-08.02.2023)
|
| Nikolay V. Shilov (Innopolis University): Introduction to substractural logics (in the footsteps of the Day of Logic 2023) | Abstract: In my short talk Overview of World Logic Day 2023 events that I could attend (online) given for the seminar' meeting on occasion "Logic Day 2023" I briefly touched a talk Paradox and Substructurality given by Elia Zardini for Formal Philosophy Seminar on January 13, 2023. Because of an interest of the audience of ruSTEP to understand substructoral logics better, I would like to introduce these logics with more details in my forthcoming talk. | Day and date: Wednesday February 1, 2023 | Video on IIS YouTube Channel. ( Presentation is available.) |
| Special meeting in occasion of the World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) |
Short description: In the year 2023 our seminar will continue the tradition to celebrate the World Logic Day "Logic Day 2021" and "Logic Day 2020".
The session was a joint event with
the Mathematical Club of the Innopolis University with a separate
Telegram chat Logic Day in Innopolis .
Agenda of the meeting (with references to some materials):
|
Day and date: Friday January 20, 2023 | (Links to some materials are in the tab left to this one.) |
| Problems' Day | Problems' Day continue a tradition of "Problems Day 2020" and "Problems Day 2021". Presenters: (1) Arkadiy Klimov (Institute for Design Problems in Microelectronics, Moscow) A subclass of Petri nets that allows simple distributed execution, (2) Dmitry Kondratyev (Institute of Informatics Systems, Novosibirsk) Program specification paradigms and the SpecifyThis contest, (3) Nikolay Shilov (Innopolis University, Innopolis) Finally, what is the complexity of Dijkstra's assignment algorithm? | Day and Date: Friday December 30, 2022. | Video on IIS Youtube Channel. (Presentations (links are in the tab left to this one) are available.) |
| Yury A. Kochetov (Institute of Mathematics, Siberian Division of RAS, Novosibirsk): The packing problems for two dimensional rectangular items | Abstract: We consider the well-known strip packing and bin packing problems for two dimensional rectangular items with and without rotations by 90 degrees. We present some mixed integer mathematical models, solution coding schemes and decoding procedures. Simulated Annealing metaheuristic based on the so-called Sky-line procedure and Oriented Trees coding scheme will be demonstrated on small test instances with at most 100 rectangles. | Day and date: Friday December 16, 2022 | Video on IIS YouTube Channel. ( Presentation is available.) |
| Date of the meeting of ruSTEP intersected with dates of Open Conference of the Institute of System Programming RAS. | One of five sections of the conference was Program analysis, modeling and transformation technologies, it was about "optimization methods in compiler and code generation, static and dynamic program analysis, etc." Programme (in Russian) of the conference (including the section Programme) is available here. | Day and date: Friday December 2, 2022 | Video of section on ISP YouTube Channel. |
| Sergey M. Staroletov (Altai State Technical University): Towards Modeling and Verification of Eurobalise Telegram Encoding Algorithm | The talk presented a recent paper published by presenter in Transportation Research Procedia (v. 61, 2022, pp. 447-454, https://doi.org/10.1016/j.trpro.2022.01.073).
Paper abstract: A eurobalise is designed to broadcast the current state of the railway to a passing train. Such a transmitter is activated with an approaching train and its goal is to dispatch messages called telegrams. In this article, we consider the encoding process of such telegrams. Since the CRC checksum building method is based on operations with polynomials over the Galois field modulo 2, we describe a proven library to work with polynomials. Next, we present the implementation of the encoder in a modeling language according to the open specification and then discuss its verification strategies using the Model Checking method. |
Day and date: Friday November 18, 2022 | Video on IIS YouTube Channel. ( Presentation is available.) |
| Dmitry A. Kondratyev (Institute of System Informatics, Novosibirsk, Russia): Automation of C Program Deductive Verification without Using Loop Invariants | On the first week of November 2020 and 2021 our seminar served as a platform for the annual PSSV - Workshop Program Semantics, Specification and Verification (Theory and Applications) - PSSV-2021 and PSSV-2020. However, this year the organizers of the PSSV decided to refrain from holding a seminar.
However, this year, on November 4, instead of the PSSV meetings, we held a regular ruSTEP meeting, but a special one - dedicated to the memory of one of the founders of the PSSV, Valery A. Nepomniaschy (August 7, 1939 - December 25, 2021). ruSTEP meeting on November 4, 2022 consisted of two parts: firstly, D.A. Kondratiev will present Valery A. Nepomniaschy's latest published work "Automation of deductive verification of C-programs without the use of loop invariants" (joint research with D.A. Kondratyev), followed by a memorial session. (Recall that in 2019 Colloquium on Theoretical and Experimental Programming dedicated to the anniversary of Valery A. Nepomniaschy (Col-TEP-2019) was held at the ISI SB RAS.) Abstract of Dmitry A. Kondratyev's talk: Automation of C program verification is an important problem in modern software development. To solve this problem, the solution of the following problems must be automated: loop invariants, proof of verification conditions, and localization of errors in the case of invalid verification conditions. To this end, the C-lightVer system is under development in the Ershov Institute of Informatics Systems of the Siberian Branch of the Russian Academy of Sciences. This system uses an integrated approach to the automated deductive verification of C programs. This approach includes a symbolic method of verification of definite iterations for eliminating loop invariants, strategies for proving verification conditions, and a method for error localization. The symbolic method of verification of definite iterations is based on replacing the action of certain loops by the application of a special recursive function rep. The error localization method is based on matching the verification conditions to the source code and on generation of a report about the correspondence between the verification conditions and program fragments. Thus, the problem of automation of verification of C programs containing nested loops naturally arises. The application of the symbolic method of verification of definite iterations for such programs leads to a composition of the functions rep for outer and inner loops. A novel result presented in this talk is a strategy of automation of proof of verification conditions for such programs. This strategy is based on induction on the index of iteration in the outer loop. To prove the induction step, another result presented in this talk is used. This is a strategy for programs the specification of which contains functions with the concatenation property. The talk also presents strategies of error localization and modifications of the error localization method for the case of nested loops. These strategies are also used for verifying the loop properties that may indicate the presence of errors. As an example of applying the results presented in this talk, automatic verification of insertion sort without loop invariants is considered. Refernce: Kondratyev D.A., Nepomniaschy V.A. Automation of C Program Deductive Verification without Using Loop Invariants. Programming and Computer Software. 2022. Volume 48. Issue 5. pp. 331-346. DOI: (https://doi.org/10.1134/S036176882205005X). |
Day and date: Friday November 4, 2022 | Video on IIS Youtube Channel. ( Presentation by D.A. Kondratyev, a short memorial presentation by N.V. Shilov, and photos of V.A. Nepomniaschy on PSSV-2018 (courtesy by Vladimir Sazonov and Mark Trakhtenbrot) и and on conference PSI-2011 (courtesy by Mark Trakhtenbrot) are available also.) |
| Nikolay V. Shilov (Innopolis University, Russia): Review of Matching Logic | Abstract: It was a review of the paper Matching logic by Grigore Rosu (Logical Methods in Computer Science, Volume 13, pp 1-61, December 2017, available here). The review may be considered as complimentary to ruSTEP talk Formal Operational Semantics in Practice (K-framework Applications in Industry) by Vasil Dyadov on June 23, 2022.
Abstract of the paper: This paper presents ''matching logic'', a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the ''patterns'', are constructed using ''variables'', ''symbols'', ''connectives'' and ''quantifiers'', but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that ''match'' it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, modal logic, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning with equality remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have an operational semantics, but it is not limited to this. |
Day and date: Fridays October 21&28 and Tuesday November 1, 2022 | Videos on IIS Youtube Channel: part 1, part 2,and part 3. ( Presentation is available.) |
| Sirojiddin Komolov (Innopolis University, Russia): The state of the contemporary science in Uzbekistan | Sirojiddin Komolov is a Senior Instructor at Innopolis University. Recently he (with Sherzod Rakhmatov) published in Uzbekistan a monographic textbook Fundamentals of artificial intelligence. Machine learning. | Day and date: Friday October 7, 2022 | Video on IIS Youtube Channel. ( Presentation is available.) |
| Vladimir V. Ivanov (Innopolis University, Russia): Complexity analysis of Russian text | Abstract: Automatic evaluation of the complexity of texts is in demand in education and a number of other areas. Solving this problem should improve the quality of educational materials (especially for the personalized learning). However, it remains unresolved even for the English language, although it has attracted the attention of many researchers. The talk will consider general approaches, complexity models for Russian texts (based on a small number of low-level parameters), as well as neural networks. With regard to the Russian language, all of the above tasks have not yet been studied in deep. | Day and date: Thursdays September 22, 2022 | Videos on IIS Youtube Channel: part 1, part 2,and part 3 (with discussion). ( Presentation is available.) |
| Julio Cesar Carrasquel (Higher School of Economics, Moscow, Russia): Formal Modeling and Validation of Stock Trading Systems Behavior: A Petri Net Approach | Abstract: The talk presentув Ph.D. Thesis with oral defense scheduled on September 16, 2022. Thesis accumulates a study on the formal modeling of processes in trading systems using different extensions of Petri nets — a well-known formalism for modeling and analysis of concurrent distributed systems. Novel methods to validate the real behavior of trading systems by comparing models of Petri net extensions using event data from these systems are also presented. In this dissertation summary, we first introduce what are trading systems and how process mining, a data science discipline that focuses on the analysis of processes, can be used to validate these systems. Also, we introduce and motivate our choice to employ Petri nets and conformance checking, a kind of process mining techniques, as the specific approaches for modeling and validation of processes in trading systems. Afterwards, we define the research problem, the main research contributions, and finally we outline the structure of this thesis. | Day and date: Thursdays September 8, 2022 | Videos on IIS Youtube Channel: part 1 and part 2. ( Presentation is available.) |
| Nikolai D. Kudasov (Innopolis University, Russia): Higher-order unification from E-unification with second-order equations and parametrised metavariables | Abstract: Type checking and, to a larger extent, type and term inference in programming languages and proof assistants can be implemented by means of unification. In presence of dependent types, variations of higher-order unification are often used, such as higher-order pattern unification. In practice, there are often several mechanisms for abstraction and application, as well as other eliminators (such as projections from pairs) that have to be accounted for in the implementation of higher-order unification for a particular language. In this work, we study the possibility of representing various higher-order unification problems as a special case of E-unification for second-order algebra of terms. This allows us to present beta-reduction rules for various application terms, and some other eliminators as equations, and reformulate higher-order unification problems as E-unification problems with second-order equations. We then present a procedure for deciding such problems, introducing second-order mutate rule (inspired by one-sided paramodulation) and generic versions of imitate and project rules. We also provide a prototype Haskell implementation for syntax-generic higher-order unification based on these ideas in Haskell programming language. | Day and date: Thursdays June 30, 2022 | Videos on IIS Youtube Channel: part 1, part 2, part 3, and part 4. ( Presentation is available.) |
| Vasil Dyadov (Kaspersky Lab, Russia): Formal Operational Semantics in Practice (K-framework Applications in Industry) | Abstract: K-framework is a modern approach to programming language design, program analysis and verification. It allows to define an operational semantics of programming language in simple and intuitive way, and get a bunch of tools automatically: from interpreters to symbolic-execution engines and provers. One can define his own language in literally 15 minutes and start to program in this language, experiment, test, prove properties of programs in this language and so on. Currently K-framework is more and more widely used in industry: from block-chains to NASA aerospace programs. And it was proven by practice to be very effective tool for program verification, safety and security analysis. Also K-framework is very helpful in computer science courses that are aimed at language design and formal semantics. | Day and date: Thursdays June 23, 2022 | Video on IIS Youtube Channel. ( Presentation and chat are available.) |
| Artem S. Androsov and Sergey P. Shary (Novosibirsk State University): IntvalPy - a Python interval computation library | Abstract: The talk presents the IntvalPy library that implements interval computations in Python. Unlike other existing interval libraries, IntvalPy provides the ability to work with both classical interval arithmetic and complete Kaucher interval arithmetic. In addition, the library was developed taking into account the IEEE 1788-2015 standard for interval arithmetic on digital computers, which guarantees high accuracy of the results. The top-level functionality of the IntvalPy library implements the state-of-the-art methods for recognizing and estimating solution sets for interval linear systems of equations, computing their formal solutions, and visualizing solution sets for interval equations and systems of equations. | Day and date: Thursday June 16, 2022 | Video on IIS Youtube Channel. ( Presentation is available.) |
| Andrey A. Belevantsev (Institute of System Programming of the RAS): Static analysis algorithms of the Svace tool | Abstract: Abstract: The talk presents the current state of the Svace static analyzer family that is being developed at Ivannikov Institute for System Programming of the RAS. Svace finds errors in programs written in C/C++, Java, Kotlin, Go, and C#. We will shortly describe the analysis architecture and then present the main algorithms for intraprocedural analysis based on value ids, interprocedural summary based analysis, static symbolic execution, and some auxiliary algorithms. We will also discuss static analysis specifics of the languages other than C. | Days and dates: Thursday May 26 (the first part) and Thursday June 2 (the second part), 2022 |
Video of the first part of the talk on IIS Youtube Channel (recorded May 26, 2022).
Video of the second part of the talk on IIS Youtube Channel (recorded June 2, 2022). |
| Violetta Sim (Innopolis University, Russia): Formalizing ɸ-calculus: a purely object-oriented calculus of decorated objects | Abstract: Many calculi exist for modelling various features of object-oriented
languages. Many of them are based on λ-calculus and focus either
on statically typed class-based languages or dynamic prototype-based languages. We formalize untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms
of objects and relies on decoration as a primary mechanism of object extension. It is not based on λ-calculus, yet with only four
basic syntactic constructions is just as complete (in particular, it is
Turing complete and possesses Church-Rosser property). We also
provide a sound translation to Wand’s λ-calculus with records and
concatenation, and discuss the key differences of these calculi.
This is a joint research with Nikolai Kudasov. |
Day and date: Wednesday June 1, 2022 | Video on IIS Youtube Channel. ( Chat is available.) |
| Kirill V. Ziborov (Moscow State University): Formal verification of smart contracts developed for CPP InnoChain | Abstract: The talk provided a mathematical model for the smart contracts implementation that considers the concept of a state and its change in a distributed ledger system. This model is implemented in the HOL4 proof assistant, and it demonstrates the possibility of its application for specifying the correctness properties of smart contracts. Also, two approaches to the development of smart contract models in HOL4 were reviewed and compared. Higher-order logic functions are being used in the first approach, while the second one relies on the concept of a monad and monadic functions. The model for the smart contracts execution and approaches for modeling the logic of their operation were applied for the implementation and formal verification of a smart contract that controls aircraft refueling. This example shows that in practice, smart contract models in HOL4 can be translated and integrated with the source code of the InnoChain distributed ledger system in the CakeML programming language. A repository of the project is available at https://github.com/RZRussel/hol4-contract-verification. | Day and date: Thursday May 12, 2022 | Video on IIS Youtube Channel. ( Presentation is available.) |
| Igor S. Anureev (A.P. Ershov Institute of Informatics Systems and Cyber-Physical Systems Lab, Novosibirsk, Russia): Ontological Approach to Deductive Verification of Imperative Programs | Abstract: The talk presented an ontological approach to the deductive verification of imperative programs. The approach is based on a new type of transition systems - attribute systems, the specification language of attribute systems ASL and new types of semantics of imperative programming languages - ontological, ontological operational, and ontological logical. The approach will be illustrated using a model imperative language. | Days and dates: Thursday February 10 (the first part) and Thursday April 28 (the second part), 2022 | Video of the first part on IIS Youtube Channel. |
| Natalia O. Garanina (A.P. Ershov Institute of Informatics Systems and Cyber-Physical Systems Lab, Novosibirsk, Russia): Formal Aspects of Event-Driven Temporal Logics | Abstract: The talk introduced Event-Driven Temporal Logic (EDTL) formalism for specification of requirements for reactive software. EDTL-requirements are presented as a 6-component pattern, which relates the occurrence and order of observable events in a concurrent system. The formal semantics of EDTL requirements is defined as a finite automaton, an LTL formula, and a FOL formula. We develop (1) the bounded checking algorithm for EDTL-requirements, (2) the method for checking the consistency of a set of EDTL requirements, (3) a formal semantic classification of EDTL requirements, and (4) a method for representing some classes of EDTL requirements in natural language are developed. | Day and date: Thursday April 14, 2022 | Video on IIS Youtube Channel. ( Presentation is available.) |
| Nikolay V. Shilov (Innopolis University): "Computer science and its relation to mathematics" by Donald Knuth - a paper that has changed my life. A review, a look back, and a reflection after 44 years. | Description: It was a special meeting in occasion of a traditional Day of Mathematicians celebrated annually on April 1 in some universities (including Novosibirsk State University). Nikolay V. Shilov reviewed a paper Computer science and its relation to mathematics by Donald Knuth (1974, Amer. Math. Monthly., 81(4), doi:10.2307/2318994 that he read first time in 1977. | Day and date: Friday April 1, 2022 | |
| Mariya S. Ushakova (Siberian Federal University, Krasnoyarsk, Russia): Formal verification of data driven functional parallel programs | Abstract: The talk was devoted to the use of formal verification methods for programs in the Pifagor language. This language is based on the data driven functional parallel computing model. In this model a program can be represented as a data flow graph without any resource constrains. This simplifies the process of formal verification since we only need to consider the logic of data flow dependencies in the program. A method of formal verification based on the Hoare logic has been developed for data driven functional parallel programs. For increasing the visibility of a proof, a graphical representation of the program data flow graph is used.
Also, for a better understanding the principals of data driven functional parallel computing model, the entire Pifagor project will be briefly described in the report.
The talk is based on PhD thesis submitted for defense on profile 2.3.5. Mathematical and system software for computing systems, complexes and computer networks (technical sciences). Thesis and an extended abstract are available at https://research.sfu-kras.ru/node/14728 |
Day and date: Thursdays March 17, 2022 | Video on IIS Youtube Channel. ( Presentation and chat are available.) |
| A special meeting in occasion of the International Women Day | As a year ago ruSTEP organize a special meeting
in occasion of the International Women Day.
Agenda:
|
Day and date: Tuesday March 8, 2022 | Video on IIS Youtube Channel. (Presentation by L.V. Gorodnyaya and D.A. Kondratyev, I.V. Shoshmina and chat are available..) |
| Radhakrishnan Delhibabu (School of Computer Science and Engineering Vellore Institute of Technology (VIT), Vellore, India): Application of Artificial Intelligence | Short description: Radhakrishnan Delhibabu presented his current research in Artificial Intelligence. | Day and date: Wednesday February 16, 2022 | Video on IIS Youtube Channel. ( Presentation is available.) |
| Tatyana V. Snytnikova: Efficient implementation of the model of associative computing on graphics accelerators | Abstract: The talk presents the implementation of the model of associative computing (STAR-machine) on graphics accelerators. The effectiveness of this implementation is substantiated because the GPU implementation has associative properties in a weak sense. This is confirmed by both theoretical estimates and computational experiments. The following are recommendations for adapting and optimizing associative algorithms for GPU execution. On a graph with 5000 vertices, the GPU-adapted associative graph transitive closure algorithm runs 2378 times faster than the sequential algorithm. The talk is based on PhD thesis submitted for defense on profile 05.13.11 - mathematical and software for computers, complexes and computer networks. | Day and date: Thursdays February 3, 2022 | Video on IIS Youtube Channel. ( Presentation and chat are available.) |
| 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 session was a joint event with
the Mathematical Club of the Innopolis University with a separate
Telegram chat Logic Day in Innopolis .
Agenda of the meeting (with references to materials of some talks):
|
Day and date: Friday January 28, 2022 | (Links to some are in the tab left to this one.) |
| 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 and date: Thursdays January 27, 2022 | Video on IIS Youtube Channel. ( A preliminary presentation and chat are available.) |
| 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, (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:
|
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:
|
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:
|
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 fractography 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. |