Bemutatkozás

A szoftvertermékek összetettsége ma már olyan nagy, hogy pusztán a forráskód átnézésével nagyon nehéz, időigényes, sokszor pedig szinte lehetetlen megérteni őket. Emiatt a szoftveriparban egyre nagyobb szerepet kapnak azok az eszközök, amelyek támogatják a kód megértését, karbantartását, ellenőrzését, hibakeresését vagy átalakítását. Ezek az eszközök működhetnek dinamikusan, tehát futás közben, vagy statikusan, vagyis a vizsgált vagy átalakított program futtatása nélkül.

Kutatócsoportunk statikus kódelemzési és programátalakítási módszereket dolgoz ki, valamint keretrendszereket fejleszt számos széles körben használt programozási nyelvhez, például C/C++, C#, Erlang, Elixir, Haskell, Java, Python és P4 nyelvekhez. Emellett olyan eszközök integrációján is dolgozunk, amelyek nyílt forráskódú elemzők eredményeit teszik könnyen felhasználhatóvá. Kutatásaink kiterjednek a programátalakítások formális verifikációjára, továbbá az eleve helyes refaktorálási módszerek vizsgálatára is. Foglalkozunk programozási nyelvek formális szemantikájával, a programegyenértékűség elméleteivel, valamint olyan átírási elméletekkel, amelyek alkalmasak a refaktoráló átalakítások leírására.

Jelenleg kutatócsoportunk öt különböző kutatás-fejlesztési és innovációs projektben vesz részt: CodeChecker, CodeCompass, RefactorErl, HARP és T4P4S.

Kutatási területek

• Statikus programelemzési és programátalakítási technikák
• Kódmegértés és szoftverkarbantartás támogatása
• Szoftvervizualizáció
• Biztonságos kódolás elmélete és gyakorlata
• Kódellenőrzés (szabványok és egyedi követelmények alapján)
• Minőség-, komplexitás- és futási idő elemzés, szoftvermetrikák
• Zöld informatika
• Formális szemantika, logikák és verifikáció
• Átírási rendszerek
• Interaktív tételbizonyítás
• Szoftvertesztelés

Módszertan

A szoftverek algoritmikus elemzése megköveteli a programozási nyelvek szabályainak formalizálását, valamint a kód szintaktikai és szemantikai információinak reprezentálását. Bevezettük a Szemantikus Programgráf fogalmát, amely az absztrakt szintaxisfán alapuló reprezentációk kiterjesztése. Ez a megközelítés lehetővé teszi, hogy szimbolikus, szemantikai és vezérlési folyamatelemzéseket hatékonyan, lehetőség szerint inkrementálisan végezzünk. Ezekre az elemzésekre építve fejlesztünk ellenőrző eszközöket, vizualizációs megoldásokat, valamint szemantikamegőrző programátalakításokat. A formalizáció során jól bevált eszközökre támaszkodunk, mint például a Coq, a K-keretrendszer és a QuickCheck. Tevékenységeink nagy részét az ELTE–Ericsson Szoftvertechnológiai Laboratóriumban végezzük, és ipari partnereinkkel együttműködve a tudományos elmélet és a gyakorlati alkalmazás hatékony kombinációit kutatjuk.

Kutatócsoport tagjai

• Horváth Zoltán
• Bozó István
• Cserép Máté
• Horpácsi Dániel
• Kozsik Tamás
• Lukács Dániel
• Pataki Norbert
• Porkoláb Zoltán
• Tejfel Máté
• Simon Thompson
• Tóth Melinda
• továbbá 12 postdoc és PhD diák

Projektek

Nemzetközi projektek: ParaPhrase: Parallel Pakerns for Adap9ve Heterogeneous Mul9core Systems, 288570 (FP7, 2013-2015)

Hazai projektek:

• 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 ipari partner

Kiemelt publikációk

• 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]

Kapcsolat

Tóth Melinda – toth_m@inf.elte.hu