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

(PSSV-2019, July 1 and 2, 2019, Novosibirsk Akademgorodok, Russia)

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

The workshop is a satellite event of A.P. Ershov Informatics Conference (the PSI Conference Series, 12th edition) in the framework of Computer Science Summer in Russia (CSSR). Workshop Programme includes 4 invited talks (from academia and industry), 9 contributed academic talks, 2 guest lectures (from academia and industry) and is followed by informal short seminar on specification and verification of the standard functions.

Important Dates Scope and Topics Program Committee and Contacts Co-Chairs and Steering Committees Novosibirsk local organizing committee Invited Speakers Accepted talks and Programme Venue(s) and Directions Submissions, Publication and Presentation Registration, Visa and Accommodation Sponsors

Important dates

  • Paper (extended abstract) submission due date: Wednesday May 1, 2019 (extended but strict)
  • Notification: Monday May 27, 2019 (extended but strict)
  • Start of poster/student paper submission: Monday May 27, 2019
  • Poster/student paper submission due date: Sunday June 2, 2019 (strict)
  • Final versions of accepted extended abstracts for pre-workshop publication: Sunday June 9, 2019 (extended but strict)
  • Poster/student paper notification: Sunday June 9, 2019
  • Registration: by Sunday June 23, 2019 (recommended but soft date)
  • Workshop: July 1-2, 2019
  • Revised selected papers submission for post-workshop publication (by invitation): TBD
(Back to Top.)

Scope and Topics

Research and work in progress papers are 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 (University of Nottingham, UK),
  • Alexander Bolotov (University of Westminster, UK),
  • Vladimir Itsykson (St. Petersburg State Polytech. University, Russia),
  • Igor Konnov (INRIA Nancy & LORIA, France),
  • 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),
  • Valery Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia),
  • Valery Sokolov (Yaroslavl State University, 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 (Institute of Informatics Systems, Novosibirsk, Russia)

  • Igor Anureev (anureev(at)
  • Aleksey Promsky
(Back to Top.)

Invited Speakers

  • Alexei Lisitsa (Department of Computer Science, University of Liverpool): Proving safety by disproving: finite countermodel finding for the infinite-state and parameterized verification
    • Abstract: Traditional model checking has been very successful in the verification of finite state systems. In many cases, though the finite state abstraction is not enough, as we might need to verify the algorithm or protocol for essentially unbounded computation/execution, e. g. to ensure that a protocol is correct for any number of participants, or for any size of a data structure. In such cases, we are facing infinite state, or parameterized systems, the verification of which in general is an undecidable problem.
      In this talk, we introduce and overview conceptually simple but powerful and efficient method for automated safety verification of infinite-state and parameterized system. The method utilises modelling of reachability between the states of a system as derivability in the classical first-order (FO) logic. With such modelling to establish the safety of a system, that is non-reachability of unsafe states, it is sufficient to show that a particular first-order formula is not provable. In this FCM method, the latter task is delegated to the available automated finite model finding procedures.
      In the talk we present theoretical foundations, show the relative completeness of the method and illustrate it by numerous applications for infinite-state and parameterized verification tasks selected from the areas of
      1. mutual exclusion protocols;
      2. cache coherence protocols, which ensure that multiple caches in multi-core systems have consistent copies of the fragments of the main memory;
      3. recreational mathematics, including the first fully automated solution of so-called MU-puzzle, taken from the famous book Goedel, Escher, Bach: An Eternal Golden Braid book by D. Hofstadter.
  • Sergey P. Shary (Novosibirsk State University and Institute of Computational Technologies of Siberian Branch of Russian Academy of Sciences, Novosibirsk): Quantifier solutions to interval systems of linear algebraic equations
    • Abstract: The talk is devoted to interval systems of linear algebraic equations, a classical object, which is quite simple, but serves as a basis for a large number of mathematical models of the real world. Solutions and sets of solutions for such systems can be defined in a wide variety of ways, since the interval uncertainty, by its very nature, has a dual character, which is associated with the use of different logical quantifiers, either existence or universality. In this way, we obtain definitions of the so-called quantifier solutions of interval equations, having a clear meaning and can be interpreted as solutions of games or decision-making processes under conflict and uncertainty.
      We consider various numerical methods for estimating sets of quantifier solutions for interval systems of linear algebraic equations. They are based on the use of the Kaucher complete interval arithmetic, where improper (reverse) intervals are allowed and basic arithmetic operations are algebraic and order completions of those for the usual real intervals.
  • Bin Fang (Huawei): Formal Modelling and Verification for Heap-manipulating Programs
    • Abstract: First, we demonstrate how to obtain formal specifications of sequential dynamic memory algorithms using a refinement-based approach. We define a hierarchy of models ranked by the refinement relation that capture a large variety of techniques and policies employed by memory allocation algorithms. This hierarchy forms an algorithm theory for memory allocators using list and it could be extended with other policies. The formal specifications are written in Event-B annotation and the refinements have been proved using the Rodin platform. Also we investigate applications of the formal specifications obtained, such as model-based testing, code generation and verification on code level.
      Second, we define a technique for inferring precise invariants of heap-manipulating programs based abstract interpretation which is a framework used in static analysis. The abstract domain is constructed step-by-step by combining shape and numeric abstractions. The abstract elements are presented by our fragment of Separation Logic which can tack the complex construal and numerical properties on the structure of memory and on its size and content. To obtain compact elements of this abstract domain, we propose a composition operator to link hierarchical abstractions of the shape. It increases the readability and modularity of the specification as well as the modularity of the static analysis method.

Accepted talks and Programme

Venues and Directions

(Back to Top.)

Submission, Publication and Presentation

Program Committee invites regular research submissions (on topics of program semantics, specification and verification) in the form of extended abstracts (up to 8 pages, Lecture Notes in Computer Science style) in English. Additional details may be included in an appendix up to 4 pages for Program Committee. Each regular research submission will be reviewed by 3 PC members. Program Committee also invites poster and student papers (up to 4 pages). Each of these submissions submission will be reviewed by PC. All submissions (regular, poster and student) should be via EasyChair conference system (

All accepted papers will be published before the workshop:

  • all regular and short papers - in a special issue of the electronic journal System Informatics (2019, n.14) (done!),
  • extended abstracts of all poster talks altogether with short abstracts of all invited, regular and short talks - in printed volume of abstracts (to be available on the workshop).

Selected papers will be published after the workshop in Russian peer-review journal Modeling and Analysis of Information Systems ( and then translated and published in Automatic Control and Computer Sciences( (indexed by WoS and Scopus).

At least one author of every accepted paper should present a talk on the workshop.

Conference Proceedings

X Workshop PSSV — Abstracts (PDF, 2.49 MB)

Registration, Visas, Accommodation:

Please proceed to REGISTRATION section of the PSI web-page. All participants (including speakers and Program Committee members) should register prior the workshop dates (i.e. July 1), nevertheless is highly recommended for participants to register a week ahead (i.e. by Sunday June 23, 2019.


Information hosting: IIS eng logo

Hosting (venue) organization: Novosibirsk State University logo

(Back to Top.)