XI Workshop
Program Semantics, Specification and Verification:
Theory and Applications

will be held online November 3-4, 2020


  • Submission server for abstracts of work in progress, position papers and posters will be open October 12-19, 2020.
  • Notification for ALL submissions will be send to authors by October 26, 2020
  • PSSV-2020 will host a panel discussion on (experimental and industrial) contemporary programming languages. Andrey Breslav (JetBrains), Aleksei Nedoria (Huawei), Antony Polukhin (Yandex), Alexey Nezvanov (The Hight School of Economics) and Evgene Zouev, Alexey Kanatov and Nikolai Kudasov (Innopolis University) have confirmed their participation as panelists.
  • In addition to academic invited talks (already announced on this page), there will be one invited industrial talk from Leading Research Center for Blockchain Technology of Innopolis University, which will be presented by Leonid Merkin. The invited talk will be followed by a short talk Verification of HotStuff With TLA+/TLC for an Industrial Project (by Vladimir Kukharenko (MIPT), Kirill Ziborov (MSU), Rafael Sadykov (MSU), Alexandr Naumchev (Innopolis University)).

PSSV logo PSSV-2010-2016 workshops' pages:
PSSV-2017 workshop' page:
PSSV-2018 workshop' page:
PSSV-2019 workshop' page:

Important Dates Scope and Topics Program Committee and Contacts Co-Chairs and Steering Committee local Organizing Committee Invited Speakers and Talks Programme and Venue(s): TBD Types of Submissions and Publications Sponsor(s)

Scope and Topics

Research, work in progress, position and student papers were welcome. List of topics of interest includes (but is 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:

  • Natasha Alechina (Utrecht University, Netherlands),
  • Alexander Bolotov (University of Westminster, UK),
  • Vladimir Itsykson (St. Petersburg State Polytech. University, Russia),
  • Igor Konnov (Informal Systems, Austria),
  • Victor Kuliamin (Institute for System Programming, Moscow, Russia),
  • Andrei Klimov (Keldysh Institute of Applied Mathematics, Moscow, Russia),
  • Alexei Lisitsa (University of Liverpool, UK),
  • Irina Lomazova (Higher School of Economics, Moscow, Russia),
  • Manuel Mazzara (Innopolis University, 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)
  • Vladimir Zakharov (Moscow State University, Russia, zakh(at)

Steering Committee

  • Valery Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia, vnep(at)
  • Valery Sokolov (Yaroslavl State University, Yaroslavl, Russia, valery-sokolov(at)
(Back to Top.)

Local Organizing Committee (Higher School of Economics - National Research University)

  • Irina Lomazova (ilomazova(at)
  • Vladimir Zakharov (zakh(at)
(Back to Top.)

Invited speakers

  • Natasha Alechina (Intelligent Software Systems, Information and computing sciences department, Utrecht University, The Netherlands): State of the Art in Logics for Verification of Resource-Bounded Multi-Agent System ( Check abstract here.)
  • Ekaterina Komendantskaya (School of Mathematical and Computer Sciences, Heriot-Watt University Edinburgh, UK): Refinement types for Verification of Neural Networks (This is a collaborative work with Wen Kokke and Daniel Kienitz. Check abstract here.)
  • Samvel K. Shoukourian (IT Educational and Research Center, Yerevan State University, Armenia): Polynomial algorithm for equivalence problem of deterministic multitape finite automata (This is a joint work with Hayk A. Grigoryan. Check abstract here.)
  • Ilya Sergey (Yale-NUS College and National University of Singapore): Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast ( Check abstract here.)
(Back to Top.)

Types of Submissions and Publications

Program Committee solicits

  • regular research submissions in the form of extended abstracts (up to 8 pages, LNCS style) in English (additional details could be included in an appendix up to 4 pages for Program Committee), each regular research submission will be reviewed by 3 PC members;
  • work in progress, position, poster and student papers (up to 4 pages), each of these submissions will be reviewed by a PC member.

Right now Easy Chair submission page is open for regular papers.

Extended abstracts of all accepted papers will be published before the workshop in electronic journal System Informatics ( Selected revised and extended papers will be published after the workshop in Russian peer-review journal Modeling and Analysis of Information Systems ( 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( (indexed by WoS and Scopus).

Important dates

regular research submissions (extended abstracts) September 28, 2020 (extended date)
short submissions (abstracts of work in progress, position papers and posters)
start - October 12, 2020
end - October 19, 2020
notification for ALL submissions October 26, 2020 (extended date)
final versions of regular research submissions (for pre-proceedings) October 31, 2020 (extended date)
workshop (offline or online) November 3-4, 2020
invitations of selected talks to post-proceedings November 5, 2020
papers for the post-proceedings November 15, 2020
notification for the post-proceedings papers November 15, 2020


Information hosting: System Informatics logo
Pre-proceeding: IIS eng logo
Post-proceeding: IIS eng logo
(Back to Top.)