We invite you to participate in the Ivannikov ISP RAS Open Conference, which will take place on December 5-6, 2019 in the main building of the Russian Academy of Sciences, Moscow, Russia: Moscow, Leninskiy prospekt, 32A.
The Open Conference is organized with support of:
To participate in the Ivannikov ISP RAS Conference please register. To present your research please submit a paper, that wasn't yet published or submitted for other conferences.
We accept original unpublished articles containing the results of research or describing the work in progress. We invite both researchers and practitioners. All accepted papers will be published in the Proceedings of Ivannikov ISP RAS Open Conference, that is indexed in Web of Science and Scopus. The proceedings will be published online in IEEE Xplore digital library.
Submission Guidelines are here.
Paticipation in the conference and publication of articles are free of charge. Travel and accommodation, as well as other expenses are to be paid by the participant.
The Ivannikov ISP RAS Open Conference is an annual event organized by the Institute for system programming of the Russian Academy of Sciences (ISP RAS) to discuss fundamental achievements in computer science and to present its new innovative technologies developed for practical commercial use in various industrial projects.
The main goal is to support the innovation ecosystem, created in ISP RAS for successful development of IT-technologies and their use in education, science and industry.
Every year the Conference unites acknowledged researchers from scientific and educational organizations and representatives of leading IT and other companies.
The section is devoted to optimization methods in compiler and code generation, static and dynamic program analysis, etc. The topics include:
The section is devoted to data management and data analysis (methods and systems for storing and analyzing large volumes of text, graph, multimedia, scientific and other types of data). The topics include:
The section is devoted to the use of open source software in solving continuum mechanics problems (OpenFOAM, Salome, ParaView, DAKOTA etc.) and comparison of developed software with commercial programs. The topics include:
1 Science Department at the Technion, Israel Institute of Technology, Israel
1Head of Global Public Policy and Government Relations, New-York, USA, 2 Machine Learning Engineer, Google, Google Cloud
1 Core Software Engineer (Distributed Systems) at Hazelcast
1 SINP MSU
1 NRC "Kurchatov Institute"
1 Petrozavodsk State University, 2 Institute of Applied Mathematical Research, KarRC RAS
1 NCFU
1 HSE
1 Corresponding member of RAS, Doctor of Science, Head of Chair of Informatics, MIPT, 2 Ph.D., Deputy Director of Applied Geophysics Lab, MIPT
1 Czech Technical University in Prague and Institute of Mathematics.
1 Professor at Toulon University, research director at Mediterranean Institute of Oceanography (M.I.O) Université Toulon
1 Keldysh Institute of Applied Mathematics, RAS
1 IBRAE RAS
1 FITS IU RAS, 2 Institute of Oceanology P.P. Shirshova
1 Institute of Oceanology P.P. Shirshova, 2 Keldysh Institute of Applied Mathematics, RAS, 3 MSU, Faculty of Computational Mathematics and Cybernetics
1 ISP RAS
1 Keldysh Institute of Applied Mathematics, RAS, 2 ISP RAS
1 Principal Researcher at Microsoft Research, Redmond, USA
1 Samsung Research
1 Languages and Frameworks Head, Huawei Russian Research Institute, St. Petersburg
1 Head Engineer, Huawei R&D Center, 2 TechLead, Huawei R&D Center
1 ISP RAS
1 Belarusian State University of Informatics and Radioelectronics
1 ISP RAS
Anxiety is a framework for finding errors and potential vulnerabilities during software development, QA, and deployment phases. It is based on dynamic symbolic execution, which allows generating input data for the issues found without source code or debugging information present in the binary. Anxiety can be used for adhering to the GOST R 56939-2016 requirements.
AstraVer Toolset is a deductive verification system for key software components. It allows developing and verifying security policy models as well as proving the correctness of software modules written in the C programming language. AstraVer is essential for ensuring the required trust levels from ADV_SPM and ADV_FSP assurance families as defined in the ISO 15408 standard.
BINSIDE is a static program analysis tool for finding defects in binary code. It is useful when checking programs without source code, such as closed source 3rd party libraries, as well as assisting with required static information to dynamic analysis tools.
Constructivity 4D is a technology for creating innovative software services that is capable of processing highly dynamic scenes and vast arrays of spatial and temporal data. It performs visual analysis of millions of objects with individual geometry and dynamic behavior. Constructivity is deployed within the Synchro system that is used for 4D modeling of extremely large construction sites.
DIGITEF is a software system based on OpenFOAM and other open source tools, as well as unique libraries developed at ISP RAS. DigiTEF solves various application problems of gas dynamics, aerodynamics, hydrodynamics, and acoustics. It is tailored for creating and working with highly sophisticated digital models of industrial devices. DigiTEF is included in the Unified Register of Russian Programs (№ 5377).
TRAWL is a unique production level tool for analyzing various binary code features that supports multiple target processor architectures. It does not require debug information or source code. Trawl can be used to analyze all kinds of software ranging from boot loaders to OS kernels and user level applications. It is included in the Unified Register of Russian Programs (№ 5323).
ISP FUZZER is a tool for performing dynamic program analysis based on the fuzzing approach. It can detect errors, backdoors, and vulnerabilities either with or without access to the program’s source code. ISP Fuzzer allows organizing a development process that adheres to the GOST R 56939-2016 requirements.
Klever is a framework for checking models extracted from the source code of large software systems developed in the C programming language. Klever provides means for automatic checking of a variety of security, robustness, and performance requirements.
Lingvodoc is a system intended for collaborative multi-user documentation of endangered languages, creating multi-layered dictionaries and performing scientific work with the received sound and text data. It is a result of a joint project with the Institute of Linguistics of the Russian Academy of Sciences and Tomsk State University. Lingvodoc is under active development since 2012 and can be found on lingvodoc.ispras.ru.
MASIW is a toolset for developing highly reliable hardware and software systems for avionics, medicine, and other safety critical areas. It is designed for engineers creating airborne hardware– software systems that are developed using the integrated modular avionics (IMA) approach. MASIW can be easily adapted for other application areas.
MicroTESK is an industry-targeted framework for generating test programs in the assembly language for functional verification of microprocessors. It includes the modeling framework (building microprocessors models based on formal specifications) and the generation framework (building test programs based on test templates).
Protosphere is a system of deep packet inspection (DPI). It is the part of intrusion and information leak protection systems. Protosphere detects inconsistencies between a protocol specification and a specific implementation. It allows to add support quickly for new protocols (either open or closed) due to the flexibility of its internal representation.
Retrascope is a functional verification toolkit for digital hardware designs. Retrascope provides automated engines for code analysis, formal model extraction and functional test generation. The toolkit accepts as inputs digital hardware module descriptions, written on the synthesizable subset of Verilog and VHDL languages, as well as their behavioral specifications.
SciNoon is a system for collaborative exploration of scientific papers. This software is essential for a group of researchers to dive quickly into the new area of knowledge and to find answers on their questions, following up with tracking new research on the topic of interest with highly customizable alerts.
SVACE is an essential tool of the secure software development life cycle, the main static analyzer that is used in Samsung Corp. It detects more than 50 critical error types as well as hundreds of coding issues. Svace supports C, C++, C#, and Java. Support for Kotlin and Go programming languages is in progress and is planned for Q4 of 2020. Svace is included in the Unified Register of Russian Programs (№ 4047).
Texterra is a scalable platform for extracting semantics from text. It contains the complete set of technologies for creating multifunctional applications for text analysis. Texterra bases its semantic analysis approach in the concept identification. It is included in the Unified Register of Russian Programs (№ 4048).
ISP Obfuscator is a set of technologies to prevent mass exploitation of vulnerabilities resulting from errors or backdoors. When a hacker is capable of attacking one of the devices that has a certain software installed, the rest will remain protected by changes made by the tool to the software code.
The software and performing complex, resource-intensive calculations using both containers and virtual machines. They are designed especially for the deployment of cloud environments.
Talisman is a framework for data analysis that is designed for retrieving people, community, and company data. It utilizes modern approaches for machine learning, computer linguistics, complex network analysis and big data processing. Talisman is capable of finding relations and their patterns by analyzing large graphs consisting of hundreds of millions of nodes.
ISP RAS Foundation Platform for creating program analysis systems is built on top of open source QEMU emulator. The software is essential for organizing multi and cross platform development. It also supports reverse debugging and introspection features, as well as the full system emulation mode for debugging low-level software.
Method for automatic recognition and classification of 12-lead ECG.
Early prediction of retinal organoid differentiation using neural networks.
1 Brookhaven National Laboratory, Upton, USA, 2 Professor, Universidad Andrés Bello, Santiago, Chile
1 UNAB, ISP RAS
1 UNAB, ISP RAS
1 ISP RAS
1 ISP RAS
1 Skolkovo Institute of Science and Technology
1 HSE, 2 Department of Product Innovation and Development of IB Group LLC, 3 BMSTU
1 Vyatka State University
1 Federal Research Center "Computer Science and Control" of RAS
1 University of Latvia
1 ISP RAS
1 Dorodnicyn Computing Centre, RAS
1 Prof. Dr.-Ing., The University of Luxembourg
1 Professor, Aix-Marseille University
1 Chalmers University of Technology, Gothenburg, Sweden
1 SPbPU, 2 STR Group, Inc.
1 ISP RAS
1 ISP RAS
1 Kazan Federal University
1 ISP RAS
1 ISP RAS, 2 Bauman Moscow State Technical University, 3 Keldysh Institute of Applied Mathematics, RAS
1 ISP RAS
1 Norwegian University of Science and Technology, Trondheim, Norway
1 Institute of Hydrodynamics M.A. Lavrentieva SB RAS
1 Bauman Moscow State Technical University
1 MSU, 2 ISP RAS
1 Principal Researcher at Microsoft Research, Redmond, USA
Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet, there are many applications where satisfiability, and optionally a model or a proof, is insufficient. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. The tutorial describes, in an interactive way using jupyter notebooks, logical services from the point of view of the Satisfiability Modulo Theories solver Z3.
1 Professor, ISP RAS
1 Samsung Research Russia
1 Alexander Mozhaysky Military Space Academy
1 Ntts Modul'
1 Yerevan State University
1 Positive Technologies
1 Huawei
1 FGU Federal Research Center of NIISI RAS
1 ILIT RAS — Branch of FSRC "Crystallography and Photonics" RAS
1 Lomonosov Moscow State University, 2 Keldysh Institute of Applied Mathematics of the RAS, 3 ISP RAS, 4 NRC "Kurchatov Institute"
1 Kazan Federal University
1 ISP RAS
1 Keldysh Institute of Applied Mathematics, RAS
1 Institute of Atmospheric Physics A.M. Obukhov RAS
1 Bauman Moscow State Technical University
1 ISP RAS
1 NRNU MEPhI
1 ISP RAS
1 ISP RAS
Paticipation in the conference and publication of articles are free of charge. Travel and accommodation, as well as other expenses are to be paid by the participant.
Contact us via e-mail scsec@ispras.ru to get instructions.
The papers should be 3-7 pages long, formatted using Templates for Conference Proceedings. Peer review is double-blind. Please remove any references to authors (such as names, affiliations or e-mails) from submitted articles, as well as direct references to previous works. In case of successful review and acceptance you will be requested to submit camera-ready text with necessary author details.
Submission is open at EasyChair.
Submissions that violate these guidelines will be rejected.
Where to find us
The conference takes place at the Main building of the Russian Academy of Science. See the map for exact information.
The RAS Main building is situated not far from Moscow Metro station "Leninskiy prospect" and Moscow Central Circle station "Ploshchad Gagarina".
The conference is held from 9:00 to 18:00 (with coffee breaks and lunch for guests and participants).