PSSV 2016

Seventh Workshop
Program Semantics, Specification and Verification:
Theory and Applications
(PSSV 2016, June 14-15, 2016)

Main Workshop page: http://pssv-conf.ru PSSV logo

The workshop will be held in affiliation with International Ńonference "Computer Science in Russia" (ŃSR 2016, http://logic.pdmi.ras.ru/csr2016/) in St. Petersburg, Russia. PSSV logo
Official language: English.

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.

Program Committee:

  • Natasha Alechina (University of Nottingham, UK),
  • Sergey Baranov (St.Petersburg Institute for Informatics and Automation, Russia),
  • Alexander Bolotov (University of Westminster, UK),
  • Nina Evtushenko (Tomsk State University, Russia),
  • Vladimir Itsykson (St. Petersburg State Polytech. University, Russia),
  • Victor Kuliamin (Institute for System Programming, Moscow, Russia),
  • Alexei Lisitsa (University of Liverpool, UK),
  • Irina Lomazova (Higher School of Economics, Moscow, Russia),
  • Nikolay Shilov (Institute of Informatics Systems, Novosibirsk, Russia),
  • Vladimir Zakharov (Moscow State University, Russia).

Program Chairs:
  • 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)

Organization Chair:
  • Nikolay Shilov (Institute of Informatics Systems, Novosibirsk, Russia, shilov(at)iis.nsk.su)

Program

Tuesday June 14, 2016
09.00 - 10.00 Registration
Session 1
10.00 - 11.00 Dmitry Nadezhin. Theorem proving with ACL2 for industry artefacts (Invited Talk)
11.00 - 11.30 Irina Shoshmina. Developing formal requirements to distributed program system behaviour
11.30 - 12.00 Coffee-Break
12.00 - 12.30 Nikolay Shilov: Fix point Consideration of Discrete Dynamic Programming Algorithm Design Pattern
12.30 - 13.00 Andrei Molchanov: Non-empty intersection problem for the free commutative algebraic program model
13.00 – 14.30 Lunch
Session 2
14.30 - 15.30 Andrey Karpov and Evgeniy Ryzhkov. Experience of checking open source projects by PVS-Studio team: how programmers on C, C ++ and C # make mistakes (Invited talk)
15.30 - 16.00 Vladimir Zakharov and Gulgaisha Temerbekova. On the minimization and equivalence checking of sequential reactive systems
16.00 - 16.30 Vladimir Itsykson: The formalism for software library semantic specification
16.30 - 17.00 N. Vizovitin , V. Nepomniaschy and Stenenko A.A. Verification of UCM Models with Scenario Control Structures Using Coloured Petri Nets
Wednesday June 15, 2016
Session 3
10.00 - 11.00 Igor Konnov: Model Checking of Threshold-based Fault-tolerant Distributed Algorithms (Invited Talk)
11.00 - 11.30 Tatyana Liah and Vladimir Zyubin: Model Checking of industrial control algorithms in combination with virtual objects
11.30 - 12.00 Coffee-Break
12.00 - 12.30 Natalia Shabaldina and Maxim Gromov: Using balm-ii for deriving parallel composition of timed finite state machines with output delays and timeouts: work-in-progress
12.30 - 13.00 Sergey Baranov and Victor Nikiforov: Application Density and Feasibility Checking in Real-Time Systems
13.00 – 14.30 Lunch
Session 4
14.30 - 15.30 Bertrand Meyer. Verification of OO programs: the toughest open issues (Invited talk)
15.30 - 16.00 N. Garanina and E.Sidorova. A Verification Method for a Family of Multi-agent Systems of Ambiguity Resolution
16.00 - 16.30 Anton Ermakov and Nina Yevtushenko. Increasing the fault coverage of tests derived against Extended Finite State Machines
16.30 - 17.00 A.Tiugashev. Methods of Software Verification in Space Industry

Sponsors:

  • Invited talks are supported by PVS-Studio, PVS-Studio is the static code analysis tool for C, C++ and C# programs;
  • Preliminary publication is supported by electronic journal System Informatics published by Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences;
  • Post-workshop publication of selected revised and extended papers will be supported by journal Modeling and Analysis of Information Systems published by Yaroslavl State University.

Contacts and Updates:

For further details and updates please refer the main Workshop page at http://pssv-conf.ru. In case of program question please contact Program chairs, for organization issues – the Organization Chair.