skip to main content
Idioma:

Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation

Miné, Antoine

Foundations and trends in programming languages, 2017-01, Vol.4 (3-4), p.120-372 [Periódico revisado por pares]

Boston - Delft: Now Publishers

Texto completo disponível

Citações Citado por
  • Título:
    Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation
  • Autor: Miné, Antoine
  • Assuntos: Abstract Interpretation ; Computer Science ; Computer software ; Program Verification ; Programming Languages ; Software engineering ; Static and Dynamic Program Analysis ; Technology ; Verification
  • É parte de: Foundations and trends in programming languages, 2017-01, Vol.4 (3-4), p.120-372
  • Notas: 11
    99
    978-1-68083-386-7
    Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation
    PGL-034
    10.1561/9781680833874
    260
    Now Publishers
    Foundations and Trends® in Programming Languages
    978-1-68083-387-4
  • Descrição: Born in the late 70s, Abstract Interpretation has proven an effective method to construct static analyzers. It has led to successful program analysis tools routinely used in avionic, automotive, and space industries to help ensuring the correctness of mission-critical software. This tutorial presents Abstract Interpretation and its use to create static analyzers that infer numeric invariants on programs. We first present the theoretical bases of Abstract Interpretation: how to assign a well-defined formal semantics to programs, construct computable approximations to derive effective analyzers, and ensure soundness, i.e., any property derived by the analyzer is true of all actual executions — although some properties may be missed due to approximations, a necessary compromise to keep the analysis automatic, sound, and terminating when inferring uncomputable properties.We describe the classic numeric abstractions readily available to an analysis designer: intervals, polyhedra, congruences, octagons, etc., as well as domain combiners: the reduced product and various disjunctive completions. This tutorial focuses not only on the semantic aspect, but also on the algorithmic one, providing a description of the data-structures and algorithms necessary to effectively implement all our abstractions. We will encounter many trade-offs between cost on the one hand, and precision and expressiveness on the other hand. Invariant inference is formalized on an idealized, toy-language, manipulating perfect numbers, but the principles and algorithms we present are effectively used in analyzers for real industrial programs, although this is out of the scope of this tutorial. This tutorial is intended as an entry course in Abstract Interpretation, after which the reader should be ready to read the research literature on current advances in Abstract Interpretation and on the design of static analyzers for real languages.
  • Editor: Boston - Delft: Now Publishers
  • Idioma: Inglês
Links
Voltar para lista de resultados
Ir para página anteriorAnterior Resultado  5 AvançarIr para próxima página

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.