PSSV-2018

  

IX Workshop
Program Semantics, Specification and Verification:
Theory and Applications
(PSSV-2018, June 21-22, 2018, Yaroslavl, Russia)

Annually since 2010
PSSV logo PSSV-2017: http://persons.iis.nsk.su/en/pssv2017

Workshop venue: conference-hall "Tensor" (Yaroslavl, Uglicheskaya str., 36).

Important Dates Scope and Topics Program Committee and Contacts Co-Chairs, Steering and Organizing Committees Invited Speakers, Memorial Session, and talk from Hosting Organization Programme and Publication Registration, Accommodation, and links to Workshop photos Sponsors and hosting

Important dates
  • Paper (extended abstract) submission: May 1 May 4, 2018
  • Notification: May 27 May 29, 2018
  • Final versions of accepted extended abstracts for pre-workshop publication: June 4, 2018
  • Poster/student paper submission: June 4, 2018
  • Poster/student paper notification: June 10, 2018
  • Registration: June 17, 2018
  • Workshop: June 21-22, 2018
  • Revised selected papers submission for post-workshop publication (by invitation): September 10, 2018
(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),
  • Egor Kuzmin (Yaroslavl State University, Russia, to be confirmed),
  • 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),
  • Alexander Okhotin ( St. Petersburg State University, Russia),
  • Aleksey Promsky (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)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)

Organizing Committee
  • Egor Kuzmin (Yaroslavl State University, Russia, kuzmin(at)uniyar.ac.ru)
  • Valery Sokolov (Yaroslavl State University, Yaroslavl, Russia, valery-sokolov(at)yandex.ru)
(Back to Top.)

