 |
PSSV-2021 |
|
|
XII Workshop
|
| was held fully online using Zoom |
| on Thursday and Friday November 4-5, 2021 |
| Annually since 2010 | |
 |
|
| PSSV-2019: http://persons.iis.nsk.su/en/pssv2019 | |
| PSSV-2020: http://persons.iis.nsk.su/en/pssv2020 |
Actual Programme of PSSV-2021 (with links to abstracts and recordings of the talks) is available here
| Important Dates | Scope and Topics | Program Committee and Contacts | Co-Chairs and Steering Committee | Organizing Committee | Invited Sessions and Speakers | Submission and Publication | Sponsor(s) |
Scope and Topics
Research, work in progress, position and student papers were welcome. List of topics of interest included (but was not limited to):
- formalisms for program semantics
- formal models and semantics of programs and systems
- semantics of programming and specification languages
- formal description techniques
- logics for formal specification and verification
- deductive program verification
- automatic theorem proving
- model checking of programs and systems
- static analysis of programs
- formal approach to testing and validation
- program analysis and verification tools
Program Committee:
(tentative list, to be confirmed)- Thomas Baar (University of Applied Sciences HTW Berlin, Germany)
- Alexander Bolotov (University of Westminster, UK)
- Vladimir Itsykson (St. Petersburg State Polytech. University, Russia)
- Andrei Klimov (Keldysh Institute of Applied Mathematics, Moscow, Russia)
- Igor Konnov (Informal Systems, Austria)
- Victor Kuliamin (Institute for System Programming, Moscow, Russia)
- Alexei Lisitsa (University of Liverpool, UK)
- Irina Lomazova (Higher School of Economics, Moscow, Russia)
- Manuel Mazzara (Innopolis University, Russia)
- Dmitry Mordvinov (St. Petersburg State University and JetBrains Research, Russia)
- Sergey Staroletov (Polzunov Altai State Technical University, Barnaul, Russia)
- Nina Yevtushenko (Tomsk State University and Institute for System Programming, RAS, Moscow, Russia)
Program Co-Chairs
- Nikolay Shilov (Innopolis University, Russia, shiloviis(at)mail.ru)
- Vladimir Zakharov (Moscow State University, Russia, zakh(at)cs.msu.su)
Steering Committee
- Valery Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia, vnep(at)iis.nsk.su)
- Valery Sokolov (Yaroslavl State University, Yaroslavl, Russia, valery-sokolov(at)yandex.ru)
Local Organizing Committee at Innopolis University
- Mansur Khazeev (m.khazeev(at)innopolis.ru)
- Nikolay Shilov (shiloviis(at)mail.ru)
General coordination and management
- Alexei Promsky (Deputy Director of the A.P. Ershov Institute of Informatics Systems)
- Nikolay Shilov (Head of the Lab of Software and Service Engineering of the Innopolis University)
Invited Sessions and Speakers
- Session devoted to the anniversary the achievements of Professor Alexander K. Petrenko,
Head of the
Software Engineering Department of Institute for System Programming Russian Academy of Sciences (SED ISP RAS)
- Alexander K. Petrenko: The position of formal methods in nowadays software industrial development
Abstract: Formal methods of software development as they are understood today emerged in the late 1960s. They are steadily evolving, but the degree of their practical application is low. By itself, this problem attracts the attention of researchers. The reasons hindering the expansion of the use of formal methods are constantly being analyzed. Some of these reasons are widely known, while others have received little attention. Understanding these reasons is important for both the enhancing of formal methods themselves and their increasingly widespread use in practice.
The talk examines the tendencies of rethinking the positions of formal methods in the development of industrial software and the author's experience in solving technical and organizational problems over the past 30 years, from works for the Buran, Soviet space programme, to recent projects for the development and the verification of safety critical software systems. -
Victor V. Kuliamin: Formal Security Models
Abstract: The talk considers some patterns in formalizing security models of various systems, mostly related with access control. It sums up the ISP RAS experience in formal modelling of security requirements of several industrial operating systems and distributed control systems.
-
Alexander S. Kamkin: High-Level Synthesis of Computing Systems: Motivation, Challenges, and
Existing Solutions
Abstract: Recently, there has been a decrease in the growth rate of single-processor performance. The main reasons for that lie in semiconductor physics (in the 2000s, Dennard's scaling law stopped working). The solution is to create application-specific computers focused on particular tasks. The problem is moved to the economic plane: how to make development of such systems profitable? Obviously, comprehensive design automation is required, which can be achieved (among other things) through high-level synthesis (HLS). The latter is understood as automated construction of digital circuits from behavioral (algorithmic) descriptions. This talk provides a brief overview of the HLS area, including problems, approaches to their solution, and available tools.
-
Alexey V. Khoroshilov: Verification of operating systems
The talk presents experience of ISPRAS in design and application of various verification techniques to operating systems including model-based testing, systematic fault injection, data race detection, software model checking and deductive verification. Also we discuss how this experience is used in development of the ARINC-653 real-time operating system according DO-178C requirements.
- Alexander K. Petrenko: The position of formal methods in nowadays software industrial development
- Host session: talks from
Innopolis University
-
Nikolai D. Kudasov: Nameless and scope-safe (de Bruijn notation as a nested datatype)
Abstract: Implementing lambda terms with named bound variables is awkward because of renaming. So it is more than common to use a nameless representation using de Bruijn indices for variables. But of course there's more than one way to cook a lambda term. About 20 years ago Richard Bird and Ross Patterson showed how nested datatypes can represent generalised de Bruijn indices. We will see this idea and what benefits it may provide to implementations of languages and proof assistants.
- Alexandr V. Naumchev: Security audit of code using contracts and program proving. (Attention: the topic has changed!)
Abstract: Secure software is defined as software that exposes no undocumented functionality. This definition assumes that all desirable functionality is fully understood and documented in a consistent manner. Functionalities, however, are elicited and documented using notations distant from code. How then should software developers who write code understand whether their code exposes undocumented functionality? This work offers a formal definition of secure code that roots back to Hoare logic and Design by Contract (DbC). The software process resulting from the proposed definition relies on AutoProof, a DbC-based program prover, and makes it possible to formally verify the security of the code. Experimental findings suggest that the approach is practical in the context of a programming language with contracts and the associated program prover. The experiments were performed on EiffelBase2, a fully verified library of containers that had been specified with the strong emphasis on the impossibility of having undocumented functionality. The talk gives numerous examples of malicious code injections in EiffelBase2 that "bypass" the specification and pass the verification with AutoProof.
The talk discusses a number of open questions, including seamlessness, the role of tools and education, and how to make industrial applications benefit more from the contributions of formal approaches.
-
Nikolai D. Kudasov: Nameless and scope-safe (de Bruijn notation as a nested datatype)
- Partner session: talks from
Laboratory of Theoretical Programming of A.P. Ershov Institute of Informatics Systems
- Nataliya O. Garanina: The Optimization Problem with Model Checking
Abstract: For systems which demonstrate various behaviors, the optimization problem is to determine the best behavior (in some sense). The talk gives an overview of approaches to solving this problem with various model checking techniques. We also present the ideas of using the method of counterexamples for the problem of auto-tuning parallel programs.
- Dmitry A. Kondratyev: Automatic deductive verification of C programs using the C-lightVer system
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 automation of deductive verification consists of following challenges: problem of loop invariants, problem of automatic verification condition proving and problem of error localization. Following approaches are implemented in the C-lightVer system to solve these challenges: symbolic method of verification of definite iterations, strategies for proving verification conditions and semantic labeling method. Symbolic method of verification of definite iterations allows us to avoid defining invariants in the case of special kinds of loops. Proof strategies allow us to automatize verification conditions proving for various classes of C programs. Semantic labeling method allows us to generate explanations of unproven verification conditions for error localization. These methods are the base of the complex approach of the C-lightVer system to deductive verification automation.
- Nataliya O. Garanina: The Optimization Problem with Model Checking
Submission and Publication
Program Committee had solicited
- regular research submissions in the form of an extended detailed abstract (6-8 pages in English, LNCS style recommended) reviewed by 3 PC members;
- work in progress, position, poster and student research reports in the form of extended abstract (3-4 pages in English, LNCS style recommended) reviewed by a PC member.
Selected revised and extended papers were published (after the workshop) in the Vol 28, No 4 (2021) of Modeling and Analysis of Information Systems . ( Modeling and Analysis of Information Systems is a Russian peer-review journal where PSSV selected and revised papers are published since the very first edition of the workshop in 2010.) We expect (as it was in the previous years of the PSSV) that English translations of some of these selected papers will appear next year in Automatic Control and Computer Sciences(http://www.springer.com/computer/hardware/journal/11950) (indexed by WoS and Scopus).
Important dates
| Activity or milestone | Current status |
| | passed |
| |
passed |
| | done |
| | done |
| | done |
| | done |
| | passed |
| | done |
| | done |
Sponsor(s)
| Information hosting: |  |
| Selected Post-Proceeding: |  |