Artificial Intelligence (AI) is reshaping the landscape of many fields and software engineering is no exception. This talk provides an overview of the current state of AI applications in software engineering with potential benefits and challenges that come along. It focuses on AI-driven tools and techniques for code analysis, testing, debugging and quality assurance in general. The talk also highlights the challenges and opportunities in adopting AI for software engineering, such as improving developer productivity, reducing human errors and enhancing the overall software development process. Lastly, it discusses the potential future trends and implications of AI in the software engineering domain.

Konstantin Sorokin is a researcher at the Compiler Technology Department of ISP RAS. He graduated from Moscow State University from the faculty of Computational Mathematics and Cybernetics in 2018 (master's degree). He leads an R&D group that works on applications of AI to various software engineering tasks with focus on development of source code analysis and testing assistants for industrial partners (e.g. ISPRAS-Samsung joint laboratory). His research interests include compiler technologies, static and dynamic analysis, applications of AI/ML for enhancing productivity of software engineers and QA team members.

Formal specifications have been promoted by researchers for many years as a way to specify requirements and as a basis for creating high-quality software. However, developers are skeptical about the use of formal methods in general and formal specifications in particular. This report is devoted to the formal specifications of libraries and the experience of their application in real software engineering tasks. Cases of the use of formal specifications in tasks of unit test generation, static and dynamic analysis, integration of multi-component projects, test automation and program migration will be considered.

Vladimir Itsykson graduated from St. Petersburg Polytechnic University in 1996 with a degree in Informatics and Computer Engineering. In 2000, he defended his dissertation on the topic of modeling computer systems and began working as an associate professor in the department of computer systems and software technologies. Since 2015, head of the department, since 2019 - director of the Higher School of Intelligent Systems and Supercomputer Technologies. Since 2023, he has been working as a professor at the Institute of Applied Computer Science at ITMO University. Since 2000, head of the research laboratory “Verification and Program Analysis”.  In 2015, the laboratory became part of the Jetbrains Research group of laboratories.Under his leadership, more than 50 research projects have been completed, including collaboration with such companies as Panasonic, Intel, Jetbrains, Huawei. Areas of scientific interests: static program analysis, dynamic program analysis, software verification, formal specifications.

The secure software development life cycle involves the use of a number of technologies, the combined use of which will increase the security property of the software by reducing the number of errors contained in it. Among such technologies are static analysis of source and binary code, dynamic analysis and fuzzing. Also special compiler based defenses and obfuscation used to prevent exploitation the defects and errors, what not found and properly fixed, what lead to remain in the software after the release. In this presentation, a number of studies will be considered, affecting the mentioned topics, carried out in order to further develop the Crusher software package.

Shamil Kurmangaleev is a Leading Researcher at the Department of Compiler Engineering, ISP RAS. He is a Ph.D. (2013) from ISP RAS on optimization, portability and obfuscation of C/C++ programs. He leads a group that is working on developments in the field of static and dynamic program analysis. His research interests include compiler technologies, various applications of static and dynamic analysis, and methods for combining them.

Model-Based Approach is well-known technology for software analysis and design. However, the approach is not widespread in industry at the moment. Product line approach is actively used in development of hardware/software systems during last 30 years for many areas including telecommunication, avionics, etc. To provide configurability for reusable assets in product lines XML is used. However, it is very often inconvenient and leads to chaos. Instead of that DSLs might be used catching domain abstractions, reducing specification size and providing its correctness. Model-based approach can be integrated with DSLs in the context of product lines development supporting navigation features for DSL source code. The lecture will highlight details of this idea, outline some real-life project from telecommunication area, and present a discussion.

Dmitry Koznov received his M.Sc. in Software Engineering (1994), Ph.D. (2000) in Software Engineering Department from Saint-Petersburg State University. He has defended Doctor of Science thesis in 2016 and become a full professor at Saint-Petersburg State University. He has been a visiting professor at the NUS (Singapore 2000, 2002), the LUT (Finland, 2014), the SUSTech (Chine, 2018). Dmitry has taken part in a number of cooperation and industrial projects with software companies such as HP, JetBrains, Intel, etc. His research interests include: model-driven development, dsls, software engineering teaching technologies, telecommunications.

The steadily growing spectrum of various computer applications working on big and bigger data volumes have drastically changed the requirements for modern computer systems. Heterogeneous computing architectures are currently being widely accepted as the most promising solution for a wide range of systems scaling from datacentres down to battery operated embedded devices. In this talk we will introduce the architectural motivations and the choices for heterogeneous computing systems and will focus on their programmability challenges. Several widely adopted programming models and languages for heterogeneous computing will be outlined along with some typical technologies of heterogeneous computing. The complimentary but rather central role of data management, e.g., mapping, movement, access, static and dynamic management, will be discussed. Naturally, we will indicate the forthcoming challenges and open research questions related to the above.

Georgi Gaydadjiev received his M.Sc. (1996) in Electrical Engineering and Ph.D. (2007) in Computer Engineering from Delft University of Technology. He is currently a full professor in Innovative Computer Architectures at the University of Groningen and a honorary visiting professor at Imperial College. He holds three patents, co-authored more than 180 refereed scientific conference and journal articles and received three best paper awards. His research interests include: Computer (System) Architecture and Micro-architecture, Reconfigurable and Heterogeneous Computing, Distributed and Advanced Memory Systems, Design tools and Methodologies, Low-Power Architectures, Architectural Support for Compilers and Runtime Systems.

K-framework is a modern approach to programming language design, program analysis and verification. It allows to define an operational semantics of programming language in simple and intuitive way, and get a bunch of tools automatically: from interpreters to symbolic-execution engines and provers. One can define his own language in literally 15 minutes and start to program in this language, experiment, test, prove properties of programs in this language and so on. Currently K-framework is more and more widely used in industry: from block-chains to NASA aerospace programs. And it was proven by practice to be very effective tool for program verification, safety and security analysis. Also K-framework is very helpful in computer science courses that are aimed at language design and formal semantics.

Vasil Diadov is a leader of formal methods group in Kaspersky labs and lecturer in MIPT. Graduated in 2005 from National University of Electronic Technology. His work is focused on industrial application of formal methods  (in Kaspersky OS, in Huawei virtual machine, etc). His interests are in model-checking, model-finding, formal semantics, symbolic execution, program verification and matching logic.

The talk will be devoted to using deep learning methods and particularly Transformers for source code processing. We will discuss what applied tasks benefit from using neural networks, the high-level overview of the Transformer-based approaches, and what are the open problems and limitations of these approaches. We will pay specific attention to Transformer-based solutions because they often achieve state-of-the-art results in various applied tasks. As Transformers were initially developed for natural language processing, we will also discuss the ways of adapting Transformers to source code specifics and in which cases it is needed. The general goal of the talk is to give an introduction to the field and to provide understanding when neural network-based models may be useful in practice.

Nadezhda Chirkova is a research fellow at the Centre of Deep Learning and Bayesian methods of the HSE University. Her research is mainly focused on using deep learning models for source code and adapting neural network-based methods to source code specifics, and her works are publiched at top-tier machine learning conferences (NeurIPS, EMNLP, AAAI etc). At HSE, Nadezhda also teaches machine learning courses and is one of the main organizers of the international Deep|Bayes summer school.

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

Bernd-Holger Schlingloff is chief scientist at the Fraunhofer institute FOKUS and professor for software technology at the Humboldt University of Berlin. His main interests are specification, verification and testing of embedded safety-critical software. He obtained his Ph.D. from the Technical University of Munich in 1990 with a thesis on temporal logic of trees; after that, he worked on model checking of real-time systems at CMU. Subsequently, he was associate professor at the TU Munich and, from 1997 to 2001, managing director of the Bremen Institute for Safe Systems. His habilitation in 2001 was on partial state space analysis of safety-critical systems. Since 2002, when he joined Fraunhofer, he is managing industrial projects in the automotive, railway, and medical technology domain. His areas of expertise include quality assurance of embedded control software, model-based development and model checking, logical verification of requirements, software product lines, and automated software testing.

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.

Dmitry Mordvinov is the researcher in JetBrains Research and senior lecturer in Saint-Petersburg State University. He graduated in 2013 from Saint-Petersburg State University and got his Ph.D. in 2021 in A.P. Ershov Institute of Informatics Systems. From 2019, he leads the formal verification group in Programming Languages and Tools Lab in JetBrains Research. His work is focused on theory and practice of symbolic execution engines and automated inductive invariants inference. His research interests include software verification, symbolic execution, type theory and model theory.

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.

Anton Podkopaev is an associate professor at HSE University (St. Petersburg, Russia) and a research group leader at JetBrains Research. He was a postdoc at MPI-SWS and did his PhD at St. Petersburg University. Anton works on rigorous mathematical specifications and proofs for realistic concurrency systems including CPU architectures (e.g., x86, Arm, Power) and languages (e.g., C/C++, Java, JavaScript). His interests include proving compiler correctness, verifying of concurrent algorithms in weak memory models, mechanizing proofs in interactive theorem provers, functional programming.

Static analyzers for finding program defects have found their niche in the line of production tools improving program quality. A number of well-established commercial and open source projects exist and are widely used. But the related static analysis research is not drowsing because of that, and it produces many potentially far reaching techniques that improve the classical analysis methods as well as build upon them something completely new.  In this talk we will give a number of examples of such research that we are working on now and plan to explore in the near future within the Svace static analyzer collection.

Andrey Belevantsev is the leading researcher at the Compiler Technology Department of ISP RAS. He got his Dr.Sc. (2018) and Ph.D. (2008) from ISP RAS on the topics of static analysis and speculative compiler optimizations. He leads ISPRAS-Samsung joint laboratory that is focused on various system programming infrastructure projects such as static analysis and optimization tools for Android and Tizen environments. His research interests include compiler optimizations, toolchains improvement for productivity and performance, and various static analysis applications.

In my presentation, I will talk about the applied research conducted at Fraunhofer FOKUS in the field of formal verification. Our work is closely related with the Frama-C static analysis platform and was originally motivated to complement process-based quality assurance activities for safety-critical systems. Gradually, the focus of our work shifted to security-critical systems where, among others, we are using Frama-C to prove the absence of runtime errors in C code. We have also been engaged in the creation and maintenance  of "ACSL by Example" — an extensive collection of formally verified classic algorithms implemented in C. Finally, I will talk about our efforts to execute computationally expensive components of Frama-C as a cloud-based verification service.

Dr. Jens Gerlach is head of the Verification group at Fraunhofer FOKUS. He is also responsible for the business domain Railway at Fraunhofer FOKUS. Jens Gerlach studied at Humboldt University in Berlin and joined the institute in 1992. From 1996 to 1999 he was senior researcher of the Real World Computing Partnership in Tsukuba, Japan. After his return to Fraunhofer he worked as project leader of various industry and research projects. In 2002 he received his Ph.D. from TU Berlin on the subject of domain engineering and generic programming. The focus of his work is quality assurance projects for critical embedded systems. His area of research encompasses formal methods and static software analysis methods for such systems.

Being able to write good papers is an essential skill in academia, yet it is not an easy one to master for students and young developers. Software engineering being a highly practical area makes the task even more diffcult for them. Despite a tight connection between research and industrial activities, the two differ greatly from each other. The challenge here is to carry out research which would be relevant from both an academic and a practical point of view as well as to write high quality papers. The lecture is going to discuss some patterns of software engineering research presenting both good and bad examples. The organisation of a standard academic software engineering paper will be outlined and a number of typical errors made by young Russian researchers will be analysed.

Dmitry Koznov graduated with honours from St Petersburg State University (SPbSU), Faculty of Mathematics and Mechanics, in 1994. Between 1994 and 2000 he worked in various positions (developer, manager, department head) in a number of industrial companies in the area of creating software development tools. In 2000 Dmitry went back to SPbSU to enrol in a postgraduate programme. Upon completing the course and defending his thesis, he received a PhD degree in 2002. Since then he has been working at SPbSU first as an assistant professor (2002-2008), then an associate professor (2008-2017), and finally as a full professor (2017 till present). In 2016 he was awarded the degree of Doctor of Engineering. Dmitry has taken part in a number of R&D and industrial projects in the areas of model-driven development and software documentation. He functioned as a coordinator for the SPbSU representatives in international research projects within the Source-East Finland-Russia ENPI CBC Programme (2011-2013) and the Nordic Council of Ministers Programme (2010-2011). Dmitry has also been a supervisor of 6 research projects supported by the Russian Foundation for Basic Research (RFBR) and has won research and educational grants from Microsoft, Hewlett-Packard, Intel, the government of St Petersburg, etc. He has acted as an academic supervisor for 6 postgraduate students who have defended their PhD theses. His current areas of research are software documentation and near duplicate detection. Dmitry has been a visiting professor at the NUS (Singapore, 2002), the LUT (Finland, 2016), the SUSTech (Chine, 2018).

In this presentation, we focus on the design and the verification of critical real-time embedded systems. We provide an overview of verification capabilities that are proposed by the AADL, the real-time scheduling theory and tools implementing them. The AADL (Architecture Analysis and Design Language) is an SAE International Standard dedicated to the modeling of embedded real-time critical systems, covering both hardware and software concerns. AADL supports various kinds of analysis (scheduling, safety and reliability, ...) but also code generation. From a scheduling point of view, an AADL model is composed of threads communicating with each other and running on an abstracted hardware platform. Real-time scheduling theory is a set of methods which can be applied to predict the temporal behavior of the AADL threads. The presentation will be organized in two parts. First, we present the foundations of scheduling analysis theory for uniprocessor real-time systems and their modeling with AADL. Second, we introduce some of the current challenges this research community is addressing.

Frank Singhoff is Professor of Computer Science in the Lab-STICC laboratory, UMR CNRS 6285 and in the Computer Science Department at the Université de Bretagne Occidentale, France. He received his engineering degree in Computer Science from the CNAM/Paris in 1996 and his PhD from Télécom-Paris-Tech in 1999. His current research focuses on real-time scheduling analysis and architecture description languages on multi and many cores. In 2002, he started Cheddar, a toolset designed to perform analysis with the real-time scheduling theory. Frank Singhoff is also a member of the SAE AS-2C committee working on the AADL. He received an ACM SIGAda “Outstanding Ada Community Contributions Award” in 2010.

The life of the information system after its permanent operation is essentially just beginning. At the same time, not the developer of application software, but the owner of the system have problems ensuring its quality in continuous operation. Unfortunately, little publications has been devoted to this topic. The proposed report is one such work. The paper describes more than 12 years of experience in the organization and features of automated testing of the operating system: testing its functional integrity and destination indicators.

Boris Pozin is CTO in EC-leasing and professor in NSU HSE, the leading researcher in the field of software testing and software and systems engineering. Не has extensive experience in the field of system maintenance and creation of enabling systems for mission critical information systems. He is chair of SEMAT Russian Chapter, Co-Chairman of Program Committee of the international conference APSPE.

Many papers are devoted to static analysis algorithms and methods, however almost nothing was said about efforts needed for successful analyzer deployment. As we have seen in practice during implementation of the Svace static analyzer, many research problems have to be solved in order to get a really useful tool without end-user’s obstruction. This talk briefly discusses main challenges of defect detection tool development and deployment. We will examine all tiers of program analysis: from build phase integration to warnings presentation taking into account multiple programming languages (C, C++, C#, Java) special aspects. The first phase is responsible for build interception and makes it possible to inject special tools for gathering build environment specifics and running the tool's own compiler with corresponding parameters.  The second stage is responsible for analyzing intermediate representation generated by first phase, it is described in publications often but we still cover the most tricky points. And the last stage is needed for warning presentation using existing CI or our graphical interfaces.

Valery Ignatyev is the senior researcher at the Compiler Technology Department of ISP RAS. He has graduated from the Faculty of Computational Mathematics and Cybernetics of the Lomonosov Moscow State University with honor in 2009. In 2015 he defended his Ph.D. thesis on the «Program static analysis for automatic checking of configurable C and C++ programming language constraints». Since 2007 Valery Ignatyev has been working at the ISP RAS. The last 9 years he is working on compiler technology problems. His research interests include compiler technologies, program analysis.

Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. We present the current state-of-the-art in the field and we put it in context, looking at the history of software architecture and the reasons that led to the diffusion of objects and services first, and microservices later. Open problems and future challenges are introduced. This talk primarily addresses newcomers to the discipline, while offering an academic viewpoint on the topic. In addition, some practical issues are investigated and some potential solutions are pointed out.

Manuel Mazzara is a professor of Computer Science at Innopolis University (Russia) with research background in formal methods, software verification and software engineering. He has more than a decade of expertise in service-oriented architectures and programming, and with several publications in top venues coming from continuous cooperation with European and US industry, plus governmental/intergovernmental institutions, always at the edge between science and software production. He has got an understanding of the hot topics early enough in order to suggest directions for scientific deepening and market development, always aligned with ethical and societal considerations.

Modern cyberphysical systems are of increasing complexity, composed of an increasing number of components and subsystems of heterogenous nature, of different criticity levels and where different non-functional aspects – such as timing, energy, dependability and more and more also security – are as important as functionality. Current approaches use different models and corresponding tools for different viewpoints and guarantee overall correctness by means of strong assumptions. A more flexible contract-based approach would allow to relax some of these strong assumptions without abandoning the current modelling approach and the current tools.

Susanne Graf is a deputy director of VERIMAG, a joint research lunit of CNRS and Grenoble University. Her scientific domain of interest is methods and tools for developing correct software where she is particularly interested in the application domain of safety-critical embedded systems. In particular, she has worked on abstraction methods and on compositional approaches. Currently, her main interest is contract-based approaches and how to make them applicable to current industrial practice.

After many years of successful development of new algorithms for software model checking, there is a need to consolidate the knowledge about the different algorithms and approaches. This talk gives a coarse overview over four algorithms. We compare the following different "schools of thought" of algorithms: bounded model checking, k-induction, lazy predicate abstraction, and lazy abstraction with interpolants. Those algorithms are well-known and successful in software verification. They have in common that they are based on SMT solving as the back-end technology, using the theories of uninterpreted functions, bit vectors, and floats as underlying theory. All four algorithms are implemented in the verification framework CPAchecker. Thus, we can present an evaluation that really compares only the core algorithms, and keeps the design variables such as parser front end, SMT solver, used theory in SMT formulas, etc. constant. We evaluate the algorithms on a large set of verification tasks, and discuss the conclusions.

Dirk Beyer is Professor of Computer Science and has a Research Chair for Software Systems at the University of Passau, Germany. He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada, and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004) in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is the architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.

The talk presents experience in application of various verification techniques to operating systems. It includes deductive verification of Linux security modules, software model checking of Linux device drivers, static analysis to detect data races in operating system kernels, model-based testing for compliance to API standards like LSB and POSIX, systematic fault injection for run-time testing.

Alexey has graduated from Computer Sciences Department of the Lomonosov's Moscow State University with honour in 2001. He received a Ph.D. in Computer Sciences in 2006 on the Formal Specification and Testing of Asynchronous Systems. Alexey works for the Institute for System Programming of the Russian Academy of Sciences (ISPRAS) since 1999. His research interest includes formal methods for software and hardware systems, model based testing, verification of operating systems and design of safety critical embedded systems. Alexey was the lead architect of the LSB Infrastructure program run jointly by ISPRAS and Linux Foundation. He is a director of the Linux Verification Center of ISPRAS, where a number of verification techniques are developed and applied to Linux kernel and other real-time operating systems.

Automatic exploit generation demanded not only by Black-Hat hackers but benign developers too. Generation of workable exploit – is the best way to evaluate severity of found defect and set right priority to fix the bug. Over the past decade a lot of papers were presented to offer methods of automatic (or automated) exploit generation using only raw binary code. However, at the same time software protection mechanisms were significantly developed. They aimed to prevent exploitation or to mitigate its consequences. The talk compares exploitation techniques and protection mechanisms in the modern software, shows how secure software development utilizes advances in compiler technology.

Vartan Padaryan is the leading researcher at the Compiler technology Department of the Institute for System Programming of the Russian Academy of Sciences (ISP RAS). He has graduated from the faculty of Computational Mathematics and Cybernetics of the Lomonosov Moscow State University with honor in 2000. In 2005 he defended his Ph.D. thesis on the «Research and development of estimation methods for scalability and performance of data-parallel programs». He has published over 50 articles. Since 1997 Vartan Padaryan has been working at the ISP RAS. The last 9 years he is working on computer security problems. His research interests include compiler technologies, program analysis and reverse engineering, network security, parallel and distributed programming.

Deriving distributed implementations from global specifications has been extensively studied for various application domains, and under various assumptions and constraints. We explore here the problem from the knowledge perspective: a process can decide to execute a local action when it has the knowledge to do so. We discuss typical knowledge atoms, useful for expressing local enabling conditions with respect to different notions of correctness, as well as different means for obtaining knowledge and for representing it locally in an efficient manner. Our goal is to use such a knowledge-based representation of the distribution problem for either deriving distributed implementations automatically from global specifications on which some constraint is enforced -- a difficult problem -- or for improving the efficiency of existing protocols by exploiting local knowledge. We also argue that such a knowledge-based presentation helps achieving the necessary correctness proofs.

Standards are what most people in the industry have heard of, but little have seen. Languages suAbstarch as C and C++, programming interfaces like POSIX, networking like TCP or Web-Services, cryptography such as RSA and AES, development processes like change management and quality control... Almost everything around a coder is supported by standards. They are curtained by components, libraries and tools, but they are there. What are they - the standards? What are they for you? What can you do with them? And what can you do for them? The talk discusses the importance of knowing the standards, the pros and conses of following and breaking the standards, and the ways you can contribute to them.

Distributed system is a group of decentralized interacting executers. Communication in a distributed system is said to be fair, if any executer that wants to communicate with another one will eventually communicate. Distributed algorithm is the communication protocol implementing a distributed system to solve some task. Multiagent system is a distributed system that consists of agents. An agentis an autonomous rational reactive object (in Object Oriented sense) whose internal state can be characterized in terms of agent's believes, desires, intentions, and rationale. Multiagent algorithm is a distributed algorithm that solves some problem by means of cooperative work of agents. But in an individual agent’s perspective a multigent algorithm is a reactive and proactive knowledge/believe-based rational algorithm to achieve agent’s own desires. Agent's beliefs represent its “knowledge” about itself, other agents and an “environment”; this “knowledge” may be incomplete, inconsistent, and (even) incorrect; beliefs evolve in reaction to “signal” that it gets from the environment (i.e. agents are reactive). Agent's desires represent its long-term aims, obligations and purposes (that may be controversial); usually desires don’t change on the run ofmultiagent algorithm. Agent's intentions are used for a short-term planning; this ability to make and change short-term plans is calledagent’s proactivety. A rational agent has clear “preferences” (rationale) and always chooses the action (in feasible actions) that leads to the “best” outcome for itself. Every agent is autonomous, i.e. any change of its believes, desires and intentions depends on the agent itself, and a change can’t be decreed from outside.In the talk we examine (from epistemic point of view) knowledge and beliefs of agents that arrive one by one to a resource center to rent for a while one of available desired resources. Available resources are passive, they form a cloud; each of the available resources is lend on demand if there is no races for this resource and returns to the cloud after use. Agents also form a cloud, but leave the cloud immediately when they rent a desired resource. All agents are rational and can communicate with each other in P2P-manner, negotiate and flip (change intentions) so that all flips must always be rational for participating agents. The problem is to design a multiagent algorithm, which allows each arriving agent sooner or later to rent some of desired resource.

One of the core practical problems in proving the correctness of programs is to take care of specifying and verifying properties that do not change: the so-called frame properties. Because frame properties are tedious to write, mechanical assistance is necessary. I will present a general convention for specifying frame properties and a framework (developed with A. Kogtenkov) to infer them automatically, based on the “alias calculus”.

AddressSanitizer (ASan) is a tool that finds buffer overflows (in stack, heap and globals) and use-after-free bugs in C/C++ programs. ThreadSanitizer (TSan) finds data races in C/C++ and Go programs. MemorySanitizer (MSan) is a work-in-progress tool that finds uses of uninitialized memory (C++). These tools are based on compiler instrumentation (LLVM and GCC), which makes them very fast (e.g. ASan incurs just 2x slowdown). In this talk we will share our experience in huge scale testing using these tools and discuss new related research areas.

Despite of the fact that there are myriads of well-meaning ways of using digital devices and Internet, the world, unfortunately, does not consist exclusively of decent people. More crimes are getting turned to the virtual world, while computers and Internet are becoming instruments of committing crimes. It is quite natural that countermeasures appear, and, moreover, there is an entire branch of science, called digital forensics, devoted to investigation of crimes committed online or with the use of digital devices. In contrast to usual data examination, forensic data analysis is covered by strict legislation, and, therefore, digital forensic software should be special. As the niche is rather narrow, there are not many companies in the world that deliver solutions to the digital investigation market. One of them is the Russian company “Belkasoft”.

The increasing utilization of embedded software in application domains such as automotive, aerospace or railway has resulted in a staggering complexity that has proven difficult to negotiate with conventional design approaches and processes. In addition, more and more projects need to comply with functional safety standards such as ISO 26262, DO-178C, or EN 50128 because modern software-based applications increasingly control or interact with mission-critical or safety related system components. Development approaches and processes play a decisive role in addressing the complexity, productivity, and quality challenges. Because of its ability to address these challenges, Model-Based Design has been extensively used in various application domains. More recently, companies have begun to consider and adopt Model-Based Design for the development of embedded software for high-integrity applications.

We argue that the main challenges to be overcome in developing future generations of IT-enabled products and services lie not so much in the software engineering discipline itself as in the collaborative relationships that software engineers have with other disciplines. We briefly review the need for more emphasis on multi-disciplinary approaches and consider three classes of demanding system: embedded products, systems-of-systems and cyber-physical systems. In each of these areas, we argue that there is a need for engineering with formal semantic bases that enable joint modelling, analysis and simulation of groups of heterogeneous models.

Qualitative evaluation and comparison of changes of indications of objects having different nature is used by designers, managers, people making decisions (PMD) and experts to make the decisions more reasonable. For support of such activity on the analysis of changes of data connected with certain dates and time intervals, models of fuzzy time series are applied. In this article a model of fuzzy tendency the carrier of which is a fuzzy time series and its variety — elementary tendency model — is offered. The offered models are applied for solution of the problem of summarization of fuzzy time series in terms of tendencies.

Optimal scheduling of loading, warehousing and delivering of goods, picking up and transporting passengers, allocating drivers, pilots, crew members or service engineers to tasks, and ensuring that capacities match demands, is difficult and often impossible to achieve when demand is unpredictable and the operation is frequently interrupted by changes in orders, delays, bad weather, no-shows or resource failures. Real-time schedulers, which can rapidly react to every disruptive event and re-schedule affected resources before the next disruptive event occurs, are the answer. The talk will discuss how Multi-Agent Technologies (MAT) can help in dynamic scheduling and other complex problems, like optimization, pattern discovery, text understanding, etc.

Taming complexity by building models is one of the oldest and best established engineering principles. In Software Engineering this is complicated by the inherent typically high degree of abstraction, that easily leads to misunderstandings already at requirement analysis time. Additionally, taking care of heterogeneity leads within the modern model driven development approaches to a variety of aspect- and phase-specific models, whose interplay can be hardly overseen even by experts. Here is where the `eXtreme Model Driven Design? (XMDD) strikes, with a coherent and user-oriented modeling approach. The backbone of the entire Software/System lifecycle is a behavioural model accessible to the users (typically, application experts with little IT background). This model is on one hand selectively refined until the IT experts can proceed with a simple service-oriented implementation, but on the other hand it serves the application expert as a continuously available and up-to-date 'sensor', control- and validation instrument. This way, harmony between the Application expert and the IT side is established and coherently maintained, with high benefits especially in application domains with high evolution needs. The potential of this approach has been proven not only in scenarios from the business- and bioinformatics, but also in its successful use in distributed, cooperative project-based teaching.

This session will give you an overview of what cloud computing is and what cloud platform-as-a-service such as Windows Azure Platform can be used for in creating solutions for the real world scenarios. You will learn about all major components of Windows Azure Platform and how they work with each other in massively scalable architecture. You will find out what others around the world are building in the cloud, what issues they are encountering and how these issues are getting resolved.

The talk provides a review of recent advances in hybrid verification techniques, such as model based testing, extended static analysis, runtime verification, and compound structured testing, and focuses on improvements of tools supporting these approaches. The review shows that along with implementation of new techniques like counterexample-guided abstraction refinement or directed structured test generation based on constraint resolution, modern verification tools also develop to be more modular and tend to use more things as modules from other tools. Thus implementation of integrated verification methods applying a variety of techniques recently available only in research prototypes becomes reachable in industrial software development tools.