Search

When designing a tractable static analysis, one usually needs to approximate the trace semantics. This paper proposes a systematic way of regaining some knowledge about the traces by performing the abstraction over a partition of the set of traces instead of the set itself. This systematic refinement is not only theoretical but tractable: we give automatic procedures to build pertinent partitions of the traces and show the efficiency on an implementation integrated in the Astree static analyzer, a tool capable of dealing with industrial-size software.

We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software.The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization (Sect. 3 and 7), the symbolic manipulation of expressions to improve the precision of abstract transfer functions (Sect. 6.3), the octagon (Sect. 6.2.2), ellipsoid (Sect. 6.2.3), and decision tree (Sect. 6.2.4) abstract domains, all with sound handling of rounding errors in oating point computations, widening strategies (with thresholds: Sect. 7.1.2, delayed: Sect. 7.1.3) and the automatic determination of the parameters (parametrized packing: Sect. 7.2).

We present a method for analyzing assembly programs based on source program analysis and invariant translation. It is generic in the choice of an abstract domain for representing stores. This method is adapted to the design of certification tools for assembly programs generated by compiling programs written in an imperative language, without writing a specific compiler or modifying an existing one since invariant translation only uses standard debugging information. A prototype was developed for a procedural subset of the C language.

We report on a successful preliminary experience in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expansion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees.; Nous rapportons sur une expérience préliminaire fructueuse sur la conceptionet l'implantation d'un analyseur statique de programmes, basé sur l'interprétation abstraite, pour la vérification de l'absence d'erreurs à l'exécution dans des logiciels critiques embarqués temps-réel. L'analyseur est à la fois précis (aucune fausse alarme dans l'expérimentation considérée) et efficace (moins d'une minute de temps d'analyse pour 10 000 lignes de code). Même s'il est basé sur une simple analyse d'intervalles, de nombreuses extensions à cette analyse classique ont été introduites pour obtenir de telles performances : expansion des petits tableaux, élargissements étagés, dépliages de boucles, partitionnement de traces, relation entre compteurs de boucle et autres variables. L'efficacité de l'outil vient d'une représentation astucieuse des environnements abstraits basée sur des applications fonctionnelles implantées par des arbres binaires de recherche équilibrés.

We provide a context semantics for Multiplicative-Additive Linear Logic (MALL), together with proofnets whose reduction preserves semantics, where proofnet reduction is equated with cut-elimination on MALL sequents. The results extend the program of Gonthier, Abadi, and Levy, who provided a "geometry of optimal ?-reduction" (context semantics) for ?-calculus and Multiplicative-Exponential Linear Logic (MELL). We integrate three features: a semantics that uses buses to implement slicing; a proofnet technology that allows multidimensional boxes and generalized garbage, preserving the linearity of additive reduction; and finally, a read-back procedure that computes a cut-free proof from the semantics, a constructive companion to full abstraction theorems.

In order to achieve better precision of abstract interpretation-based static analysis, we introduce a new generic abstract domain, the trace partitioning abstract domain. We develop a theoretical framework allowing a wide range of instantiations of the domain, proving that all these instantiations give correct results. From this theoretical framework, we go into implementation details of a particular instance developed in the Astrée static analyzer. We show how the domain is automatically configured in Astrée and the gain and cost in terms of performance and precision.

Separation Logic brought a major breakthrough in the area of program verification. Since its introduction, Separation Logic has made its way into a number of practical tools that are used on a daily basis for verifying programs, ranging from operating systems kernels and file systems to data structures and graph algorithms. These programs are written in a wide variety of programming languages at different abstraction levels, ranging from machine code and assembly, to C, Java, OCaml, and Rust, just to name a few. Numerous extensions to Separation Logic have been proposed over the past two decades. In this habilitation manuscript, I present an overview of my own contributions---and that of my co-authors---over the period from 2009 to 2022. The manuscript is organized in three main parts. The first part describes a foundational set up of sequential Separation Logic, with the logic being proved sound with respect to a semantics mechanized in an interactive proof assistant. The presentation targets a imperative lambda-calculus, sufficiently minimalistic to allow for an easy-to-teach presentation of the theory, yet sufficiently rich to support the verification of realistic programs. The second part presents the technique of characteristic formulae, which enables smooth proofs of practical programs in a proof assistant. Compared with the characteristic formulae introduced in my PhD thesis, I here give a simplified presentation based on weakest preconditions and, most importantly, I show how to justify characteristic formulae in a foundational manner. The third part of this manuscript describes extensions to Separation Logic for resource analysis: time credits for establishing amortized execution bounds, big-O notation to support asymptotic reasoning, and space credits to establish space bounds in the presence of a garbage collector. The manuscript ends with two closing chapters. One provides a survey of publications on Separation Logic for sequential programs. The other covers research perspectives.

