Thesis Details

Automata in Software Verification and Testing

Ph.D. Thesis Student: Hruška Martin Academic Year: 2023/2024 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Automaty ve Verifikaci a Testování Software

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

Degree Programme
Computer Science and Engineering, Field of Study Computer Science and Engineering
5 March 2024
HRUŠKA, Martin. Automata in Software Verification and Testing. Brno, 2023. Ph.D. Thesis. Brno University of Technology, Faculty of Information Technology. 2024-03-05. Supervised by Vojnar Tomáš. Available from:
    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 = ""
Back to top