ABSTRACT. In order to synthesize automatically a controller satisfying a specification given in GR(1) (a subset of linear temporal logic), the environment, where the controller is expected to operate, needs to be characterized by a sufficient set of GR(1) assumptions. Assumptions refinement procedures identify alternative sets of assumptions that make controller synthesis possible. However, since assumptions spaces are intractably large, techniques to explore a subset of them in a guided fashion are needed. In particular, it is important to identify weakest assumptions refinements to avoid overconstraining the environments and hence deeming the controller to be inadequate. The objective of my research is to devise a heuristic search approach that uses estimates of goodness of explored assumptions to direct the search towards better solutions. The work involves defining computable metrics that capture quality features of assumptions (such as their weakness), and automated ways to select a good subset of refinements in the search procedure.

ABSTRACT. Since a few years neural networks are the most powerful tool for perception tasks, especially in image processing, and superior performances in these tasks sparked the desire to use them in safety-critical systems, e.g., autonomous vehicles. However, verifying the safety of systems that are using neural networks remains a challenge, because neural networks raise certain dependability concerns (such as adversarial inputs). Resulting from this need, the research topic of formal verification of neural networks emerged. We identify some of the main challenges of this field and discuss how to address them.

ABSTRACT. Many complex applications which have to tackle simulation and data analysis are a prerogative to High-Performance Computing. And so, high data volumes and performance requirements have held the parallel community developers with a clasp to deliver scalable, accurate, and most importantly bug-free solutions. Message Passing (MP) is a prominent programming model via which nodes of a distributed system communicate. Writing correct and bug-free parallel programs are hard because the participating entities interact in such non-deterministic ways that are difficult to anticipate before-hand. Programmers have to predict messaging patterns, perform data marshaling and compute locations for coordination in order to design correct and efficient programs. Unfortunately, there is a shortage of verification and formal-method techniques that can guarantee the development of correct solutions.

ABSTRACT. Requirements are informal and semi-formal descriptions of the expected behavior of a system. They are usually expressed in the form of natural language sentences and checked for errors manually, \textit{e.g.}, by peer reviews. However, manual checks are error-prone and time-consuming. With the increasing complexity of cyber-physical systems and the need of operating in safety- and security-critical environments, it became essential to automatize the consistency check of requirements and build artifacts to help system engineers in the design process.