As software is an essential component of many embedded systems or online information systems, its malfunction can cause harm or security vulnerabilities. New bugs and vulnerabilities keep being discovered in existing software; many of those bugs and vulnerabilities are caused by violations of memory safety. In particular, low-level code, written in languages that offer few safety guarantees, is the most prone to this kind of bug. However, writing low-level code is sometimes necessary for performance or direct access to hardware features. Formal methods can be used to verify the safety of low-level programs, but automated analysis techniques to verify memory-related properties, such as shape analyses, still require important human effort, preventing wide adoption. In this thesis, we propose a practical automated analysis based on types that express structural invariants on memory down to the byte level. This analysis, which we formalize in the framework of abstract interpretation, offers a trade-off between precise, flow-sensitive shape analyses and scalable, flow-insensitive pointer analyses. It can be applied to low-level code with only a small amount of manual annotations. We show how the type-based abstraction can be complemented with retained and staged points-to predicates to handle precisely common low-level code patterns, such as data structure initialization. We demonstrate the effectiveness and practicality of the analysis by verifying the preservation of structural invariants (implying spatial memory safety) on C and machine code programs, showing that it can be helpful in eliminating an entire class of security vulnerabilities. We then apply our analysis to executables of embedded kernels and show that our type-based invariants allow to verify absence of runtime errors and absence of privilege escalation. To do this, we introduce the concept of implicit properties, i.e. properties which can be defined without reference to a specific program, and therefore lend themselves well to automated verification; and we prove that absence of privilege escalation is an implicit property. Parameterized verification, i.e. verification of the kernel independently from applicative code and data, poses many challenges, such as the need to summarize memory, or the dependence on a complex precondition on the initial state. We propose a methodology to solve them using our analysis technique. We apply this methodology to verify absence of runtime errors and absence of privilege escalation on a full, unmodified embedded kernel with a high level of automation.; Les logiciels étant des composants essentiels de nombreux systèmes embarqués et de nombreux systèmes d'information, un dysfonctionnement logiciel peut entraîner d'importants dommages ou des failles de sécurité. De nouveaux bugs et de nouvelles vulnérabilités sont trouvés régulièrement dans les programmes existants; une grande partie d'entre eux est causeé par des violations de la sûreté mémoire. En particulier, le code bas niveau, écrit dans des langages de programmation qui offrent peu de garanties de sûreté, est le plus susceptible de contenir ce type de bug. Malgré cela, écrire dans un langage bas niveau reste parfois nécessaire pour des raisons de performance, ou pour accéder directement aux fonctionnalités du matériel. Les méthodes formelles peuvent permettre de vérifier la sûreté des programmes bas niveau, mais les techniques automatisées de vérification de propriétés mémoire, telles que les analyses de forme, nécessitent encore un effort manuel im portant, ce qui est un obstacle à une adoption large. Dans cette thèse, nous proposons une analyse automatisée facilement applicable, basée sur un système de types exprimant des invariants structurels sur la mémoire, précis jusqu'au niveau de l'octet. Cette analyse, que nous formalisons dans le cadre de l'interprétation abstraite, offre un compromis entre les analyses de forme, précises et sensibles au flot de contrôle, et les analyses de pointeurs, qui sont insensibles au flot de contrôle mais passent très bien à l'échelle. Elle peut être appliquée à du code bas niveau avec peu d'annotations manuelles. Nous montrons comment cette analyse basée sur les types peut être complémentée par des prédicats de pointeurs conservés et reportés, afin de supporter précisément des motifs fréquents en code bas niveau tels que l'initialisation de structures de données. Nous démontrons l'efficacité et l'applicabilité de l'analyse en vérifiant la conservation d'invariants structurels (qui impliquent la sûreté mémoire spatiale) sur des program mes C et du code machine, montrant qu'elle peut être utile pour éliminer toute une classe de failles de sécurité. Nous appliquons ensuite notre analyse à des exécutables de noyaux embarqués, et nous montrons que nos invariants à base de types permettent de vérifier l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges. Pour cela, nous introduisons le concept de propriété implicite, c'est-à-dire de propriété qui peut être définie sans référence à un programme en particulier, qui se prêtent bien à la vérification automatique; et nous montrons que l'absence d'escalade de privilèges est une propriété implicite. La vérification paramétrée, c'est-à-dire la vérification de noyaux indépendamment du code et des données des applications, comporte plusieurs défis, comme le besoin de résumer la mémoire ou bien la dépendance à une précondition complexe sur l'état initial. Nous proposons une méthodologie pour les résoudre à l'aide de notre technique d'analyse. À l'aide de cette méthodologie, nous vérifions l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges su r un noyau entier sans modification, avec un haut niveau d'automatisation.

Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Relational analyses offer several advantages, such as their ability to infer semantics properties more expressive compared to state analyses. Moreover, they offer the ability to make the analysis compositional, using input-output relations as summaries for procedures, which is an advantage for scalability. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input-output memory states and taking shapes into account is challenging. In this Thesis, we propose a set of novel logical connectives to describe such relations, which rely on separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory is modified (and how). Using these connectives, we build an abstract domain and design a compositional static analysis by abstract interpretation that over-approximates relations over memory states containing inductive structures. We implement this approach as a plug-in of the FRAMA-C analyzer. We evaluate it on small programs written in C that manipulate singly linked lists and binary trees, but also on a bigger program that consists of a part of Emacs. The experimental results show that our approach allows us to infer more expressive semantic properties than states analyses, from a logical point of view. It is also much faster on programs with an important number of function calls without losing precision., Les analyses statiques ont pour but d’inférer des propriétés sémantiques de programmes. Nous distinguons deux importantes classes d’analyses statiques : les analyses d’états et les analyses relationnelles. Alors que les analyses d’états calculent une sur-approximation de l’ensemble des états atteignables d’un programme, les analyses relationnelles calculent des propriétés fonctionnelles entre les états d’entrée et les états de sortie d’un programme. Les analyses relationnelles offrent plusieurs avantages, comme leur capacité à inférer des propriétés sémantiques plus expressives par rapport aux analyses d’états. De plus, elles offrent également la possibilité de rendre l’analyse compositionnelle, en utilisant les relations entrée-sortie comme des résumés de procédures, ce qui est un avantage pour le passage à l’échelle. Dans le cas des programmes numériques, plusieurs analyses ont été proposées qui utilisent des domaines abstraits numériques relationnels, pour décrire des relations. D’un autre côté, modéliser des abstractions de relations entre les états mémoires entrée-sortie tout en prenant en compte les structures de données est difficile. Dans cette Thèse, nous proposons un ensemble de nouveaux connecteurs logiques, reposant sur la logique de séparation, pour décrire de telles relations. Ces connecteurs peuvent exprimer qu’une certaine partie de la mémoire est inchangée, fraîchement allouée, ou désallouée, ou que seulement une seule partie de la mémoire est modifiée (et de quelle manière). En utilisant ces connecteurs, nous construisons un domaine abstrait relationnel et nous concevons une analyse statique compositionnelle par interprétation abstraite qui sur-approxime des relations entre des états mémoires contenant des structures de données inductives. Nous avons implémenté ces contributions sous la forme d’un plug-in de l’analyseur FRAMA-C. Nous en avons évalué l’impact sur l’analyse de petits programmes écrits en C manipulant des listes chaînées et des arbres binaires, mais également sur l’analyse d’un programme plus conséquent qui consiste en une partie du code source d’Emacs. Nos résultats expérimentaux montrent que notre approche permet d’inférer des propriétés sémantiques plus expressives d’un point de vue logique que des analyses d’états. Elle se révèle aussi beaucoup plus rapide sur des programmes avec un nombre conséquent d’appels de fonctions sans pour autant perdre en précision.

