Original title: Rozvoj nástroje ASMA pro analýzu programů s řetězci pomocí symbolických automatů
Translated title: Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Authors: Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2022
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %. In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
Keywords: abstraktní regulární model checking; ARMC; ASMA; AutomataDotNet; konečné automaty; převodníky; regulární model checking; reverzní konkatenace; RMC; symbolické konečné automaty; VeriFIT; abstract regular model checking; ARMC; ASMA; AutomataDotNet; finite automata; regular model checking; reverse concatenation; RMC; symbolic finite automata; transducers; VeriFIT

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

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


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