Приглашенные доклады на конференции SYRCoSE'21 обещают быть интересными! Да и в основной программе можно найти что-нибудь по вкусу: http://syrcose.ispras.ru/?q=node/12 Чтобы получить Zoom-ссылку, надо зарегистрироваться. См. ниже.
Андрей Климов ---------- Forwarded message --------- From: Shilov Nikolay <shilov...@mail.ru> Date: Mon, 24 May 2021 at 13:14 Subject: Семинар ruSTEP: приглашение на 27-28 мая 2021 г. Уважаемые подписчики новостей о предстоящих заседаниях *ru-STEP* (=russian seminar on Software Engineering, Theory and Experimental Programming, https://persons.iis.nsk.su/ru/ruSTEP)! Приглашаем вас в предстоящие *четверг и пятницу 27 и 28 мая* 2021 г. на пленарные доклады XI SYRCoSE (Spring/Summer Young Researchers' Colloquium on Software Engineering, http://syrcose.ispras.ru/). SYRCoSE организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет). Во время XI SYRCoSE планируется три пленарных доклада: 1. *Дмитрий Александрович Мордвинов* (СПбГУ, JetBrains Research, Россия): *Property Directed Symbolic Execution* в четверг *27 мая 2021 г. с 10:00 до 11:00* (московского времени) - Symbolic execution is a popular technique for systematic exploration of program paths, with a wide range of applications, including unit test generation, security vulnerability detection, and program verification. In this talk, we'll briefly discuss the standard approaches in symbolic execution: state forking, path exploration strategies, function summarization and lazy instantiation. In the second part, we'll talk about the problem of directed symbolic execution: given a program, target program instruction and first-order formula, find program path reaching the target instruction, ending up in a state which satisfies the formula, or prove its absence. I'll present, step-by-step, some approaches we've developed during our current research project. In particular, we'll talk about the bidirectional symbolic execution, the efficient combination of forward and backward symbolic exploration. I'll present our implementation of this approach in our extension of klee symbolic virtual machine. Finally, we'll discuss the adaptation of recent breakthrough in hardware verification, the property-directed reachability approach, in the bidirectional symbolic execution engine. 2. *Антон Викторович Подкопаев* (Высшая Школа Экономики, JetBrains Research, Россия): *Programming Language Memory Models: Problems, Solutions, and Directions* в пятницу *28 мая с 9:30 до 10:30* (московского времени) - Due to compiler and hardware optimizations, modern programming languages (PLs) do not provide sequential consistent memory model SC, which guarantees that all concurrent behaviors of a program could be explained as a sequential execution of some interleaving of program's threads. Instead, they have weak memory models which allow more behaviors. Such memory models have to balance between performance and guarantees provided to software developers, or, as one may say, the balance is actually between performance and sanity. That is, performance forces a memory model to allow more optimizations and, therefore, more program behaviors, whereas sanity forces a memory model to provide guarantees like data-race-freedom (DRF) that a program without races has only sequentially consistent executions which restricts the set of allowed executions. In this talk, we introduce weak memory concurrency, consider requirements imposed on PL memory models, and examine ones used by industry C11 and Java and their drawbacks. Then, we explore new memory models RC11, MRD, Promising 1.0/2.0, Weakestmo proposed as a solution for the drawbacks: what these models provide, which compromises they take, how expensive performance-wise, if at all, these compromises are, and how hard is to adapt the models for mainstream languages. We conclude with a discussion on how to choose a memory model for your language or VM depending on your desiderata. 3. *Holger Schlingloff* (Fraunhofer FOKUS, Германия): *Formal Methods for Reliable Autonomous Systems* в пятницу *28 мая с 9:30 до 10:30* (московского времени) - A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, the more such systems take over safety-critical tasks, such as driving a car or flying a plane, the more important it becomes to establish the correctness and reliability of their behaviour. In this talk I survey what can be done as state-of-the-art in the specification and verification of autonomous behaviour, and propose challenges to researchers and engineers in this domain. The talk is based on the AAMAS'21 paper "Towards a Framework for Certification of Reliable Autonomous Systems", available at https://link.springer.com/article/10.1007/s10458-020-09487-2 С аннотациями докладов можно познакомиться пo ссылке http://syrcose.ispras.ru/?q=node/36. Пожалуйста зарегистрируйтесь на http://syrcose.ispras.ru/?q=node/26 для доступа к трансляции пленарных и других докладов SYRCoSE. Пожалуйста, распространяйте информацию о нашем семинаре среди ваших коллег, приглашайте их регистрироваться в https://forms.gle/earZy3hFJKmHQLoZ7.
