<div>In this thesis, we explore different methods to enhance the safety and robustness for autonomous systems. We achieve this goal using concepts and tools from reachability analysis and control barrier functions. We first take on a multi-player reach-avoid game that involves two teams of players with competing objectives, namely the attackers and the defenders. We analyze the problem and solve the game from the attackers' perspectives via a moving horizon approach. The resulting solution provides a safety guarantee that allows attackers to reach their goals while avoiding all defenders. </div><div><br></div><div>Next, we approach the problem of target re-association after long-term occlusion using concepts from reachability as well as Bayesian inference. Here, we set out to find the probability identity matrix that associates the identities of targets before and after an occlusion. The solution of this problem can be used in conjunction with existing state-of-the-art trackers to enhance their robustness.</div><div><br></div><div>Finally, we turn our attention to a different method for providing safety guarantees, namely control barrier functions. Since the existence of a control barrier function implies the safety of a control system, we propose a framework to learn such function from a given user-specified safety requirement. The learned CBF can be applied on top of an existing nominal controller to provide safety guarantees for systems.</div>

Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.

No description available.

Les travaux présentés dans cette thèse sont lies aux problèmes de vérification de l'atteignabilité et de la terminaison de programmes qui manipulent des données entières non-bornées. On décrit une nouvelle méthode de vérification basée sur une technique d'accélération de boucle, qui calcule, de manière exacte, la clôture transitive d'une relation arithmétique. D'abord, on introduit un algorithme d'accélération de boucle qui peut calculer, en quelques secondes, des clôtures transitives pour des relations de l'ordre d'une centaine de variables. Ensuite, on présente une méthode d'analyse de l'atteignabilité, qui manipule des relations entre les variables entières d'un programme, et applique l'accélération pour le calcul des relations entrée-sortie des procédures, de façon modulaire. Une approche alternative pour l'analyse de l'atteignabilité, présentée également dans cette thèse, intègre l'accélération avec l'abstraction par prédicats, afin de traiter le problème de divergence de cette dernière. Ces deux méthodes ont été évaluées de manière pratique, sur un nombre important d'exemples, qui étaient, jusqu'a présent, hors de la portée des outils d'analyse existants. Dernièrement, on a étudié le problème de la terminaison pour certaines classes de boucles de programme, et on a montré la décidabilité pour les relations étudiées. Pour ces classes de relations arithmétiques, on présente un algorithme qui s'exécute en temps au plus polynomial, et qui calcule l'ensemble d'états qui peuvent générer une exécution infinie. Ensuite on a intégré cet algorithme dans une méthode d'analyse de la terminaison pour des programmes qui manipulent des données entières. / This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which non-terminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs. / Tato pr´ace pˇredstavuje nov´e metody pro verifikaci program°u pracuj´ıc´ıch s neomezen´ymiceloˇc´ıslen´ymi promˇenn´ymi, konkr´etnˇe metody pro anal´yzu dosaˇzitelnosti a koneˇcnosti.Vˇetˇsina tˇechto metod je zaloˇzena na akceleraˇcn´ıch technik´ach, kter´e poˇc´ıtaj´ı tranzitivn´ıuz´avˇery cykl°u programu.V pr´aci je nejprve pˇredstaven algoritmus pro akceleraci nˇekolika tˇr´ıd celoˇc´ıseln´ychrelac´ı. Tento algoritmus je aˇz o ˇctyˇri ˇr´ady rychlejˇs´ı neˇz existuj´ıc´ı techniky. Z teoretick´ehohlediska pr´ace dokazuje, ˇze uvaˇzovan´e tˇr´ıdy relac´ı jsou periodick´e a poskytuje tud´ıˇzjednotn´e ˇreˇsen´ı prol´emu akcelerace.Pr´ace d´ale pˇredstavuje semi-algoritmus pro anal´yzu dosaˇzitelnosti celoˇc´ıseln´ych program°u, kter´y sleduje relace mezi promˇenn´ymi programu a aplikuje akceleraˇcn´ı technikyza ´uˇcelem modul´arn´ıho v´ypoˇctu souhrn°u procedur. D´ale je v pr´aci navrˇzen alternativn´ıalgoritmus pro anal´yzu dosaˇzitelnosti, kter´y integruje predik´atovou abstrakci s accelerac´ıs c´ılem zv´yˇsit pravdˇepodobnost konvergence v´ypoˇctu. Proveden´e experimenty ukazuj´ı, ˇzeoba algoritmy lze ´uspˇeˇsnˇe aplikovat k verifikaci program°u, na kter´ych pˇredchoz´ı metodyselh´avaly.Pr´ace se rovnˇeˇz zab´yv´a probl´emem koneˇcnosti bˇehu program°u a dokazuje, ˇze tentoprobl´em je rozhodnuteln´y pro nˇekolik tˇr´ıd celoˇc´ıseln´ych relac´ı. Pro nˇekter´e z tˇechto tˇr´ıdrelac´ı je v pr´aci navrˇzen algoritmus, kter´y v polynomi´aln´ım ˇcase vypoˇc´ıt´a mnoˇzinu vˇsechkonfigurac´ı programu, z nichˇz existuje nekoneˇcn´y bˇeh. Tento algoritmus je integrov´ando metody, kter´a analyzuje koneˇcnost bˇeh°u celoˇc´ıseln´ych program°u. Efektivnost t´etometody je demonstrov´ana na nˇekolika netrivi´aln´ıch celoˇc´ıseln´ych programech.

