Research group

Programming Languages and Tools Lab

Publications

An Empirical Study of Partial Deduction for MiniKanren

March 2021

Ekaterina Verbitskaia, Daniil Berezun, Dmitry Boulytchev

Read more

Beyond the elementary representations of program invariants over algebraic data type

2021

Kostyukov Yurii, Dmitry Mordvinov, and Grigory Fedyukovich

Mechanized Theory of Event Structures: A Case of Parallel Register Machine

2021

Vladimir Gladstein, Dmitrii Mikhailovskii, Evgenii Moiseenko, Anton Trunov

Syrcose'21

Read more

Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One

2021

Daniil Berezun, Dmitry Boulytchev

TFPIE-2021

Read more

Recursive Expressions for SPARQL Property Paths

August 2020

Ciro Medeiros, Umberto Costa, Semyon Grigorev, Martin A. Musicante

Regular expressions are used in SPARQL property paths to query RDF graphs. However, regular expressions can only define the most limited class of languages, called regular languages. Context-free languages are a wider class containing all regular languages. There are no context-free expressions to define them, so it is necessary to write grammars. We propose an extension of regular expressions, called recursive expressions, to support the definition of a subset of context-free languages. The goal of our work is therefore to provide simple operators allowing the definition of languages as close as possible to context-free languages.
ADBIS, TPDL and EDA 2020 Common Workshops and Doctoral Consortium

Read more

Context-Free Path Querying by Kronecker Product

August 2020

Egor Orachev, Ilya Epelbaum, Rustam Azimov, Semyon Grigorev

Context-free path queries (CFPQ) extend the regular path queries (RPQ) by allowing context-free grammars to be used as constraints for paths. Algorithms for CFPQ are actively developed, but J. Kuijpers et al. have recently concluded, that existing algorithms are not performant enough to be used in real-world applications. Thus the development of new algorithms for CFPQ is justified. In this paper, we provide a new CFPQ algorithm which is based on such linear algebra operations as Kronecker product and transitive closure and handles grammars presented as recursive state machines. Thus, the proposed algorithm can be implemented by using high-performance libraries and modern parallel hardware. Moreover, it avoids grammar growth which provides the possibility for queries optimization.

ADBIS 2020. Advances in Databases and Information Systems. Lecture Notes in Computer Science.

Read more

Reconciling Event Structures with Modern Multiprocessors

July 2020

Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis

The European Conference on Object-Oriented Programming (ECOOP)

Read more

Context-Free Path Querying with Single-Path Semantics by Matrix Multiplication

June 2020

Arseniy Terekhov, Artyom Khoroshev, Rustam Azimov, Semyon Grigorev

A recent study showed that the applicability of context-free path querying (CFPQ) algorithms with relational query semantics integrated with graph databases is limited because of low performance and high memory consumption of existing solutions. In this work, we implement a matrix-based CFPQ algorithm by using appropriate high-performance libraries for linear algebra and integrate it with RedisGraph graph database. Also, we introduce a new CFPQ algorithm with single-path query semantics that allows us to extract one found path for each pair of nodes. Finally, we provide the evaluation of our algorithms for both semantics which shows that matrix-based CFPQ implementation for Redis-Graph database is performant enough for real-world data analysis.

GRADES-NDA'20: Proceedings of the 3rd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA)

Read more

Modification of Valiant’s algorithm for the string-matching problem

June 2020

Susanina Y.A., Yaveyn A.N., Grigorev S.V.

This paper aims to present Valiant’s algorithm modification, which main advantage is the possibility to divide the parsing table into successively computed layers of disjoint submatrices where each submatrix of the layer can be processed independently. Moreover, our approach is easily adapted for the string-matching problem.

Proceedings of the Institute for System Programming

Read more

Context-Free Path Querying via Matrix Equations

June 2020

Yuliya Susanina

Context-free path querying (CFPQ) widely used for graph-structured data analysis in different areas. It is crucial to develop highly efficient algorithms for CFPQ since the size of the input data is typically large. We show how to reduce GFPQ evaluation to solving systems of matrix equations over R --- a problem for which there exist high-performance solutions. Also, we demonstrate the applicability of our approach to real-world data analysis.
Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data

Read more

Repairing and Mechanising the JavaScript Relaxed Memory Model

June 2020

Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod Shu-yu Guo

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

Read more

Promising 2.0: Global Optimizations in Relaxed Memory Concurrency

June 2020

Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

Read more

Optimizing GPU programs by partial evaluation

February 2020

Aleksey Tyurin, Daniil Berezun, Semyon Grigorev

