 |
PSSV-2019 |
|
|
X Workshop
|
| Annually since 2010 | |
 |
|
| PSSV-2017: http://persons.iis.nsk.su/en/pssv2017 | |
| PSSV-2018: http://persons.iis.nsk.su/en/pssv2018 |
The workshop was 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 included 4 invited talks (from academia and industry), 9 contributed academic talks, 2 guest lectures (from academia and industry) and was followed by informal short seminar on specification and verification of the standard functions.
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, 2019Poster/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, 2019Registration: by Sunday June 23, 2019 (recommended but soft date)Workshop: July 1-2, 2019Revised selected papers submission for post-workshop publication (by invitation): by Sunday September 22, 2019
Scope and Topics
Research and work in progress 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.
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).
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 (Institute of Informatics Systems, Novosibirsk, Russia)
- Igor Anureev (anureev(at)iis.nsk.su)
- Aleksey Promsky
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- mutual exclusion protocols;
- cache coherence protocols, which ensure that multiple caches in multi-core systems have consistent copies of the fragments of the main memory;
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
Programme and Venue(s)
PSSV was held in the Rector Tower of Novosibirsk State University (NSU)in the conference hall 212. Invited talk by Moshe Vardi (a joint event with PSI and CSR on Tuesday July 2) was held in the lecture theater 3307 in the New Building of NSU. Workshop Programme (with some presentations) is available at https://persons.iis.nsk.su/files/persons/pages/pssv_final_programme.pdf.
 |
 |
 |
Types of Submissions and Publications
Program Committee had solicited 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 could be included in an appendix up to 4 pages for Program Committee.) Each regular research submission have been reviewed by 3 PC members. Program Committee also had solicited poster and student papers (up to 4 pages). Each of these submissions were reviewed by a PC member. Easy Chair conference management system was in use for submissions, reviewing, PC discussions and decision, authors' notification and other workshop-related correspondence.
Extended abstracts of all accepted contributions had been published before the workshop:
- extended abstracts of all regular and short talks - 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.
Selected revised and extended papers have been published after the workshop in Russian peer-review journal Modeling and Analysis of Information Systems (Vol 26, No 4, 2019) (https://www.mais-journal.ru/jour/issue/view/112/showToc). 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).
Sponsorship
Information hosting:
Hosting (venue) organization: 