The Workshop on Program Semantics, Specification and Verification


The Workshop on Program Semantics, Specification and Verification: Theory and Applications (PSSV 2010) affiliated with 5th International Computer Science Symposium in Russia (CSR-2010, June 16-20, 2010) will be held on June 14-15, 2010 in Kazan, Russia.

Scope and Topics

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 specification of programs and systems;
  • logics for formal specification and verification;
  • deductive program verification;
  • model checking of programs and systems;
  • formal approach to testing and validation;
  • software verification tools.

Accepted Papers and Program

List of Accepted Papers can be found here.
A preliminary program: English, Russian.

Official Languages

English and Russian

Accomodation

For information about hotels with special rates see Accomodation page.
Dormitory of Kazan State University is also available.

Program Chairs

Valery Nepomniaschy (Institute of Informatics Systems, Novosibirsk, Russia, vnep@iis.nsk.su)
Valery Sokolov (Yaroslavl State University, Yaroslavl, Russia, sokolov@uniyar.ac.ru)

Program Committee

Natasha Alechina (University of Nottingham, UK)
Boris Konev (University of Liverpool, UK)
Victor Kuliamin (Institute for System Programming, Moscow, Russia)
Vsevolod Kotlyarov (St. Petersburg State Polytechnic University, Russia)
Nikolay V. Shilov (Institute of Informatics Systems, Novosibirsk, Russia)
Natalia Sidorova (Techn. University Eindhoven, Netherlands)
Vladimir Zakharov (Moscow State University, Russia)

Submission and Publication

Program committee plans to have contributed talks and posters presentations. Program Committee invites submissions in the form of extended abstracts with length up to 6 pages A4 in 12 pt font with line-spacing 1.5 intervals (in English or in Russian). Additional details may be included in an appendix up to 4 pages for Program Committee. Submissions should be in PDF format. They should be sent (as attachments) by e-mail to Alexei Promsky (Inst. of Informatics Systems, Novosibirsk, Russia) promsky@iis.nsk.su and their abstracts should be sent (as attachments) to PSSV Chairs. The confirmation will be send during 3 days. All accepted papers will be published in the preliminary proceedings before the workshop and the volume of the proceedings will be distributed at the workshop. Selected papers will be published after the workshop in one of Russian peer-review journals. At least one author of every accepted paper should present a talk in the workshop.


Preliminary Program

Monday, June 14
08:30 - 09:45 Registration
09:45 - 10:00 Opening of
the Workshop
Session 1
10:00  - 10:30  Bashkin V.A. On the use of single-periodic bases for global symbolic verification
10:30  - 11:00 Bashkin V.A.,
Lomazova I.A.		 Two-level modeling of multiagent systems based on the generalized nets of active resources
11:00 - 11:30  Valiev M.K.,
Dekhtyar M.I.		 Complexity of verification of nondeterministic probabilistic multi-agent systems
11:30 - 12:00  Kuzmin E.V.,
Sokolov V.A.,
Chalyy D.J.		 On languages of automaton counter machines
12:00 - 14:00 Lunch
Session 2
14:00 - 14:30 Konnov I.V. Using adaptive symmetry reduction for LTL model checking
14:30 - 15:00 Garanina N.O. Model Checking of Distributed Systems with Affine Data Structures
15:00 - 15:30 Podlovchenko R.I. A technique for generating systems of equivalent transformations complete in various models of computations and its application to algebraic models of programs
15:30  - 16:00 Coffee Break
Session 3
16:00 - 17:30 Posters presentations  Anikeev M., Madlener F., Schlosser A., Huss S.A., Walther C. Viable Approach to Machine-Checked Correctness Proof of Algorithm Variants in Elliptic Curve Cryptography
Belyaev A.B. Verification the algorithm of transactional memory
Davydov A.V.,
Larionov A.A.		 On the calculus of positive-constructed formulas for the automated theorem proving
Kalentyev A.A.,
Tyugashev A.A.,
Shulyndin A.V.		 Formal verification of the real-time control algorithm’s specifications
Klebanov A.A.,
Stepanov O.G.,
Shalyto A.A.		 On the Formal Specification And Verification of Automata-based Programs via Specification Patterns
Klepinin A.V.,
Melentyev A.A.		 Integration of semantic verification into Java compilers
Malshakov G.V. Verification of integration of subsystems automation for higher education institution
Fedotov V.N. Service-oriented approach to integration testing in distributed systems
Shelekhov V.I. Verification and synthesis of addition programs under the rules of statement correctness
Shilov N.V. Experiment with a verifying compiler F@BOOL@

Tuesday, June 15
Session 4
10:00  - 10:30  Letichevsky A.A., Letychevskyi O.A.,
Weigert T. 		Predicate transformers for symbolic verification
10:30  - 11:00 Kotlyarov V.P.,
Drobintsev P.D.		 The technology of quality software development based on integration of verification and testing
11:00 - 11:30  Nepomniashy V.A., Anureev I.S., Atuchin M.M., Maryasov I.V., Petrov A.A., Promsky A.V. SPECTRUM-2: the System of C program analysis and verification
11:30 - 12:00  Shoshmina I.V.,
Karpov Y.G.		 Technology for distributed embedded systems design and verification
12:00 - 14:00 Lunch
Session 5
14:00 - 14:30 Bataev A.V.,
Davydov A.A.,
Nalutin N.Y., Sinitsyn S.V.		 Test data generation method based on formal specifications
14:30 - 15:00 Burdonov I.B.,
Kosachev A.S.		 Simulation of systems with refusals and destruction
15:00 - 15:30 Burdonov I.B.,
Kosachev A.S.		 Safe simulation testing
15:30  - 16:00 Coffee Break
Session 6
16:00 - 17:30 Panel Discussion Actual problems of program verification. From theory to applications.