Program of 7th Workshop on Program Semantics, Specification and Verification: Theory and Applications

14 June 2016

Time slot
Session 1 Chair: V. Sokolov
10:00–11:00 Dmitry Nadezhin. Theorem proving with ACL2 for industry artifacts
11:00–11:30 Irina Shoshmina. Developing formal requirements to distributed program system behaviour
11:30–12:00 Coffee-Break
12:00–12:30 N. 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
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
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

15 June 2016

Time slot
Session 3
10:00-11:00 Igor Konnov. Model Checking of Threshold-based Fault-tolerant Distributed Algorithms
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
Session 4 Chair: V. Itsykson
14:30–15:30 Bertrand Meyer. Verification of OO programs: the toughest open issues
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