Shape analyses rely on expressive families of logical properties to infer complex structural invariants, such that memory safety, structure preservation and other memory properties of programs dealing with dynamic data structures can be automatically verified. Many such analyses manipulate abstract memory states that consist of separating conjunctions of basic predicates describing atomic blocks or summary predicates that describe unbounded heap regions like lists or trees using inductive definitions. Moreover, they use finite disjunctions of abstract memory states in order to take into account dissimilar shapes. Although existing analyses enable local reasoning of memory regions, they do, however, have the following issues: (1) The summary predicates are not expressive enough to describe precisely all the dynamic data structures. In particular, a fairly large number of data structures with unbounded sharing, such as graphs, cannot be described inductively in a local manner; (2) Abstract operations that read or write into summaries rely on materialization of memory cells. The materialization operation in general creates new disjunctions, yet the size of disjunctions should be kept small for the sake of efficiency. However, local predicates are not enough to determine the right set of disjuncts that should be clumped together and to define precise abstract join and widen operations. In this thesis, we study separating conjunction-based shape predicates and the related abstract operations, in particular, abstract joining and widening operations that lead to critical modifications of abstract states. We seek a lightweight way to enable some global reasoning in existing shape analyses such that shape predicates are more expressive for abstracting data structures with unbounded sharing and disjuncts can be clumped precisely and efficiently. We propose a shape abstraction based on set variables that when integrated with inductive definitions enables the specification and shape analysis of structures with unbounded sharing. We implemented the shape analysis domain by combining a separation logic-based shape abstract domain of the MemCAD analyzer and a set abstract domain, where the set abstractions are used to track unbounded pointer sharing properties. Based on this abstract domain, we analyzed a group of programs dealing with adjacency lists of graphs. We design a general semantic criterion to clump abstract memory states based on their silhouettes that express global shape properties, \ie, clumping abstract states when their silhouettes are similar. Silhouettes apply not only to the conservative union of disjuncts but also to the weakening of separating conjunctions of memory predicates into inductive summaries. Our approach allows us to define union and widening operators that aim at preserving the case splits that are required for the analysis to succeed. We implement this approach in the MemCAD analyzer and evaluate it on real-world C libraries for different data structures, including doubly-linked lists, red-black trees, AVL-trees and splay-trees. The experimental results show that our approach is able to keep the size of disjunctions small for scalability and preserve case splits that takes into account dissimilar shapes for precision., L'analyse statique des programmes permet de calculer automatiquement des propriétés sémantiques valides pour toutes les exécutions. En particulier, dans le cas des programmes manipulant des structures de données complexes en mémoire, l'analyse statique peut inférer des invariants utiles pour prouver la sûreté des accès à la mémoire ou la préservation d'invariants structurels. Beaucoup d'analyses de ce type manipulent des états mémoires abstraits représentés par des conjonctions en logique de séparation dont les prédicats de base décrivent des blocs de mémoire atomiques ou bien résument des régions non-bornées de la mémoire telles que des listes ou des arbres. De telles analyses utilisent souvent des disjonctions finies d’états mémoires abstraits afin de mieux capturer leurs dissimilarités. Les analyses existantes permettent de raisonner localement sur les zones mémoires mais présentent les inconvénients suivants: (1) Les prédicats inductifs ne sont pas assez expressifs pour décrire précisément toutes les structures de données dynamiques, du fait de la présence de pointeurs vers des parties arbitraires (i.e., non-locales) de ces structures ; (2) Les opérations abstraites correspondant à des accès en lecture ou en écriture sur ces prédicats inductifs reposent sur une opération matérialisant les cellules mémoires correspondantes. Cette opération de matérialisation crée en général de nouvelles disjonctions, ce qui nuit à l'impératif d'efficacité. Hélas, les prédicats exprimant des contraintes de structure locale ne sont pas suffisants pour déterminer de façon adéquate les ensembles de disjonctions devant être fusionnés, ni pour définir les opérations d'union et d'élargissement d'états abstraits. Cette thèse est consacrée à l'étude et la mise au point de prédicats en logique de séparation permettant de décrire des structures de données dynamiques, ainsi que des opérations abstraites afférentes. Nous portons une attention particulière aux opérations d'union et d'élargissement d’états abstraits. Nous proposons une méthode pratique permettant de raisonner globalement sur ces états mémoires au sein des méthodes existantes d'analyse de propriétés structurelles et autorisant la fusion précise et efficace de disjonctions. Nous proposons et implémentons une abstraction structurelle basée sur les variables d'ensembles qui lorsque elle est utilisée conjointement avec les prédicats inductifs permet la spécification et l'analyse de propriétés structurelles globales. Nous avons utilisé ce domaine abstrait afin d'analyser une famille de programmes manipulant des graphes représentés par liste d'adjacence. Nous proposons un critère sémantique permettant de fusionner les états mémoires abstraits similaires en se basant sur leur silhouette, cette dernière représentant certaines propriétés structurelles globales vérifiées par l'état correspondant. Les silhouettes s'appliquent non seulement à la fusion de termes dans les disjonctions d'états mémoires mais également à l'affaiblissement de conjonctions de prédicats de logique de séparation en prédicats inductifs. Ces contributions nous permettent de définir des opérateurs d’union et d'élargissement visant à préserver les disjonctions requises pour que l'analyse se termine avec succès. Nous avons implémenté ces contributions au sein de l'analyseur MemCAD et nous en avons évaluées l'impact sur l'analyse de bibliothèques existantes écrites en C et implémentant différentes structures de données, incluant des listes doublement chaînées, des arbres rouge-noir, des arbres AVL et des arbres "splay". Nos résultats expérimentaux montrent que notre approche est à même de contrôler la taille des disjonctions à des fins de performance sans pour autant nuire à la précision de l'analyse.

