Thesis Details
Automata in Software Verification and Testing
This thesis focuses on applications of automata theory to software quality. In the first part, we focus on shape analysis which can be used for formal verification of programs manipulating dynamic data structures. Particularly, we develop an approach of backward program execution along possible counterexamples tracesvand counterexample-guided refinement for shape analysis based on forest automata.We also introduce a new approach based on automata over graphs with a bounded tree width which is more general than forest automata but still has feasible computation properties.
In the second part, we introduce a method for automated testing of manufacturing execution systems (MES) in digital twin. We are able to orchestrate a digital twin to reproduce behaviour of a real-world setting in which MES is deployed and so provide a safe environment for testing.Moreover, we can generate new test cases by applying automata and abstraction over them in this context.
static analysis, formal verification, shape analysis, testing, finite automata
@phdthesis{FITPT918,
author = "Martin Hru\v{s}ka",
type = "Ph.D. thesis",
title = "Automata in Software Verification and Testing",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2024,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/phd-thesis/918/"
}