Eighth Workshop
Program Semantics, Specification and Verification:
Theory and Applications
(PSSV 2017, June 26, 2017)
Annually since 2010
Call for Papers
The workshop will be held at the Faculty of Computational Mathematics and Cybernetics of Lomonosov Moscow State University
https://cs.msu.ru/en
in Moscow, Russia
in affiliation with
A.P. Ershov Informatics Conference (the PSI Conference Series, 11th edition
Workshop language: English.
Important dates
Extended abstract submission: April 24, 2017 (- extended date!)Notification: May 21, 2017Final versions of accepted extended abstracts for pre-workshop publication: June 04, 2017Free registration via Google-form by June 22, 2017, or on site on June 26, 2017 Workshop: June 26, 2017 - Revised selected papers submission for post-workshop publication: September 03, 2017
(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.)
Invited Speakers:
- Alexander V. Kogtenkov (Eiffel Software, USA): Making void safety practical
Abstract: Null pointer dereferencing remains one of the major issues in modern object-oriented languages. An obvious addition of keywords to distinguish between never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. The proposed solution avoids explicit encoding of these intermediate states in program texts in favor of statically checked validity rules that do not depend on special conditionally non-null types. Object initialization examples suggested earlier are reviewed and new ones are presented to compare applicability of different approaches. Usability of the proposed scheme is assessed on open-source libraries with a million lines of code that were converted to satisfy the rules.
- Victor V. Kuliamin (Institute for System Programming, Moscow, Russia): Verification of operating system components (Joint talk with A.K. Petrenko and A.V. Khoroshilov)
Abstract:
The talk concerns recent advances in reaching the goal of industrial operating system (OS) verification. By industrial OS we mean a system actively used in some industrial domain, elaborated and maintained for a significant time, not a proof-of-concept OS developed with mostly research intentions. We consider decomposition of this goal into tasks related with various functional components of OS and various properties under verification, and application of different verification methods to those tasks.
This is a trial to explicate and summarize the experience of several projects on various OS components and different OS features verification conducted in ISP RAS.
- Dmitry A. Zaitsev (International Humanitarian University, Odessa, Ukraine): Sleptsov Net Computing
Abstract:
Petri nets have been known for years as a model of concurrent systems but their computationally universal extensions are exponentially slow comparing Turing machines, especially when implementing arithmetic operations.
A Sleptsov net concept, suggested quarter a century ago, recently acquired its second birth due to its ability of fast implementation of basic arithmetic operations. Firing a transition in a few instances at a step leads to universal constructs which run in polynomial time. In Sleptsov net computing, a program, written in Sleptsov net language preserving concurrency of an application area, runs on Sleptsov net processor which implements concurrent firing of transitions in multiple instances providing fast computations.
Motivation for new models of hyper-computations is presented. Sleptsov net is introduced compared to Petri and Salwicki nets. A concept of universal Sleptsov net, as a prototype of a processor in Sleptsov net computing, is discussed. A small universal Sleptsov net that runs in polynomial time is constructed; it consists of 13 places and 26 transitions. Principles of programming in Sleptsov nets, as composition of reverse control flow and data, are developed. Standard control flow patterns include sequence, branching, loop, and parallel execution. Basic modules, which implement efficiently copying, logic, and arithmetic operations, are developed. Special dashed arcs are introduced for brief specification of input and output data of modules (subnets). Ways of hierarchical composition of a program via substitution of a transition by a module are discussed. Examples of Sleptsov net programs for data encryption, fuzzy logic, and partial differential equations are presented. Enterprise implementation of Sleptsov net computing promises ultra-performance.
(History of Sleptsov nets)
- Antony Polukhin ( Russian National Working Group on C++ Standardization ): Contracts in C++ (Evening Lecture)
Abstract: We will consider some new (still developing) features of the language C ++ that can be very practical for better function definition, namely - the standard heading file <algorithm> and ways how to use it in general and with contracts in particular.
(Back to Top.)
Program :
| Time | Speaker(s) | Title |
| 10:00 – 10:45 |
Victor V. Kuliamin, Alexey V. Khoroshilov and Alexander K. Petrenko |
Verification of operating system components (invited talk,
paper,
presentation) |
| 10:45 – 11:15 |
Maryasov Ilya, Valery Nepomniaschy and Dmitry Kondratyev |
Verification of Definite Iteration over Arrays with Loop Exit in C Programs (regular talk, paper,
presentation)
|
| 11:15 – 11:45 |
Artyom Aleksyuk and Vladimir Itsykson |
Automated Semantics-Driven Source Code Migration: a Pilot Prototype (regular talk,
paper,
presentation) |
| 11:45 – 12:15 |
Coffee Break |
| 12:15 – 13:00 |
Alexander V. Kogtenkov | Making void safety practical (invited talk,
paper,
presentation) |
| 13:00 – 13:30 |
Thomas Baar |
Towards Measuring the Abstractness of State Machines based on Mutation Testing
(regular talk,
presentation) |
| 13:30 – 14:00 |
Bogdan Mingela, Nikolay Troshkov, Manuel Mazzara, Larisa Safina, Alexander Tchitchigin and Daniel De Carvalho |
Towards Static Type-checking for Jolie (regular talk, paper,
presentation) |
| 14:00 – 15:00 |
Lunch |
| 15:00 – 15:45 |
Dmitry A. Zaitsev |
Sleptsov Net Computing (invited talk, paper in Russian,
presentation) |
| 15:45 – 16:15 |
Natalia Kushik, Nina Yevtushenko, Igor Burdonov and Alexander Kossatchev |
Synchronizing and Homing Experiments for Input/output Automata (regular talk
paper,
presentation) |
| 16:15 – 16:45 |
Tatiana Shmeleva |
Security of Grid Structures with Cut-through Switching Nodes (regular talk,
paper,
presentation) |
| 16:45 – 17:15 |
Coffee Break |
| 17:15 – 17:45 |
Natalia Garanina |
An Ontological Approach to a System of Requirements Patterns (position talk,
presentation) |
| 17:45 – 18:15 |
Sergey Staroletov |
Design and implementation a software for water purification with using automata approach and specification based analysis (regular talk,
paper,
presentation) |
| 18:15 – 19:00 |
Antony Polukhin |
Contracts in C++ (evening lecture,
presentation) |
(Back to Top.)
Program Committee:
- Natasha Alechina (University of Nottingham, UK),
- Sergey Baranov (St.Petersburg Institute for Informatics and Automation, Russia),
- Alexander Bolotov (University of Westminster, UK),
- Mohamed Elwakil (Northern Arizona University Flagstaff, US),
- Nina Evtushenko (Tomsk State University, Russia),
- Vladimir Itsykson (St. Petersburg State Polytech. University, Russia),
- Igor Konnov (Institute of Information Systems, TU Wien, Austria),
- Victor Kuliamin (Institute for System Programming, Moscow, Russia),
- Alexei Lisitsa (University of Liverpool, UK),
- Irina Lomazova (Higher School of Economics, Moscow, Russia),
- Valery Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia),
- Ruslan Smelyansky (Moscow State University, Russia),
- Valery Sokolov (Yaroslavl State University, Yaroslavl, Russia).
(Back to Top.)
Program Co-Chairs
- Nikolay Shilov (Innopolis University, Kazan, Russia, n.shilov(at)innopolis.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.)
Presentation and Publication
At least one author of every accepted paper should present a talk at the workshop.
- All accepted REGULAR extended abstracts as well as extended abstracts of INVITED talks
will be published before the workshop in electronic journal System Informatics
( http://www.system-informatics.ru/en/index).
Authors are kindly asked to revise their extended abstracts according to the reviewers’ recommendations and
- send (not later than June 4) revised versions to System Informatics via e-mail (si@iis.nsk.su) with subject "Application: PSSV-2017";
- send (not later than May 28) short abstracts (0.5 page) in LaTeX article style/class to Vladimir Zakharov via e-mail
(zakh@cs.msu.su) with subject line "Abstract: PSSV-2017".
Preparing revised version for publication in System Informatics please refer Instructions for the Authors available at
http://www.system-informatics.ru/en/for_authors.
- All extended abstracts accepted as POSITION papers will be published before the workshop together with
short abstracts of accepted papers in a collection of abstracts.
Authors are kindly asked to revise their extended abstracts according to the reviewers’ recommendations and send (not later than June 4)
to Vladimir Zakharov via e-mail
(zakh@cs.msu.su) with subject line "Position paper: PSSV-2017". (Size of the revised extended abstract shouldn’t exceed 8 pages.)
Revised and extended versions of selected papers presented at the workshop
will be published after the workshop in one of Russian peer-review journals.
(Back to Top.)
Registration and Related Issues:
- PSSV and PSI registrations are independent (i.e. they don't assume cross-participation).
In case of a need of visa support - please visit registration page of PSI conference at
http://psi.ispras.ru/en/registration.html.
- Participation in PSSV-2017 is free, but all participants (including authors of accepted papers and invited speakers)
are kindly asked to register using Google-form at https://goo.gl/forms/tPQ2nd35vEymHQXC2 not later than by June 22, 2017.
- At day the workshop (June 26, 2017) please come to the workshop venue with identity card (passport).
- Program and concrete venue of the workshop will come soon!
(Back to Top.)
Sponsorship
Host of the event:
Information and Publication:
(Back to Top.)
How to get PSSV venue:
Workshop PSSV 2017 will be held in Lomonosov Moscow State University, faculty of Computational Mathematics and Cybernetics (CMC, 2-nd Educational Building), in the room 582 (5-th floor).
Below you could find some useful information on the venue.
For further details and directions please follow the link or refer Google Maps .
(Back to Top.)
|