We study the static analysis on both numeric and structural properties of array contents in the framework of abstract interpretation. Since arrays are ubiquitous in most software systems, and software defects related to mis-uses of arrays are hard to avoid in practice, a lot of efforts have been devoted to ensuring the correctness of programs manipulating arrays. Current verification of these programs by static analysis focuses on numeric content properties. However, in some lowlevel programs (like embedded systems or real-time operating systems), arrays often contain structural data (e.g., lists) without using dynamic allocation. In this manuscript, we present a series of techniques to verify both numeric and structural properties of array contents. Our first technique is used to describe properties of numerical stores with optional values (i.e., where some variables may have no value) or sets of values (i.e., where some variables may store a possibly empty set of values). Our approach lifts numerical abstract domains based on common linear inequality into abstract domains describing stores with optional values and sets of values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded memory blocks like in arrays. Our second technique is an abstract domain which utilizes semantic properties to split array cells into groups. Cells with similar properties will be packed into groups and abstracted together. Additionally, groups are not necessarily contiguous. Compared to conventional array partitioning analyses that split arrays into contiguous partitions to infer properties of sets of array cells. Our analysis can group together non-contiguous cells when they have similar properties. Our abstract domain can infer complex array invariants in a fully automatic way. The third technique is used to combine different shape domains. This combination locally ties summaries in both abstract domains and is called a coalesced abstraction. Coalescing allows to define efficient and precise static analysis algorithms in the combined domain. We utilize it to combine our array abstraction (i.e., our second technique) and a shape abstraction which captures linked structures with separation logicbased inductive predicates. The product domain can verify both safety and functional properties of programs manipulating arrays storing dynamically linked structures, such as lists. Storing dynamic structures in arrays is a programming pattern commonly used in low-level systems, so as to avoid relying on dynamic allocation. The verification of such programs is very challenging as it requires reasoning both about the array structure with numeric indexes and about the linked structures stored in the array. Combining the three techniques that we have proposed, we can build an automatic static analysis for the verification of programs manipulating arrays storing linked structures. We report on the successful verification of several operating system kernel components and drivers., Dans cette thèse, nous étudions l'analyse statique par interprétation abstraites de programmes manipulant des tableaux, afin d'inférer des propriétés sur les valeurs numériques et les structures de données qui y sont stockées. Les tableaux sont omniprésents dans de nombreux programmes, et les erreurs liées à leur manipulation sont difficile à éviter en pratique. De nombreux travaux de recherche ont été consacrés à la vérification de tels programmes. Les travaux existants s'intéressent plus particulièrement aux propriétés concernant les valeurs numériques stockées dans les tableaux. Toutefois, les programmes bas-niveau (comme les systèmes embarqués ou les systèmes d'exploitation temps réel) utilisent souvent des tableaux afin d'y stocker des structures de données telles que des listes, de manière à éviter d'avoir recours à l'allocation de mémoire dynamique. Dans cette thèse, nous présentons des techniques permettant de vérifier par interprétation abstraite des propriétés concernant à la fois les données numériques ainsi que les structures composites stockées dans des tableaux. Notre première contribution est une abstraction qui permet de décrire des stores à valeurs numériques et avec valeurs optionnelles (i.e., lorsqu'une variable peut soit avoir une valeur numérique, soit ne pas avoir de valeur du tout), ou bien avec valeurs ensemblistes (i.e., lorsqu'une variable est associée à un ensemble de valeurs qui peut être vide ou non). Cette abstraction peut être utilisée pour décrire des stores où certaines variables ont un type option, ou bien un type ensembliste. Elle peut aussi servir à la construction de domaines abstraits pour décrire des propriétés complexes à l'aide de variables symboliques, par exemple, pour résumer le contenu de zones dans des tableaux. Notre seconde contribution est un domaine abstrait pour la description de tableaux, qui utilise des propriétés sémantiques des valeurs contenues afin de partitionner les cellules de tableaux en groupes homogènes. Ainsi, des cellules contenant des valeurs similaires sont décrites par les mêmes prédicats abstraits. De plus, au contraire des analyses de tableaux conventionnelles, les groupes ainsi formés ne sont pas nécessairement contigüs, ce qui contribue à la généralité de l'analyse. Notre analyse peut regrouper des cellules non-congitües, lorsque celles-ci ont des propriétés similaires. Ce domaine abstrait permet de construire des analyses complètement automatiques et capables d'inférer des invariants complexes sur les tableaux. Notre troisième contribution repose sur une combinaison de cette abstraction des tableaux avec différents domaines abstraits issus de l'analyse de forme des structures de données et reposant sur la logique de séparation. Cette combinaison appelée coalescence opère localement, et relie des résumés pour des structures dynamiques à des groupes de cellules du tableau. La coalescence permet de définir de manière locale des algorithmes d'analyse statique dans le domaine combiné. Nous l'utilisons pour relier notre domaine abstrait pour tableaux et une analyse de forme générique, dont la tâche est de décrire des structures chaînées. L'analyse ainsi obtenue peut vérifier à la fois des propriétés de sûreté et des propriétés de correction fonctionnelle. De nombreux programmes bas-niveau stockent des structures dynamiques chaînées dans des tableaux afin de n'utiliser que des zones mémoire allouées statiquement. La vérification de tels programmes est difficile, puisqu'elle nécessite à la fois de raisonner sur les tableaux et sur les structures chaînées. Nous construisons une analyse statique reposant sur ces trois contributions, et permettant d'analyser avec succés de tels programmes. Nous présentons des résultats d'analyse permettant la vérification de composants de systèmes d'exploitation et pilotes de périphériques.

International audience; Automatically verifying safety properties of programs is hard.Many approaches exist for verifying programs operating on Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties.Our work addresses that issue with a powerful and flexible abstractionthat morphes concrete array cells into a finite set of abstractones. This abstraction is parametric both in precision and in theback-end analysis used.From our programs with arrays, we generate nonlinear Horn clauses overscalar variables only, in a common format with clear and unambiguouslogical semantics, for which there exist several solvers. We thusavoid the use of solvers operating over arrays, which are still veryimmature.Experiments with our prototype VAPHOR show that this approach can proveautomatically and without user annotationsthe functional correctness of several classical examples, including \emph{selection sort}, \emph{bubble sort}, \emph{insertion sort}, as well as examples from literature on array analysis.

International audience; Termination of loops can be inferred from the existence of linear ranking functions. We already know that the existence of thesefunctions is PTIME decidable for simple rational loops. Since very recently, we know that the problem is coNP-complete for simple integer loops. We continue along this path by investigating programs dealing with floating-point computations. First, we show that the problem is at least in coNP for simple floating-point loops. Then, in order to work around that theoretical limitation we present an algorithm which remains polynomial by sacrificing completeness. The algorithm, based on the Podelski-Rybalchenko algorithm, can also synthesize in polynomial time the linear ranking functions it detects. To our knowledge, our work is the first adaptation of this well-known algorithm to floating-points.

International audience; Semidefinite programming (SDP) solvers are increasingly used as primitives in many program verification tasks to synthesize and verify polynomial invariants for a variety of systems including programs, hybrid systems and stochastic models. On one hand, they provide a tractable alternative to reasoning about semi-algebraic constraints. However, the results are often unreliable due to " numerical issues " that include a large number of reasons such as floating-point errors, ill-conditioned problems, failure of strict feasibility, and more generally, the specifics of the algorithms used to solve SDPs. These issues influence whether the final numerical results are trustworthy or not. In this paper, we briefly survey the emerging use of SDP solvers in the static analysis community. We report on the perils of using SDP solvers for common invariant synthesis tasks, characterizing the common failures that can lead to unreliable answers. Next, we demonstrate existing tools for guaranteed semidefinite programming that often prove inadequate to our needs. Finally, we present a solution for verified semidefinite programming that can be used to check the reliability of the solution output by the solver and a padding procedure that can check the presence of a feasible nearby solution to the one output by the solver. We report on some successful preliminary experiments involving our padding procedure.

Expressions are multilinear when variable occurrences are linear and products have factors using different variables. We demonstrate that multilinear expressions are either constant or have never a local minimum or a local maximum. Therefore the interval of multilinear expressions may be computed precisely studying their values at the bounds of the variables therein. We then propose a technique for the interval analysis of generic expressions that transforms them into multilinear ones and computes the interval of the latters.

International audience; We study thread-modular static analysis by abstract interpretation to infer the values of variables in concurrent programs. We show how to go beyond the state of the art and increase an analysis precision by adding the ability to infer some relational and history-sensitive properties of thread interferences. The fundamental basis of this work is the formalization by abstract interpretation of a rely-guarantee concrete semantics which is thread-modular, constructive, and complete for safety properties. We then show that previous analyses based on non-relational interferences can be retrieved as coarse computable abstractions of this semantics; additionally, we present novel abstraction examples exploiting our ability to reason more precisely about interferences, including domains to infer relational lock invariants and the monotonicity of counters. Our method and domains have been implemented in the AstréeA static analyzer that checks for run-time errors in embedded concurrent C programs, where they enabled a significant reduction of the number of false alarms.

International audience; This book constitutes the refereed proceedings of the 15th International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI 2014, held in San Diego, CA, USA, in January 2013. The 25 revised full papers presented were carefully reviewed and selected from 64 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.

This paper contributes to a new abstract domain that combines static numeric analysis and points-to analysis. One particularity of this abstract domain lies in its high degree of modularity, in the sense that the domain is constructed by reusing its combined components as black-boxes. This modularity dramatically eases the proof of its soundness and renders its algorithm intuitive. We have prototyped the abstract domain for analyzing real-world Java programs. Our experimental results show a tangible precision enhancement compared to what is possible by traditional static numeric analysis, and this at a cost that is comparable to the cost of running the numeric and pointer analyses separately.