PSSV-2021

 

XII Workshop
Program Semantics, Specification and Verification:
Theory and Applications
PSSV-2021

is planned to be held in hybrid mode online (using Zoom) and offline (at Innopolis University)
on Thursday and Friday November 4-5, 2021

PSSV logo PSSV-2010-2016 workshops' pages: http://pssv-conf.ru
PSSV-2017 workshop' page: http://persons.iis.nsk.su/en/pssv2017
PSSV-2018 workshop' page: http://persons.iis.nsk.su/en/pssv2018
PSSV-2019 workshop' page: http://persons.iis.nsk.su/en/pssv2019
PSSV-2020 workshop' page: http://persons.iis.nsk.su/en/pssv2020


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
(Back to Top.)

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)
(Back to Top.)

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)
(Back to Top.)

Local Organizing Committee at Innopolis University

  • Mansur Khazeev (m.khazeev(at)innopolis.ru)
  • Nikolay Shilov (shiloviis(at)mail.ru)

General coordination and management

(Back to Top.)


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.

  • Host session: talks from Innopolis University
    • Yegor Bugayenko: EOLANG and φ-calculus

      Abstract: Object-oriented programming (OOP) is one of the most popular paradigms used for building software systems. However, despite its industrial and academic popularity, OOP is still missing a formal apparatus similar to λ- calculus, which functional programming is based on. There were a number of attempts to formalize OOP, but none of them managed to cover all the features available in modern OO programming languages, such as C++ or Java. We have made yet another attempt and created φ-calculus. We also created EOLANG (also called EO), an experimental programming language based on φ- calculus.

    • 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: The Role of Formalism in System Requirements (- joint work with Jean-Michel Bruel, Sophie Ebersold, Florian Galinier,Manuel Mazzara, Bertrand Meyer)

      Abstract: A major determinant of the quality of software systems is the quality of their requirements, which should be both understandable and precise. Most requirements are written in natural language, which is good for understandability but lacks precision. To make requirements precise, researchers have for years advocated the use of mathematics-based notations and methods, known as "formal." Many exist, differing in their style, scope, and applicability.
      The talk discusses some of the main formal approaches and compares them to informal methods. The analysis uses a set of nine complementary criteria, such as level of abstraction, tool availability, and traceability support. It classifies the approaches into five categories based on their principal style for specifying requirements: natural-language, semi-formal, automata/graphs, mathematical, and seamless (programming-language-based). It includes examples from all of these categories, altogether 21 different approaches, including for example SysML, Relax, Eiffel, Event-B, and Alloy.
      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.

  • Partner session: talks from Laboratory of Theoretical Programming of A.P. Ershov Institute of Informatics Systems
    • Igor S. Anureev: The The Ontological Approach to Deductive Program Verification

      Abstract: A new ontological approach to deductive program verification is proposed. It combines approaches based on ontologies, operational semantics, axiomatic semantics and theorem proving, and consists of 4 steps. In the first step, a set of ontological constructors for target programming language instructions are developed. Executing an ontological constructor corresponding to an instruction builds an ontological model for that instruction. Ontological constructors are defined as functions in ASL, the specially developed light-weight ontology transformation language. At the second step, the program to be verified is translated into a composition of ontological constructors, which defines the ontological model of the entire program. At the third step, the ontological model is translated into the logical model of the program. Translation algorithms are based on a combination of the operational and axiomatic semantics of the programming language and are also written in the ASL language. In addition to the verification conditions, which are the standard output in deductive verification, the logical model includes a program-dependent theory. At the fourth step, the verification conditions in the context of the theory are proved in a theorem prover. To illustrate the approach, hand dryer control program written in the Reflex language, a DSL for development of control programs, is considered. Isabelle/HOL was chosen as an interactive theorem prover.

    • 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.

(Back to Top.)

Submission and Publication

The submission Web page for PSSV-2021: via EasyChair (https://easychair.org/conferences/?conf=pssv2021) .

Program Committee solicits

  • regular research submissions in the form of an extended detailed abstract (6-8 pages in English, LNCS style recommended) to be 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) to be reviewed by a PC member.
Lecture Notes in Computer Science (LNCS) style is just recommendation while size of the submissions a real requirement: a detailed extended abstract in size should be approximately as 6-8 pages in LNCS style, an extended abstract - 6-8 pages in LNCS style.

Selected revised and extended papers will be published (after the workshop) in the Modeling and Analysis of Information Systems, a Russian peer-review journal where PSSV selected and revised papers are published since the very first edition of the workshop in 2010. (See for example Vol 27, No 4 (2020) of Modeling and Analysis of Information Systems with selected and revised papers of PSSV-2020.)

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

regular research submissions (extended detailed abstracts) Sunday October 10, 2021 (extended date)
short submissions (abstracts of work in progress, position papers, etc.)
start - Sunday October 10, 2021
end - Sunday October 17, 2021
notification for ALL submissions Sunday October 24, 2021 Tuesday October 26, 2021
workshop (hybrid) Thursday and Friday November 4-5, 2021
invitations of selected talks to post-proceedings Sunday November 7, 2021
papers for the post-proceedings Sunday November 14, 2021
notification for the post-proceedings papers around the end of November, 2021


Sponsor(s)

Information hosting: Institute of Informatics Systems logo
Selected Post-Proceeding: Modelling and Analysis of Inf. Systems logo
(Back to Top.) (Back to Menu.)