Invited Speakers
  • Daniel de Carvalho: Taylor expansion of proofs and static analysis of time complexity (Link to presentation.)
    • Abstract: Gentzen introduced (1934) two different formalisms for proofs in intuitionistic logic: natural deduction (NJ) and sequent calculus (LJ). The Curry-Howard-de Bruijn isomorphism between NJ and simply-typed lambda-terms (1940) arose in the 60's, while there was no such an isomorphism for LJ, essentially because equality between LJ proofs is ``evil''. In 1971, Girard extended this isomorphism to the second-order considering an expressive polymorphic programming language (System F). Fifteen years later, inspired by Berry's notion of stability (1978), which refines Scott's notion of continuity (1972), he introduced coherence spaces as a model of System F; that is how linear logic was born. Linear logic is a refinement of intuitionistic and classical logic that distinguishes among all the proofs those using exactly once their assumptions. Taylor expansion of proofs, which expresses proofs as series of their linear approximants, was considered by Girard from a semantic viewpoint. Since the 2000s Ehrhard has been investigating topological vectorial spaces as models of linear logic. This investigation led him with Regnier to introduce differential nets (2006), which allow to express syntactically Taylor expansion.
      I will address the two following related problems: 1) Friedman proved (1975) that the standard model for the lambda-calculus with sets and functions is complete for beta-reduction; can we obtain a similar result for cut-elimination in linear logic? It was conjectured twenty years ago that it is the case with the model of sets and relations. This conjecture has finally been proved. This result shows in particular that we have a good notion of equality of proofs in linear logic. 2) If two proofs have the same Taylor expansion, are they equal? Furthermore, inspired by the closed relation between Taylor expansion and Krivine's machine, I will introduce a typing system allowing a static analysis of time complexity.
    • Bio: Daniel de Carvalho has a PhD degree in Mathematics from the University of Aix-Marseille-2, France. He worked as a lecturer and as a researcher in the Universities of Aix-Marseille-2, Paris-7, Paris-13, in the INRIA (the French National Institute for computer science and applied mathematics), in the Univerity of Roma-3 (Italy) and in the University of Copenhagen (Denmark). He currently works in Innopolis (Russia). His main research interests are: lambda-calculus, Linear Logic, Term Rewriting Systems, denotational semantics and computational complexity.
  • Dmitry Vlasov: Russell logical framework: proof language, usability and tools (Link to presentation.)
    • Abstract: When one develops a proof language, the following features are of the highest degree of importance: usability, reliability and flexibility. Language Russell was designed with these features put in the forefront. Different aspects of these features are discussed, and Russell system is compared with other popular formal math systems like Isabelle, HOL, Mizar, Metamath etc.
    • Bio: Dmitry Vlasov is a Candidate of Science (analog of PhD) in Mathematics, awarded by the Sobolev Institute of Mathematics, Novosibirsk, Russia. He works as a lecturer at the Novosibirsk State University (NSU) and as a researcher in the Sobolev Institute of Mathematics, Novosibirsk. Main research interests are: computer systems of formal mathematics, automated theorem proving, formal methods in software engineering, applied logic, model theory.
  • Nina Yevtushenko: Software testing: Finite State Machine based test derivation strategies (Link to presentation.)
    • Abstract: FSM based methods are widely used for deriving tests with guaranteed fault coverage for checking functional requirements for various types of digital / software systems including communication protocols. Given the specification machine and a fault domain, a complete test suite can be derived which detects any faulty implementation in the fault domain. Nowadays FSM based test derivation methods are extended with novel powerful methods for different FSM types. In this lecture, we present the main deterministic FSM based methods when the state number of an implementation FSM is limited and showcase corresponding experimental results. We also discuss how FSM based methods have been extended to deal with nondeterministic, possibly partial FSMs that are usually derived from functional system specifications and show how the adaptivity can help to derive shorter test suites. The complexity issues are considered for some techniques and we include a short case study for testing protocol implementations. We also briefly discuss how FSM extensions can be useful for checking not only functional but also non-functional requirements of a system under test.
    • Bio: Nina Yevtushenko received the degree "Doctor of Technical Sciences" and a professorship title from the Supreme Attestation Committee in Moscow. Up to 1991 she worked as a researcher with the Siberian Scientific Institute of Physics and Technology. From 1991 she has joined Tomsk State University as a professor and a leader of a research team working on the synthesis and analysis of discrete event systems. Presently she is a leading researcher at Ivannikov Institute for Systems Programming, RAS, Moscow. She stayed as a visiting researcher/professor at Moscow State University, Université de Montréal (Canada), University of Ottawa (Canada), Telecom SudParis (France), etc. She published more than 100 research papers and currently serves as a program committee member for a number of international workshops and conferences. Her research interests include formal methods, automata theory, distributed systems, protocol and software testing.

Memorial Session

We plan to organize a special session in memory of

Talk from Hosting Organization - JSC "Tenzor"

Vasily Kirnos: The threshold analysis of requests degradation in the computer network .
(Back to Top.)

Programme and Publication

 The final Workshop Programme is available..

All accepted papers are published in the preliminary proceedings by Yaroslavl State University, are indexed by RSCI (Russian Science Citation Index), and are available online at https://elibrary.ru/item.asp?id=35083182. Each research and memorial submission have been reviewed by 3 PC members, authors of accepted all accepted research and memorial papers will have a week to upgrade their submissions before submitting the version for the preliminary proceedings. Each short/poster/student submission will be reviewed by a PC member, authors of accepted papers of this kind will not have time to upgrade their papers and papers will be published in the preliminary proceeding in the original version.

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).

Registration, Accommodation, and Workshop Photos:

  • Registration dates and fees: free but had need a preliminary fill-in of a Google-form (for entering the workshop venue).
  • Accommodation: Park Inn by Radisson had been recommended as the first instance.
  • Some PSSV-2018 photos can be found by the following links:
(Back to Top.)

Sponsorship

Information hosting: IIS eng logo

Publication and organization: P. G. Demidov Yaroslavl State University Yaroslavl University logo

Hosting (venue) organization: JSC "Tensor" Tenzor rus logo

(Back to Top.)