Program
Day 1. April 24, 2018 (Room 259, NURE)
09:00-09:30 Opening
9:30-10:30 Session 1
09:30-10:30
Sergiy Bogomolov, Australian National University, Australia
Verification and Planning for Machine Learning Algorithms and Vice Versa
11:00-13:00 Session 2
11:00-12:00
Mykola Nikitchenko, Taras Shevchenko National University of Kyiv
Logic and Program Verification
12:00-13:00 Invited talk
Leonid Lyubchyk, National Technical University “Kharkiv Polytechnic Institute”
Problems and methods of constantly acting unmeasured disturbances rejection in control systems
14:30-16:30 Session 3
14:30-15:30
Vyacheslav Kharchenko, National Aerospace University “Kharkiv Aviation Institute”
X Injection Based Verification of Software and Programmable Systems: Theoretical Issues and Industrial Cases
15:30-16:30
Grygoriy Zholtkevych, V.N. Karazin Kharkiv National University
Time in Distributed Systems
Day 2. April 25, 2018 (Room 259, NURE)
9:00-11:00 Session 1
9:00-9:30 Poster session
9:30-10:30
Andrii Babii, Kharkiv National University of Radio Electronics
Kubernetes and Docker. Machine learning environment setup
10:30-11:00 Poster session
11:00-13:00 Session 2
11:00-12:00 Invited talk
Artem Chernodub, Clikque Technology and Ukrainian Catholic University
New Trends in Neural Networks: Generative Models
12:00-13:00 Invited talk
Ievgen Gorovy, It-Jim and Institute of Radio Astronomy
Computer vision: practical applications
14:30-15:30 Session 3
14:30-15:30
Oleksii Turuta, Kharkiv National University of Radio Electronics
Computer Vision for safe systems
Detail information about talks
Verification and Planning for Machine Learning Algorithms and Vice Versa
Abstract: Cyber-physical systems (CPS) are networks of physical and digital components and present a next generation of large-scale highly-interconnected networked embedded systems. On the one hand, CPS open enormous opportunities as they form the core of emerging smart devices and services which are going to revolutionize many traditional industries such as automotive, traffic management, power generation and delivery, as well as manufacturing. On the other hand, highly autonomous systems pose special engineering challenges as any unexpected behaviour might lead to large financial losses or even human deaths.
In this talk, we address this challenge and propose automatic techniques to analyze CPS. For this purpose, we use the concept of hybrid automata which has proven to be particularly useful to model CPS. We give an overview of techniques to ensure efficient analysis of hybrid automata. In addition, we discuss the connection between verification and hybrid planning, and use the automotive domain to showcase benefits their interplay can result at. Finally, we look at the synergies between verification/AI planning and machine learning communities and ways to exploit them.
Bio: Sergiy Bogomolov is a Lecturer / Assistant Professor at the Australian National University. Prior to joining ANU Sergiy was a Postdoctoral Researcher in the Institute of Science and Technology Austria. Sergiy is broadly interested in algorithms and techniques to support design and development workflow of trustworthy and resilient autonomous systems. For this purpose, he uses and develops techniques on the interface of cyber-physical systems verification and AI planning. His Ph.D. and M.Sc. degrees are from the University of Freiburg, Germany.
X-Injection Based Verification of Software and Programmable Systems: Theoretical Issues and Industrial Cases
Abstract: In this presentation, we discuss KhAI R&D team’s experience with the development and application of verification techniques for safety and security critical SW and FPGA based systems. Key of them are techniques based on Failure/Intrusion Modes Effects (Criticality) Analysis and Fault/Vulnerability Injection Testing (FME(C)A, FIT). These techniques are based on requirements and project analysis and aim to assess: (1) test coverage/quality of test cases; (2) trustworthiness on-line testing: indicators of fault and intrusion tolerance of developed systems. One of the most complex and interesting problems is development of multi-fault injection procedure to minimize time and assure the required safety. A few industry cases connected with development and verification of FPGA-based platform for critical application (NPP I&Cs and others) are discussed.
Bio: DrS, Professor Vyacheslav Kharchenko is Head of the Computer Systems, Networks and Cyber Security Department, National Aerospace University KhAI, Kharkiv, and Head of Centre for Safety Infrastructure Oriented Research and Analysis, PRC Radiy, Kropyvnytskyi, Ukraine. Vyacheslav and CSNC Department R&D team investigate and implement the techniques and tools for assessment, certification and development dependable applications for high available, safety critical and business critical domains.
Logic and Program Verification
Abstract: The aim of this talk is to acquaint attendees with the primary models of program semantics; to present logics based on formal program models; to discuss applicability of program logics in program analysis and verification. Program verification is a grateful area of logic application. To be successful, logics for program verification should be based on formal program models. We use denotational semantics to construct formal program models. Then we describe various classes of mappings representing program semantics such as n-ary mappings, mappings with non-fixed arity (quasiary mappings), and mappings over hierarchical data. We demonstrate that these classes have different properties that affect program construction and investigation. We construct various logics based on the described classes of mappings and demonstrate that each logic has specific features which are not characteristic for classical logic based on n-ary mappings. At last, we investigate classical Floyd-Hoare logic, logics with partial predicates and functions, logics over hierarchical data. Such analysis demonstrates that even in a case of simple programs we have to introduce new rather complicated consequence relations and new rules of calculi. In conclusion, we formulate the main challenging problems of program logics construction and program verification.
Bio: Mykola Nikitchenko is a professor of Faculty of Computer Science and Cybernetics of Taras Shevchenko National University of Kyiv. His scientific interests are foundations of computer science (informatics) and programming, mathematical logic, formal methods of software system development, abstract computability. He is the (co)author of 10 monographs/handbooks/textbooks, 50 works indexed by SCOPUS, 200 works indexed by Google Scholar.
Problems and methods of constantly acting unmeasured disturbances rejection in control systems
Abstract: The problem of unmeasured disturbances rejection in control systems is considered. The classical methods of disturbances attenuation based on LQG and H optimization methods and modern approaches to disturbances rejection using model-based control and invariant ellipsoid methods are analyzed and compared. The structural methods of synthesis based on the theory of disturbance observers with the internal predictive and inverse model are considered. A general approach is presented for the disturbance observers and compensators design on the basis of the theory of invariant observers and inverse dynamical models, the conditions for problem solvability and the achievable degree of disturbance suppression are analyzed.
Bio: Dr. Leonid Lyubchyk is a Professor and Head of Computer Mathematics and Data Analysis Department in National Technical University “Kharkiv Polytechnic Institute”, Ukraine. His field of scientific interests is control theory with a focus in robust control and control under disturbances, as well as machine learning in control.
New Trends in Neural Networks: Generative Models
Abstract: This presentation is dedicated to the new rapidly growing area in Artificial Neural Networks, namely, Generative Models. This kind of neural networks can be used for generation of artificial data samples, which can hardly be distinguished from the real ones. For example, it is possible to generate very natural faces or voice samples of never existed people. We discuss the difference between discriminative and generative models and briefly consider the most popular generative neural architectures including Generative Adversarial Networks (GANs), Variational Autoencoders (VAE), Recurrent Neural Networks (RNN). We focus our main interest on GANs and provide the detailed explanation of their design and working principles. We show the problems and limitations of GANs such as non-stable convergence and mode-collapse and discuss the directions of the future evolution.
Bio: Dr Artem Chernodub holds the position of Chief Scientist in Clikque Technology (Santa-Monica, USA) and lecturing in Ukrainian Catholic University (Lviv, Ukraine). Artem is interested in algorithms of machine learning, computer vision, natural language processing and neural networks.
Computer vision: practical applications
Abstract: 
In this presentation, we will overview computer vision (CV) applications in several fields including intelligent transportation, biometrics, remote sensing, robotics and entertainment. We will give several examples of how CV can successfully solve various weak artificial intelligence (AI) problems. A special attention will be given to usage of CV in augmented reality (AR) field. We will consider practical use cases and discuss theoretical details of this technology. In particular, we will describe what computer vision algorithms are utilized for mobile camera tracking, image retrieval, object detection, tracking and recognition. Performance of real custom AR system will be demonstrated and comprehensively discussed. Moreover, several real-life demos will be shown.
Bio: Dr Ievgen Gorovyi is senior researcher at the Microwave department in Institute of Radio Astronomy. Also he is a founder and CEO of It-Jim. The company is focused on signal and image processing, computer vision and machine learning applications. Ievgen is co-author of more than 40 publications, owner of several prizes for the best presentations at international conferences. In addition, he manages computer vision team in his company.
Computer Vision for safe systems
Abstract: In this presentation, we discuss our experiences with the application of machine learning techniques and particularly neural networks in order to build safe systems
Bio: Dr Oleksii Turuta is an associate professor at the Department of Software Engineering in the Kharkiv National University of Radioelectronics, Ukraine. Oleksii is interested in algorithms of machine learning, computer vision, natural language processing.
Organizers
Sergiy Bogomolov (Australian National University, Australia)
Andriy Yerokhin (NURE, Ukraine)
Oleksii Turuta (NURE, Ukraine)