While GPU utilization allows one to speed up computations to the orders of magnitude, memory management remains the bottleneck making it often a challenge to achieve the desired performance. Hence, different memory optimizations are leveraged to make memory being used more effectively. We propose an approach automating memory management utilizing partial evaluation, a program transformation technique that enables data accesses to be pre-computed, optimized, and embedded into the code, saving memory transactions. An empirical evaluation of our approach shows that the transformed program could be up to 8 times as efficient as the original one in the case of CUDA C naïve string pattern matching algorithm implementation.

PPoPP '20: Proceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Read more

Compilation of OCaml memory model into Power (In Russian)

December 2019

Egor Namakonov, Anton Podkopaev

Proceedings of ISP RAS

Read more

Path Querying with Conjunctive Grammars by Matrix Multiplication

December 2019

R. Azimov and S. Grigorev

Path querying with conjunctive grammars is known to be undecidable. There is an algorithm for path querying with linear conjunctive grammars which provides an over-approximation of the result, but there is no algorithm for arbitrary conjunctive grammars. We propose the first algorithm for path querying with arbitrary conjunctive grammars. The proposed algorithm is matrix-based and allows us to efficiently apply GPGPU computing techniques and other optimizations for matrix operations.

Programming and Computer Software

Read more

Improved Architecture of Artificial Neural Network for Secondary Structure Analysis

November 2019

Semyon Grigorev and Polina Lunina

BMC Bioinformatics

Read more

Property Directed Inference of Relational Invariants

October 2019

D. Mordvinov, G. Fedyukovich

Proceedings of 19th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2019

Read more

On Satisfiability of Nominal Type Systems With Variance

July 2019

A. Misonizhnik, D. Mordvinov

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Read more

Bar-Hillel Theorem Mechanization in Coq

June 2019

Sergey Bozhko, Leyla Khatbullina, Semyon Grigorev

The Bar-Hillel theorem states that context-free languages are closed under intersection with a regular set. This theorem has a constructive proof and thus provides a formal justification of correctness of the algorithms for applications mentioned above. Mechanization of the Bar-Hillel theorem, therefore, is both a fundamental result of formal language theory and a basis for the certified implementation of the algorithms for applications. In this work, we present the mechanized proof of the Bar-Hillel theorem in Coq.

Logic, Language, Information, and Computation

Read more

Evaluation of the Context-Free Path Querying Algorithm Based on Matrix Multiplication

June 2019

Nikita Mishin, Iaroslav Sokolov, Egor Spirin, Vladimir Kutuev, Egor Nemchinov, Sergey Gorbatyuk, and Semyon Grigorev

Recently proposed matrix multiplication based algorithm for context-free path querying (CFPQ) offloads the most performance-critical parts onto boolean matrices multiplication. Thus, it is possible to achieve high performance of CFPQ by means of modern parallel hardware and software. In this paper, we provide results of empirical performance comparison of different implementations of this algorithm on both real-world data and synthetic data for the worst cases.
Proceedings of the 2nd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA)

Read more

The Composition of Dense Neural Networks and Formal Grammars for Secondary Structure Analysis

March 2019

Semyon Grigorev and Polina Lunina

We propose a way to combine formal grammars and artificial neural networks for biological sequences processing. Formal grammars encode the secondary structure of the sequence and neural networks deal with mutations and noise. In contrast to the classical way, when probabilistic grammars are used for secondary structure modeling, we propose to use arbitrary (not probabilistic) grammars which simplifies grammar creation. Instead of modeling the structure of the whole sequence, we create a grammar which only describes features of the secondary structure. Then we use matrix-based parsing to extract features: the fact that some substring can be derived from some nonterminal is a feature. After that, we use a dense neural network to process features.

Proceedings of the 12th International Joint Conference on Biomedical Engineering Systems and Technologies - BIOINFORMATICS

Read more

Path querying on acyclic graphs using Boolean grammars

January 2019

Shemetova E.N., Grigorev S.V.

