Original title: Aplikace formálních metod v analýze sémantických rozdílů mezi verzemi software
Translated title: Applying formal methods to analysis of semantic differences between versions of software
Authors: Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Document type: Master’s theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Cílem této práce je navrhnout integraci formálních metod pro DiffKemp, nástroj pro statickou analýzu sémantických rozdílů v rozsáhlých programech napsaných v jazyce C. Cílem tohoto rozšíření je umožnit analýzu složitějších změn, které by typicky byly analyzovatelné spíše nástroji založenými na formálních metodách, a zároveň zachovat škálovatelnost nástroje DiffKemp na velké projekty. Principem navrženého řešení je při analýze v případě nalezení možné sémantické změny zakódovat problém ekvivalence příslušných instrukcí jako instanci problému SMT. Tím je možné sémantický rozdíl potvrdit, nebo vyvrátit s pomocí SMT solveru. Navržené řešení bylo implementováno v nástroji DiffKemp a experimenty provedené na sadě programů zvané EqBench ukazují, že rozšiřuje schopnosti nástroje DiffKemp, převážně v oblasti přesné analýzy úprav aritmetických výrazů. The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
Keywords: DiffKemp; formální metody; Linuxové jádro; LLVM IR; sbírka programů EqBench; statická analýza; sémantické rozdíly; vzory změn v kódu; Z3 solver; řešení problému SMT; code change pattern; DiffKemp; EqBench benchmark; formal methods; Linux kernel; LLVM IR; semantic differences; SMT solving; static analysis; Z3 solver

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: https://hdl.handle.net/11012/249016

Permalink: http://www.nusl.cz/ntk/nusl-618713


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses