@phdthesis{11362,
  abstract     = {Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks.
One exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. 
To deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. 
This can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks.

Our goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications.
This thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making.

First, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry.
We show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization.

Furthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable.
Our results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice.

Finally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic.
We introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only.
Our method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system.
We demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks.},
  author       = {Lechner, Mathias},
  isbn         = {978-3-99078-017-6},
  keywords     = {neural networks, verification, machine learning},
  pages        = {124},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Learning verifiable representations}},
  doi          = {10.15479/at:ista:11362},
  year         = {2022},
}

@inproceedings{10002,
  abstract     = {We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 .},
  author       = {Chatterjee, Krishnendu and Dvorak, Wolfgang and Henzinger, Monika H and Svozil, Alexander},
  booktitle    = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
  isbn         = {978-1-6654-4896-3},
  issn         = {1043-6871},
  keywords     = {Computer science, Computational modeling, Markov processes, Probabilistic logic, Formal verification, Game Theory},
  location     = {Rome, Italy},
  pages        = {1--13},
  publisher    = {Institute of Electrical and Electronics Engineers},
  title        = {{Symbolic time and space tradeoffs for probabilistic verification}},
  doi          = {10.1109/LICS52264.2021.9470739},
  year         = {2021},
}

@inproceedings{10108,
  abstract     = {We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.},
  author       = {Mühlböck, Fabian and Henzinger, Thomas A},
  booktitle    = {International Conference on Runtime Verification},
  isbn         = {978-3-030-88493-2},
  issn         = {1611-3349},
  keywords     = {run-time verification, software engineering, implicit specification},
  location     = {Virtual},
  pages        = {231--243},
  publisher    = {Springer Nature},
  title        = {{Differential monitoring}},
  doi          = {10.1007/978-3-030-88494-9_12},
  volume       = {12974},
  year         = {2021},
}

@phdthesis{10199,
  abstract     = {The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness.},
  author       = {Toman, Viktor},
  issn         = {2663-337X},
  keywords     = {concurrency, verification, model checking},
  pages        = {166},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Improved verification techniques for concurrent systems}},
  doi          = {10.15479/at:ista:10199},
  year         = {2021},
}

@misc{9946,
  abstract     = {We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.},
  author       = {Mühlböck, Fabian and Henzinger, Thomas A},
  issn         = {2664-1690},
  keywords     = {run-time verification, software engineering, implicit specification},
  pages        = {17},
  publisher    = {IST Austria},
  title        = {{Differential monitoring}},
  doi          = {10.15479/AT:ISTA:9946},
  year         = {2021},
}

@misc{5549,
  abstract     = {This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
We extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.
The archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.
To execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.
The archive contains scripts that (if run often enough) reproduces the data presented in the publication.},
  author       = {Fellner, Andreas},
  keywords     = {Markov Decision Process, Decision Tree, Probabilistic Verification, Counterexample Explanation},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes}},
  doi          = {10.15479/AT:ISTA:28},
  year         = {2015},
}