One of the problems in graph data analysis is querying for specific paths. Such queries are usually performed by means of a formal grammar that describes the allowed edge-labeling of the paths. Path query is said to be calculated using relational query semantics if it is evaluated to triple ((A,v1,v2), such that there is a path from v1 to v2 such that the labels on the edges of this path form a string derivable from the nonterminal A. We focus on the Boolean languages that use Boolean grammars to describe the labeling of paths. Although path querying using relational query semantics and Boolean grammars is known to be undecidable, in this work we propose a path querying algorithm on acyclic graphs which uses relational query semantics and Boolean grammars and approximates the exact solution. To achieve better performance in compare with the naive algorithm, considered classes of graphs were limited to acyclic graphs.

Proceedings of the Institute for System Programming

Read more

Bridging the Gap Between Programming Languages and Hardware Weak Memory Models

January 2019

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis

46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal

Read more

Relational Interpreters for Search Problems

2019

Proceedings of the 2019 miniKanren and Relational Programming Workshop

Read more

Constructive Negation for MiniKanren

2019

Proceedings of the 2019 miniKanren and Relational Programming Workshop

Read more

A Survey of Smart Contract Safety and Programming Languages

2019

A. Tyurin, I. Tyulyandin, V. Maltsev, I. Kirilenko, and D. Berezun

Preliminary Proceedings of the 13 rd Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2019), May 29-31, 2019 – Saratov, Russian Federation

Read more

Survey on Blockchain Technology, Consensus Algorithms, and Alternative Distributed Technologies

2019

N. Mishin, A. Fefelov, V. Bushev, I. Kirilenko, and D. Berezun

SEIM-19

Read more

Certified Semantics for miniKanren

2019

Proceedings of the 2019 miniKanren and Relational Programming Workshop

Read more

Extended Abstract: F# OpenCL Type Provider

September 2018

Kirill Smirenko, Semyon Grigorev

Extended abstract at TyDe 2018 (at ICFP).

Read more

Detecting Near Duplicates in Software Documentation

September 2018

D.V. Luciv, D.V. Koznov, G.A. Chernishev, A.N. Terekhov, K.Y. Romanovsky, D.A. Grigoriev

Programming and Computer Software

Read more

Parser combinators for context-free path querying

September 2018

Ekaterina Verbitskaia, Ilya Kirillov, Ilya Nozkin, Semyon Grigorev

Transparent integration of a domain-specific language for specification of context-free path queries (CFPQs) into a general-purpose programming language as well as static checking of errors in queries may greatly simplify the development of applications using CFPQs. LINQ and ORM can be used for the integration, but they have issues with flexibility: query decomposition and reusing of subqueries are a challenge. Adaptation of parser combinators technique for paths querying may solve these problems. Conventional parser combinators process linear input, and only the Trails library is known to apply this technique for path querying. We demonstrate that it is possible to create general parser combinators for CFPQ which support arbitrary context-free grammars and arbitrary input graphs. We implement a library of such parser combinators and show that it is applicable for realistic tasks.

Proceedings of the 9th ACM SIGPLAN International Symposium on Scala

Read more

Relational Programming with memoization and negation (In Russian)

August 2018

E. Moiseenko, A. Podkopaev

NTV SPbSTU

Read more

Context-free path querying by matrix multiplication

June 2018

Rustam Azimov, Semyon Grigorev

GRADES-NDA '18 Proceedings of the 1st ACM SIGMOD Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA)

Read more

Poster: Duplicate finder toolkit

2018

D.Luciv, D.Koznov, G.Chernishev, H.A. Basit, K.Romanovsky, A.Terekhov

40th ACM/IEEE International Conference on Software Engineering, ICSE 2018

Read more

Typed Relational Conversion

2018

Petr Lozov, Andrey Vyatkin, Dmitry Boulytchev

18th International Symposium on Trends in Functional Programming

Read more

Typed Embedding of a Relational Language in OCaml

2018

Proceedings ML/OCAML 2016

Read more

Improving Refutational Completeness of Relational Search via Divergence Test

2018

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming

Read more

Context-Free Path Querying with Structural Representation of Result

December 2017

Semyon Grigorev, Anastasiya Ragozina

There are several solutions for CFPQ, but how to provide structural representation of query result which is practical for answer processing and debugging is still an open problem. In this paper we propose a graph parsing technique which allows one to build such representation with respect to given grammar in polynomial time and space for arbitrary context-free grammar and graph. Proposed algorithm is based on generalized LL parsing algorithm, while previous solutions are based mostly on CYK or Earley algorithms, which reduces time complexity in some cases.

