Telbisz Csanád MSc thesis

publications/publications.bib

@@ -642,3 +642,20 @@ @misc{cziborovadMsc2023
     url_pdf = {cziborovadMsc2023.pdf},
     abstract = {Ensuring the safe operation of real-time software-intensive systems is crucial in many critical applications, such as automatic driver assist systems, monitors for railway systems, and smart cities. Automated model checking provides a mathematically precise way to maintain safety and prevent damage to property by formally verifying correctness. Real-time scheduling requirements and complex timed behavior make the verification of real-time software-intensive systems difficult. These systems also contain computations with external data, \eg sensor data, and heavily data-dependent computations. These properties pose a twofold challenge: (1) development of the software often requires complex toolchains, such as statechart-based modeling to adequately express behaviors, and (2) formal verification is adversely affected by state space explosion caused by the possible scheduling and data inputs. To counteract the latter problem, abstraction-based model checking tools have been developed in the literature. In our previous work, we developed a combination of abstraction-based algorithms to simultaneously handle timed behaviors and complex data acquisition. However, existing low-level formalisms for timed model checking lack the expressive power to represent system models from high-level modeling toolchains. While discrete approximations of timed behaviors are a common solution to enable the use of more expressive verification algorithms that do not natively support timed behaviors, this may introduce unsoundness due to discretization error. This work aims to propose an intermediate formalism to represent real-time software-intensive system models, and adapt existing abstraction-based model checking algorithms. In particular, we (i) propose an extension to the Extended Symbolic Transition System (XSTS) formalism used as an intermediate model in the Gamma statchart-based modeling toolchain to represent timed systems, leveraging the existing capabilities of Gamma and XSTS to represent complex data-driven behaviors and communication between system components. We also (ii) adapt abstraction-based model checking approaches to handle the verification of timed XSTS, including (iii) handling complex control flow caused by component communication and hierarchical modeling in our combined verification algorithm. We (iv) implement the timed XSTS formalism and the verification algorithms in the open-source Theta verification framework and (v) evaluate the proposed approaches on case studies from industrial projects, as well as synthetic benchmarks. As a result, verification of complex real-time software-intensive systems is enabled without limitations to expressive power or unsoundness introduced by discretization.},
 }
+
+@misc{telbiszcsMsc2024,
+    author = {Telbisz, Csan\'ad},
+    title = {Efficient automatic verification of concurrent programs},
+    note = {Master's Thesis, Budapest University of Technology and Economics},
+    year = {2024},
+    type = {Thesis},
+    url_pdf = {telbiszcsMsc2024.pdf},
+    url_link = {https://diplomaterv.vik.bme.hu/en/Theses/Tobbszalu-programok-hatekony-automatikus},
+    abstract = {As multi-core processors gain popularity in safety-critical systems, multi-threaded programs are increasingly used. Concurrency introduces a new level of complexity into software verification due to the great number of possible thread interleavings. Achieving satisfying test coverage is even more challenging, and naive verification techniques often become practically infeasible due to this complexity. Formal verification techniques can provide the desired safety guarantees. However, sophisticated algorithms are needed to handle the complexity of a concurrent system.
+                \par
+                Partial order reduction has proven to be an effective technique to address the problem of interleavings in model checking. The approach detects independent program statements and skips the exploration of certain thread interleavings based on this information. I present a novel theoretical framework that combines partial order reduction algorithms with abstraction-based verification. My approach relies on supplementary information from the applied abstraction when calculating dependencies between program operations. By abstracting the sources of dependency, certain operations are deemed independent, reducing interdependence within the model. Consequently, the effectiveness of partial order reduction is amplified.
+                \par
+                Calculating successor states in software model checking is costly, often requiring solving a Satisfiability Modulo Theories (SMT) problem. However, in many cases, the evaluation of a program statement does not affect the verified property. Successor state calculation can be simplified in such cases. Existing algorithms, such as the cone-of-influence reduction, statically analyze the program and eliminate irrelevant variables. In concurrent software, however, the result of a statement may be used in one interleaving of threads while unused in another. Algorithms that statically analyze the program cannot simplify such statements. My on-the-fly approach detects whether a statement can be simplified during the state space exploration based on the current state of each thread.
+                \par
+                Promising model checking approaches have been developed that encode the whole concurrent program and the verified property as an SMT problem, leaving the reasoning to the strength of SMT solvers. These methods for concurrent software verification ensure that events (variable accesses) of concurrent threads are consistently ordered. Inconsistencies in the form of cyclic precedence of concurrent events are detected and excluded. While SMT solvers are highly optimized, they remain general-purpose tools, leaving room for domain-specific optimization. I propose a domain-specific optimization to find scheduling inconsistencies and strengthen the encoding formula before starting the SMT-solving procedure. This way, the solver search space can be greatly reduced, and the overall verification performance can be significantly improved.},
+}