About Us
The complexity of software products today is so great that simply reviewing the source code makes it very difficult, time-consuming, and often nearly impossible to understand them. As a result, tools that support code comprehension, maintenance, verification, debugging, or transformation are playing an increasingly important role in the software industry. These tools can operate dynamically (i.e., at runtime) or statically (i.e., without executing the analyzed or transformed program).
Our research group develops static code analysis and program transformation methods, and builds frameworks for several widely used programming languages, such as C/C++, C#, Erlang, Elixir, Haskell, Java, Python, and P4. Furthermore, we are working on integrating tools that make the results of open-source analyzers easily accessible. Our research covers the formal verification of program transformations as well as the investigation of correct-by-construction refactoring methods. We also study the formal semantics of programming languages, theories of program equivalence, and rewriting theories suitable for describing refactoring transformations.
Currently, our research group participates in five different research, development, and innovation projects: CodeChecker, CodeCompass, RefactorErl, HARP and T4P4S.
Research Interests
- Static program analysis and program transformation techniques
- Support for code comprehension and software maintenance
- Software visualization
- Theory and practice of secure coding
- Code checking (based on standards and custom requirements)
- Quality, complexity, and execution time analysis, software metrics
- Green computing
- Formal semantics, logics, and verification
- Rewriting systems
- Interactive theorem proving
- Software testing
Methodology
The algorithmic analysis of software requires formalizing the rules of programming languages and representing the syntactic and semantic information of the code. We introduced the concept of the Semantic Program Graph, which is an extension of abstract syntax tree-based representations. This approach enables us to perform symbolic, semantic, and control flow analyses efficiently, and incrementally where possible. Building upon these analyses, we develop checking tools, visualization solutions, and semantics-preserving program transformations. During formalization, we rely on well-established tools such as Coq, the K framework, and QuickCheck. Most of our activities are carried out in the ELTE–Ericsson Software Technology Laboratory, and in collaboration with our industrial partners, we explore effective combinations of scientific theory and practical application.
Research Staff
- Zoltán Horváth
- István Bozó
- Máté Cserép
- Dániel Horpácsi
- Tamás Kozsik
- Dániel Lukács
- Norbert Pataki
- Zoltán Porkoláb
- Máté Tejfel
- Simon Thompson
- Melinda Tóth
- and 12 postdoctoral researchers and PhD students
Projects
International projects: ParaPhrase: Parallel Patterns for Adaptive Heterogeneous Multicore Systems, 288570 (FP7, 2013-2015)
National projects:
- TECH_08_A2-SZOMIN08
- KMOP-1.1.2-08/1-2008-0002 (2010-2012)
- EITKIC_12-1-2012-0001 (2013-2014)
- EFOP-3.6.2-16-2017-00013 (2017-2020)
- EFOP-3.6.3-VEKOP-16-2017-00002
- ED18-1-2019-0030, 2020-4.1.1.-TKP2020
- TKP2021-NVA-29
+ 8 industrial partners
Selected Publications
- R. Szalay, Á. Sinkovics, Z. Porkoláb (2021): Practical heuristics to improve precision for erroneous function argument swapping detection in C and C++, Journal of Systems and Software [DOI]
- Z. Porkoláb, T. Brunner, D. Krupp, M. Csordás (2018): CodeCompass: An open software comprehension framework for industrial usage, IEEE/ACM 26th International Conference on Program Comprehension [DOI]
- T. Kozsik, M. Tóth, I. Bozó (2017): Free the Conqueror! Refactoring divide-and-conquer functions, Future Generation Computer Systems [DOI]
- D. Horpácsi, P. Bereczky, S. Thompson (2023): Program equivalence in an untyped, call-by-value functional language with uncurried functions, Journal of Logical and Algebraic Methods in Programming [DOI]
- D. Lukács, G. Pongrácz, M. Tejfel (2020): Control flow based cost analysis for P4, Open Computer Science [DOI]
Contact
Melinda Tóth – toth_m@inf.elte.hu