Workshop’s agenda
Modern software engineering is a very complex process fraught with many risks. Developers’ errors can lead to disastrous consequences such as information leaks, cyber currency fraud, and even human life losses. That’s why my program synthesis research is aimed at automating low-level software engineering tasks, which will not only help prevent scores of possible mistakes, but also increase developers’ productivity, to boot.
More specifically, we want to give developers the tools to set the general features of a software system (for example, forbidding it to share users’ payment details to third parties) and then automatically generate the code which will embody this specification. This is an extremely difficult task which involves searching for the right code among the myriad of programs that exist within a specific programming language. There are many schools of thought on how to make this search the most effective it can be. My research group advocates for the approach based on programming languages type systems. That’s what my talk at ITMO University was about.
Current research work
At the moment, my research group is exploring several different areas of program synthesis. One of the problems we’re working on is how to get the automatically generated code to not only perform according to its designated functions, but also do that effectively and with the least time, memory, and energy costs possible. It turned out that however unsurmountable, this task can be solved with the help of a special type system that would describe resource consumption.
Another cutting-edge research area we’re interested in is applying program synthesis to the field of linguistics. We’re cooperating with the UCSD Faculty of Linguistics in order to identify how program synthesis can act as a linguistic tool giving phonologists a better grasp of pronunciation rules in different languages, as well as a deeper understanding of how and why children all over the world are able to master these rules in a natural way.
ITMO University scientists’ related research projects
The workshop I gave at ITMO University was attended by students and professors alike. Some of them are involved in the research that is thematically very close to my line of work, so they asked really interesting questions, including one of the most topical in our scientific field: how to make it possible for a developer to quickly diagnose a problem and alter the specification if the original specification cannot be actualized in the form of a fully functioning program? This question arose during the workshop Q&A session, but scientists haven’t come up with a more or less viable answer yet.
How ITMO University changed in ten years
I came to St. Petersburg during my vacation and jumped at the chance to visit my alma mater for the first time in ten years. I was pleasantly surprised by the fact that my department is now home to as much as four high-profile laboratories headed by young associate professors and staffed by talented PhD students working full-time and publishing their articles in the leading scientific journals. I’m really impressed by all the progress the university has made.
Collaboration opportunities
I’m especially intrigued by the work Vladimir Ulyantsev’s research group is doing in the field of automated models synthesis. I think that their invaluable findings could be of real use to our linguistic program synthesis project, so I see a great potential for our future cooperation.
ITMO.NEWS spoke to Vladimir Ulyantsev, head of ITMO University’s ‘Computer Technologies’ laboratory, to find out more about the department’s pioneering research.
Which software engineering tasks does the automated models synthesis solve?
An automated model is no more than a set of states (graph nodes) combined with conditioned transitions between them (designated graph edges). Due to its relative simplicity and illustrative properties, these models are often used for visualization and implementation of a variety of different processes and software-hardware systems. Deterministic finite-state automations, for example, find their use in compilers development and speech recognition systems. Generally speaking, any intuitive algorithm can be translated to an memory-tape automation also known as the Turing machine. This is what many ITMO’s Computer Technologies department associate professor Andrey Stankevich’s lectures are about.
More complex automation machines are used in controller software as they allow developers to build the controller system logic, automatically converting it to code. Dubbed as automata-based programming, this technique was developed by ITMO University professor Anatoly Shalyto.
During the automated model synthesis process, models are created automatically based on information pre-specified by user. In other words, instead of making engineers painstakingly create automated machines by hand, algorithms build them on prerequisite specifications. Conducting a finite-state automation synthesis implies that there are certain boundaries set by examples of a correct and faulty automation behavior, and developers have to find a model that functions on correct examples and anticipates the faulty ones. Having emerged more than fifty years ago, program synthesis is now at the forefront of software development. Our research group started working on synthesis-related tasks in 2010.
Which results do you want to achieve?
One of our main goals is perfecting and developing new approaches to finite-state automation synthesis. Our recent accomplishments include publishing a research paper that proposes improvements to the algorithm considered the best finite-state automation synthesis tool to date. Our PhD student Ilya Zakirzyanov is conducting cutting-edge research on using algorithms in creating models for pre-existing programs and has recently been awarded a Russian Foundation for Basic Research grant supporting his work in the field.
Automated model synthesis research is the driving force for designing software that is safe and reliable. That’s why we attach particular importance to cyberphysical systems testing, verification, and synthesis methods, which we develop in close collaboration with Aalto University as our ‘Computer Technologies’ laboratory co-head Valeriy Vyatkin works there. These methods are vital for building and testing controllers used on nuclear power stations and civil navigations systems. Simply put, we’re constantly searching for ways to limit the damage made by possible controllers-related mistakes. In this we are supported by the Ministry of Science and Higher Education of the Russian Federation federal target program grant.
Want to learn more about Nadezhda Polikarpova’s research? This ITMO.NEWS interview is a fascinating insight into her line of work and her riveting academic career at the University of California, San Diego.