The area of formal analysis of cryptographic protocols has been an active one since the mid 80’s. The idea is to verify communication protocols that use encryption to guarantee secrecy and that use authentication of data to ensure security. Formal methods are used in protocol analysis to provide formal proofs of security, and to uncover bugs and security flaws that in some cases had remained unknown long after the original protocol publication, such as the case of the well known Needham-Schroeder Public Key (NSPK) protocol. In this thesis we tackle problems regarding the three main pillars of protocol verification: modelling capabilities, verifiable properties, and efficiency. This thesis is devoted to investigate advanced features in the analysis of cryptographic protocols tailored to the Maude-NPA tool. This tool is a model-checker for cryptographic protocol analysis that allows for the incorporation of different equational theories and operates in the unbounded session model without the use of data or control abstraction. An important contribution of this thesis is relative to theoretical aspects of protocol verification in Maude-NPA. First, we define a forwards operational semantics, using rewriting logic as the theoretical framework and the Maude programming language as tool support. This is the first time that a forwards rewriting-based semantics is given for Maude-NPA. Second, we also study the problem that arises in cryptographic protocol analysis when it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the protocol equational theory. We also study techniques to extend Maude-NPA capabilities to support the verification of a wider class of protocols and security properties. First, we present a framework to specify and verify sequential protocol compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a theoretical framework to specify and verify protocol indistinguishability in Maude-NPA. This kind of properties aim to verify that an attacker cannot distinguish between two versions of a protocol: for example, one using one secret and one using another, as it happens in electronic voting protocols. Finally, this thesis contributes to improve the efficiency of protocol verification in Maude-NPA. We define several techniques which drastically reduce the state space, and can often yield a finite state space, so that whether the desired security property holds or not can in fact be decided automatically, in spite of the general undecidability of such problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral no publicada]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527 / TESIS

<p>Set-based methods have been leveraged in many engineering applications from robust control and global optimization, to probabilistic planning and estimation. While useful, these methods have most widely been applied to analysis over sets that are convex, due to their ease in both representation and calculation. The representation and analysis of nonconvex sets is inherently complex. When nonconvexity arises in design and control applications, the nonconvex set is often over-approximated by a convex set to provide conservative results. However, the level of conservatism may be large and difficult to quantify, often leading to trivial results and requiring repetitive analysis by the engineer. Nonconvexity is inherent and unavoidable in many applications, such as the analysis of hybrid systems and robust safety constraints. </p> <p>In this dissertation, I present a new nonconvex set representation named the hybrid zonotope. The hybrid zonotope builds upon a combination of recent advances in the compact representation of convex sets in the controls literature with methods leveraged in solving mixed-integer programming problems. It is shown that the hybrid zonotope is equivalent to the union of an exponential number of convex sets while using a linear number of continuous and binary variables in the set’s representation. I provide identities for, and derivations of, the set operations of hybrid zonotopes for linear mappings, Minkowski sums, generalized intersections, halfspace intersections, Cartesian products, unions, complements, point containment, set containment, support functions, and convex enclosures. I also provide methods for redundancy removal and order reduction to improve the compactness and computational efficiency of the represented sets. Therefore proving the hybrid zonotopes expressive power and applicability to many nonconvex set-theoretic methods. Beyond basic set operations, I specifically show how the exact forward and backward reachable sets of linear hybrid systems may be found using identities that are calculated algebraically and scale linearly. Numerical examples show the scalability of the proposed methods and how they may be used to verify the safety and performance of complex systems. These exact methods may also be used to evaluate the level of conservatism of the existing approximate methods provided in the literature.  </p>