Proceedings of the 13th Central & Eastern European Software Engineering Conference in Russia (CEE-SECR '17)

Read more

Promising Compilation to ARMv8.3 (In Russian)

December 2017

A. Podkopaev, O. Lahav, V. Vafeiadis

Proceedings of ISP RAS

Read more

On compilation correctness for a subset of a promising memory model to the ARMv8.3 memory model (In Russian)

December 2017

A. Podkopaev, O. Lahav, V. Vafeiadis

NTV SPbSTU

Read more

Graph Parsing by Matrix Multiplication

July 2017

Rustam Azimov, Semyon Grigorev

arXiv

Read more

Promising Compilation to ARMv8 POP

June 2017

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis

The European Conference on Object-Oriented Programming (ECOOP)

Read more

Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation

January 2017

Daniil Berezun and Neil D. Jones

Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Read more

Untyped Lambda-Calculus Normalization by Traversals (in Russian)

2017

Berezun D.A.

Известия вузов. Северо Кавказский регион. Технические науки. – 2017. – No 4. – C. 5–12.

Read more

Complete Head Linear Reduction (in Russian)

2017

Berezun D.A.

St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunications and Control Systems

Read more

Synchronizing constrained horn clauses

2017

Mordvinov, Dmitry, and Grigory Fedyukovich

LPAR, EPiC Series in Computing. EasyChair

Verifying Safety of Functional Programs with Rosette/Unbound

2017

Dmitry Mordvinov and Grigory Fedyukovich

TRIK studio: Technical introduction

2017

Mordvinov Dmitry, Yurii Litvinov, and Timofey Bryksin

Open Innovations Association (FRUCT), 2017 20th Conference of. IEEE

Certified Grammar Transformation to Chomsky Normal Form in F*

August 2016

Marina Polubelova, Sergey Bozhko, Semyon Grigorev

Proceedings of the Institute for System Programming

Read more

Relaxed Parsing of Regular Approximations of String-Embedded Languages

June 2016

Ekaterina Verbitskaia , Semyon Grigorev, Dmitry Avdyukhin

We present a technique for syntax analysis of a regular set of input strings. This problem is relevant for the analysis of string-embedded languages when a host program generates clauses of embedded language at run time. Our technique is based on a generalization of RNGLR algorithm, which, inherently, allows us to construct a finite representation of parse forest for regularly approximated set of input strings. This representation can be further utilized for semantic analysis and transformations in the context of reengineering, code maintenance, program understanding etc. The approach in question implements relaxed parsing: non-recognized strings in approximation set are ignored with no error detection.

Perspectives of System Informatics

Read more

Operational Aspects of C/C++ Concurrency

June 2016

Anton Podkopaev, Ilya Sergey, Aleksandar Nanevski

arXiv

Read more

Clone detection in reuse of software technical documentation

2016

Koznov, D., Luciv, D., Basit, H.A., Lieh, O.E., Smirnov, M.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9609, pp. 170-185

Incremental Garbage Collection Library for C++ (in Russian)

2016

E. Moiseenko, D. Berezun

SEIM-16

Read more

Lexical Analysis of Dynamically Generated String Expressions

2016

Marina Polubelova, Semyon Grigorev

Systems and Means of Informatics

Read more

On fuzzy repetitions detection in documentation reuse

2016

Lucive, D.V., Koznov, D.V., Basit, H.A., Terekhov, A.N.

Programming and Computer Software, 42 (4), pp. 216-224

Working Notes: Compiling ULC to Lower-level Code by Game Semantics and Partial Evaluation

2016

Daniil Berezun and Neil D. Jones

META 2016 Fifth International Valentin Turchin Workshop on Metacomputation

Read more

Survey on formal methods in robotics

2016

D. A. Mordvinov, Yu. V. Litvinov

SPbSPU Journal. Computer Science. Telecommunication and Control Systems, no. 1(236), 84–107

A Language-Independent Code Formatting by Syntactic Matching and Templates (In Russian)

October 2015

A.Podkopaev, A.Korovianskii, I.Ozernykh

NTV SPbSTU 4 (224)

Read more

Generalized Table-based LL-parsing

2015

Ragozina Anastasiya, Grigorev Semyon

Systems and Means of Informatics

Read more

Combinators and Type-Driven Transformers in Objective Caml

2015

Dmitry Boulytchev

Science of Computer Programming

Read more

On development of static analysis tools for string-embedded languages

2015

Marat Khabibullin, Andrei Ivanov, Semyon Grigorev

Proceedings of the 11th Central & Eastern European Software Engineering Conference in Russia

Read more

Polynomial-Time Optimal Pretty-Printing Combinators with Choice

2014

Anton Podkopaev, Dmitry Boulytchev

Proceedings of 9th International Andrei Ershov Memorial Conference on Perspectives of System Informatics

Read more

Precise Garbage Collection for C++ with a Non-Cooperative Compiler

2014

Daniil Berezun, Dmitry Boulytchev

Proceedings of the 10th Central and Eastern European Software Engineering Conference in Russia

Read more

String-embedded Language Support in Integrated Development Environment

2014

Semen Grigorev, Ekaterina Verbitskaia, Andrei Ivanov, Marina Polubelova, and Ekaterina Mavchun

Proceedings of the 10th Central and Eastern European Software Engineering Conference in Russia 2014

Read more

GLR-based Abstract Parsing

2013

Semen Grigorev and Iakov Kirilenko

Proceedings of the 9th Central & Eastern European Software Engineering Conference in Russia

Read more

Document Teaching to write software engineering documents with focus on document design by means of mind maps

2012

Koznov, D.V.

Proceedings of the IASTED International Conference on Computers and Advanced Technology in Education, CATE 2012 pp. 112-118

Mind maps merging in collaborative work

2011

Koznov, D., Larchik, E., Pliskin, M., Artamonov, N.

Programming and Computer Software 37 (6), pp. 315-321

Document Refactoring the documentation of software product lines

2011

Romanovsky, K., Koznov, D., Minchin, L.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4980 LNCS, pp. 158-170

Document Towards e-government services in Russia

2011

Koznov, D., Samochadin, A., Azarskov, A., Chevzova, J.

KMIS 2011 - Proceedings of the International Conference on Knowledge Management and Information Sharing pp. 294-301

Efficiently Scrapping Boilerplate Code in OCaml

2011

Dmitry Boulytchev, Sergey Mechtaev

Workshop on ML

Read more

Hardware Description Language Based on Message Passing and Implicit Pipelining

2010

Dmitry Boulytchev, Oleg Medvedev

Proceedings of the 2010 East-West Design & Test Symposium

Read more

A knowledge management approach for industrial model-based testing

2009

Koznov, D., Malinov, V., Sokhransky, E., Novikova, M.

KMIS 2009 - 1st International Conference on Knowledge Management and Information Sharing, Proceedings pp. 200-205

Computer-supported collaborative learning with mind-maps

2008

Koznov, D., Pliskin, M.

Communications in Computer and Information Science 17 CCIS, pp. 478-489

DocLine: A method for software product lines documentation development

2008

Koznov, D.V., Romanovsky, K.Yu.

Programming and Computer Software 34 (4), pp. 216-224

BURS-based Instruction Set Selection

2006

Dmitry Boulytchev

Proceedings of 6th International Andrei Ershov Memorial Conference on Perspectives of System Informatics

Read more

REAL-IT: Model-Based User Interface Development Environment

2005

A.Ivanov, D.Koznov

Proceedings of IEEE/NASA ISoLA 2005 Workshop on Leveraging Applications of Formal Methods, Verification, and Validation. Loyola College Graduate Center Columbia, Maryland, USA, P. 31-41

Cooking Raw Types in Java

2005

Dmitry Boulytchev, Eugene Vigdorchik

Workshop on Multiparadigm Programming with Object-Oriented Languages

Read more

Efficient Code Generation Algorithms (in Russian)

2004

Dmitry Boulytchev

System Informatics

Read more

Macroarchitecture Description Language for Hardware/Software Codesign (in Russian)

2004

Dmitry Boulytchev

System Programming

Read more

Macroarchitecture Description for Hardware/Software Codesign (in Russian)

2004

Dmitry Boulytchev

System Programming

Read more

OCL-based automated validation method for UML specifications

2003

Ol'khovich, L., Koznov, D.V.

Source of the DocumentProgramming and Computer Software 29 (6), pp. 323-327

On Project-Specific Languages and Their Application in Reengineering

2002

Dmitry Boulytchev, Dmitry Koznov, Andrey A. Terekhov

Proceedings of the European Conference on Software Maintenance and Reengineering, CSMR 995802, pp. 177-185

Read more

Document A method for recovery and maintenance of software architecture

2001

Koznov, D., Romanovsky, K., Nikitin, A.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2244 LNCS, pp. 324-327

An Empirical Study of Retargetable Compilers

2001

Dmitry Boulytchev, Dmitry Lomov

Proceedings of 4th International Andrei Ershov Memorial Conference on Perspectives of System Informatics

Read more

Pattern-matching and Identification of Structural Types in PL/1 (in Russian)

2000

Dmitry Boulytchev

Automated Reengeneering of Programs, Saint Petersburg

Read more

RTST++: Methodology and a CASE tool for the development of information systems and software for real-time systems

1999

Terekhov, A.N., Romanovskii, K.Yu., Koznov, D.V., Dolgov, P.S., Ivanov, A.N.

Programming and Computer Software 25 (5), pp. 276-281