ABSTRACT. TBA

ABSTRACT. In this talk, I will present Cubicle, a model checker for verifying safety properties of array-based systems, a syntactically restricted class of para­metrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. After a short presentation of the semantics of its input language, I will present some details about its implementation, mainly its symbolic backward reachability analysis which makes use of Satisfiabilty Modulo Theories.  I will conclude with a presentation of current and future works.

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. 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. 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. 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.

ABSTRACT. Mobile Ad-hoc Networks (MANETs) are self-organising networks that provide support for broadband communication, and have gained popularity in a wide range of application areas, such as public safety, emergency response networks, etc. Routing protocols of these networks provide the ground for nodes communication and finding routes which are later used for sending data packets to different destinations. Formal methods are used for formal modelling and verification of such protocols to ensure correctness and precision of design due to safety critical applications of MANETs. In this work, we sketch our different formal studies on MANET routing protocols.