path: root/doc/ppl_citations.bib

A bibliography of papers that cite the Parma Polyhedra Library
and/or the works that defined the theory upon which it is based.
Copyright (C) 2001-2010 Roberto Bagnara <bagnara AT cs.unipr.it>
Copyright (C) 2010-2013 BUGSENG srl (http://bugseng.com)

This BibTeX database is made available under the Open Data Commons
Attribution License (ODC-By) v1.0, which is reproduced below for your
convenience and available at http://opendatacommons.org/licenses/by/1.0/
Summarizing:

- You are free: to copy, distribute and use the database;  to produce
  works from the database;  to modify, transform and build upon the database.

- You must attribute any public use of the database, or works produced
  from the database, in the manner specified in the license.  For any
  use or redistribution of the database, or works produced from it,
  you must make clear to others the license of the database and keep
  intact any notices on the original database.


@Inproceedings{AlbertACGPZ08,
  Author = "E. Albert and P. Arenas and M. Codish and S. Genaim
            and G. Puebla and D. Zanardini",
  Title = "Termination Analysis of {Java} Bytecode",
  Booktitle = "Proceedings of the 10th IFIP WG 6.1 International Conference
               on Formal Methods for Open Object-Based Distributed Systems
               (FMOODS 2008)",
  Address = "Oslo, Norway",
  Editor = "G. Barthe and F. S. de Boer",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5051,
  Year = 2008,
  Pages = "2--18",
  ISBN = "978-3-540-68862-4",
  Abstract = "Termination analysis has received considerable
              attention, traditionally in the context of declarative
              programming, and recently also for imperative
              languages. In existing approaches, termination is
              performed on source programs. However, there are many
              situations, including mobile code, where only the
              compiled code is available. In this work we present an
              automatic termination analysis for sequential Java
              Bytecode programs. Such analysis presents all of the
              challenges of analyzing a low-level language as well as
              those introduced by object-oriented languages.
              Interestingly, given a bytecode program, we produce a
              \emph{constraint logic program}, CLP, whose termination
              entails termination of the bytecode program. This allows
              applying the large body of work in termination of CLP
              programs to termination of Java bytecode. A prototype
              analyzer is described and initial experimentation is
              reported."
}

@Article{AlbertACGPZ12,
  Author = "E. Albert and P. Arenas and S. Genaim and G. Puebla
            and D. Zanardini",
  Title = "Cost Analysis of Object-Oriented Bytecode Programs",
  Journal = "Theoretical Computer Science",
  Volume = 413,
  Number = 1,
  Pages =  "142--159",
  Year = 2012,
  Note = "Quantitative Aspects of Programming Languages (QAPL 2010)",
  ISSN = "0304-3975",
  URL = "http://www.sciencedirect.com/science/article/pii/S0304397511006190",
  Abstract = "Cost analysis statically approximates the cost of
              programs in terms of their input data size. This paper
              presents, to the best of our knowledge, the first
              approach to the automatic cost analysis of
              object-oriented bytecode programs. In languages such as
              Java and C#, analyzing bytecode has a much wider
              application area than analyzing source code since the
              latter is often not available. Cost analysis in this
              context has to consider, among others, dynamic dispatch,
              jumps, the operand stack, and the heap. Our method takes
              a bytecode program and a cost model specifying the
              resource of interest, and generates cost relations which
              approximate the execution cost of the program with
              respect to such resource. We report on COSTA, an
              implementation for Java bytecode which can obtain upper
              bounds on cost for a large class of programs and
              complexity classes. Our basic techniques can be directly
              applied to infer cost relations for other
              object-oriented imperative languages, not necessarily in
              bytecode form."
}

@Inproceedings{AlbertAGP08,
  Author = "E. Albert and P. Arenas and S. Genaim and G. Puebla",
  Title = "Automatic Inference of Upper Bounds for Recurrence Relations
           in Cost Analysis",
  Booktitle = "Static Analysis:
               Proceedings of the 15th International Symposium",
  Address   = "Valencia, Spain",
  Editor = "M. Alpuente and G. Vidal",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5079,
  Year = 2008,
  Pages = "221--237",
  ISBN = "978-3-540-69163-1",
  Abstract = "The classical approach to automatic cost analysis
              consists of two phases. Given a program and some measure
              of cost, we first produce \emph{recurrence relations}
              (RRs) which capture the cost of our program in terms of
              the size of its input data. Second, we convert such RRs
              into \emph{closed form} (i.e., without
              recurrences). Whereas the first phase has received
              considerable attention, with a number of cost analyses
              available for a variety of programming languages, the
              second phase has received comparatively little
              attention. In this paper we first study the features of
              RRs generated by automatic cost analysis and discuss why
              existing computer algebra systems are not appropriate
              for automatically obtaining closed form solutions nor
              upper bounds of them. Then we present, to our knowledge,
              the first practical framework for the fully automatic
              generation of reasonably accurate upper bounds of RRs
              originating from cost analysis of a wide range of
              programs. It is based on the inference of \emph{ranking
              functions} and \emph{loop invariants} and on
              \emph{partial evaluation}."
}

@Incollection{AlbertAGPZ08,
  Author = "E. Albert and P. Arenas and S. Genaim
            and G. Puebla and D. Zanardini",
  Title = "{COSTA}: Design and Implementation of a Cost and Termination
           Analyzer for {Java} Bytecode",
  Booktitle = "Formal Methods for Components and Objects",
  Editor = "Frank S. {de Boer} and M. M. Bonsangue
            and S. Graf and W. P. {de Roever}",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Year = 2008,
  Volume = 5382,
  Pages = "113--132",
  ISBN = "978-3-540-92187-5",
  Note = "Revised papers presented at the 6th International Symposium on
          Formal Methods for Components and Objects (FMCO 2007),
          Amsterdam, The Netherlands, October 24--26, 2007",
  Abstract = "This paper describes the architecture of COSTA, an
              abstract interpretation based COST and termination
              Analyzer for Java bytecode.  The system receives as
              input a bytecode program, (a choice of) a
              \emph{resource} of interest and tries to obtain an upper
              bound of the resource consumption of the program. COSTA
              provides several non-trivial notions of cost, as the
              consumption of the heap, the number of bytecode
              instructions executed and the number of calls to a
              specific method. Additionally, COSTA tries to prove
              \emph{termination} of the bytecode program which implies
              the boundedness of any resource consumption. Having cost
              and termination together is interesting, as both
              analyses share most of the machinery to, respectively,
              infer cost \emph{upper bounds} and to prove that the
              execution length is always \emph{finite} (i.e., the
              program terminates). We report on experimental results
              which show that COSTA can deal with programs of
              realistic size and complexity, including programs which
              use Java libraries.  To the best of our knowledge, this
              system provides for the first time evidence that
              resource usage analysis can be applied to a realistic
              object-oriented, bytecode programming language."
}

@Inproceedings{AlbertAPCFGGMPRRZ13,
  Author = "E. Albert and D. E. Alonso-Blas and A. Puri and J. Correas and A. Flores-Montoya and S. Genaim and M. G{\'o}mez-Zamalloa and A. N. Masud and G. Puebla and J. M. Rojas and G. Rom{\'a}n-D{\'i}ez and D. Zanardini",
  Title = "Automatic Inference of Bounds on Resource Consumption",
  Booktitle = "Formal Methods for Components and Objects, 11th International Symposium, {FMCO} 2012",
  Address   = "Bertinoro, Italy",
  Editor = "E. Giachino and R. H{\"a}hnle and F. S. de Boer and M. M. Bonsangue",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7866,
  Year = 2013,
  Pages = "119--144",
  ISBN = "978-3-642-40614-0 (Print) 978-3-642-40615-7 (Online)",
  Abstract = "In this tutorial paper, we overview the techniques that
              underlie the automatic inference of resource consumption
              bounds. We first explain the basic techniques on a
              Java-like sequential language. Then, we describe the
              extensions that are required to apply our method on
              concurrent ABS programs. Finally, we discuss some
              advanced issues in resource analysis, including the
              inference of non-cumulative resources and the treatment
              of shared mutable data."
}

@Article{AlbertGM13,
  Author = "E. Albert and S. Genaim and A. N. Masud",
  Title = "On the Inference of Resource Usage Upper and Lower Bounds",
  Journal = "ACM Transactions on Computational Logic",
  Volume = 14,
  Number = 3,
  Year = 2013,
  Abstract = "Cost analysis aims at determining the amount of
              resources required to run a program in terms of its
              input data sizes. The most challenging step is to infer
              the cost of executing the loops in the program. This
              requires bounding the number of iterations of each loop
              and findig tight bounds for the cost of each of its
              iterations. This article presents a novel approach to
              infer upper and lower bounds from cost relations. These
              relations are an extended form of standard recurrence
              equations that can be nondeterministic, contain inexact
              size constraints and have multiple arguments that
              increase and/or decrease. We propose novel techniques to
              automatically transform cost relations into worst-case
              and best-case deterministic one-argument recurrence
              relations. The solution of each recursive relation
              provides a precise upper-bound and lower-bound for
              executing a corresponding loop in the
              program. Importantly, since the approach is developed at
              the level of the cost equations, our techniques are
              programming language independent."
}

@Inproceedings{AlonsoAG11,
  Author = "D. Alonso and P. Arenas and S. Genaim",
  Title = "Handling Non-linear Operations in the Value Analysis of {COSTA}",
  Booktitle = "Proceedings of the 6th Workshop on Bytecode Semantics,
               Verification, Analysis and Transformation (Bytecode 2011)",
  Address = "Saarbrucken, Germany",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 279,
  Number = 1,
  Pages = "3--17",
  Year = 2011,
  ISSN = "1571-0661",
  Abstract = "Inferring precise relations between (the values of)
              program variables at different program points is
              essential for termination and resource usage
              analysis. In both cases, this information is used to
              synthesize ranking functions that imply the program's
              termination and bound the number of iterations of its
              loops. For efficiency, it is common to base value
              analysis on non-disjunctive abstract domains such as
              Polyhedra, Octagon, etc. While these domains are
              efficient and able to infer complex relations for a wide
              class of programs, they are often not sufficient for
              modeling the effect of non-linear and bit arithmetic
              operations. Modeling such operations precisely can be
              done by using more sophisticated abstract domains, at
              the price of performance overhead. In this paper we
              report on the value analysis of COSTA that is based on
              the idea of encoding the disjunctive nature of
              non-linear operations into the (abstract) program
              itself, instead of using more sophisticated abstract
              domains. Our experiments demonstrate that COSTA is able
              to prove termination and infer bounds on resource
              consumption for programs that could not be handled
              before."
}

@Inproceedings{AlthoffK12,
  Author = "M. Althoff and B. H. Krogh",
  Title = "Avoiding Geometric Intersection Operations
           in Reachability Analysis of Hybrid Systems",
  Booktitle = "Proceedings of the 15th ACM International Conference
               on Hybrid Systems: Computation and Control (HSCC '12)",
  Year = 2012,
  ISBN = "978-1-4503-1220-2",
  Address = "Beijing, China",
  Pages = "45--54",
  Publisher = "ACM Press, New York, USA",
  Abstract = "Although a growing number of dynamical systems studied
              in various fields are hybrid in nature, the verification
              of properties, such as stability, safety, etc., is still
              a challenging problem. Reachability analysis is one of
              the promising methods for hybrid system verification,
              which together with all other verification techniques
              faces the challenge of making the analysis scale with
              respect to the number of continuous state variables. The
              bottleneck of many reachability analysis techniques for
              hybrid systems is the geometrically computed
              intersection with guard sets. In this work, we replace
              the intersection operation by a nonlinear mapping onto
              the guard, which is not only numerically stable, but
              also scalable, making it possible to verify systems
              which were previously out of reach. The approach can be
              applied to the fairly common class of hybrid systems
              with piecewise continuous solutions, guard sets modeled
              as halfspaces, and urgent semantics, i.e. discrete
              transitions are immediately taken when enabled by guard
              sets. We demonstrate the usefulness of the new approach
              by a mechanical system with backlash which has 101
              continuous state variables."
}

@Inproceedings{Alur11,
  Author = "R. Alur",
  Title = "Formal Verification of Hybrid Systems",
  Booktitle = "Proceedings of the 11th International Conference
               on Embedded Software (EMSOFT 2011)",
  Address =  "Taipei, Taiwan",
  Editor = "S. Chakraborty and A. Jerraya and S. K. Baruah
            and S. Fischmeister",
  Publisher = "ACM Press",
  Year = 2011,
  Pages = "273--278",
  ISBN = "978-1-4503-0714-7",
  Abstract = "In formal verification, a designer first constructs a
              model, with mathematically precise semantics, of the
              system under design, and performs extensive analysis
              with respect to correctness requirements. The
              appropriate mathematical model for embedded control
              systems is hybrid systems that combines the traditional
              state-machine based models for discrete control with
              classical differential-equations based models for
              continuously evolving physical activities. In this
              article, we briefly review selected existing approaches
              to formal verification of hybrid systems, along with
              directions for future research."
}

@Inproceedings{AlurKRS08,
  Author = "R. Alur and A. Kanade and S. Ramesh and K. Shashidhar",
  Title = "Symbolic Analysis for Improving Simulation Coverage
           of Simulink/Stateflow Models",
  Booktitle = "Proceedings of the 8th ACM {\&} IEEE International Conference
               on Embedded Software (EMSOFT 2008)",
  Address = "Atlanta, Georgia, USA",
  Editor = "L. {de Alfaro} and J. Palsberg",
  Publisher = "ACM Press",
  Pages = "89--98",
  Year = 2008,
  ISBN = "978-1-60558-468-3",
  Abstract = "Aimed at verifying safety properties and improving
              simulation coverage for hybrid systems models of
              embedded controlsoftware, we propose a technique that
              combines numerical simulation and symbolic methods for
              computing state-sets.  We consider systems with linear
              dynamics described in the commercial modeling tool
              Simulink/Stateflow.  Given an initial state $x$,
              and a discrete-time simulation trajectory, our
              method computes a set of initial states that are
              guaranteed to be equivalent to $x$, where two initial
              states are considered to be equivalent if the resulting
              simulation trajectories contain the same discrete
              components at each step of the simulation.  We illustrate
              the benefits of our method on two case studies.
              One case study is a benchmark proposed in the literature
              for hybrid systems verification and another is a Simulink
              demo model from Mathworks."
}

@Inproceedings{AmatoPS10,
  Author = "G. Amato and M. Parton and F. Scozzari",
  Title = "A Tool Which Mines Partial Execution Traces to Improve
           Static Analysis",
  Booktitle = "Proceedings of the 1st International Conference on
               Runtime Verification (RV 2010)",
  Address = "Balluta Bay, St Julians, Malta",
  Series = "Lecture Notes in Computer Science",
  Editor = "H. Barringer and Y. Falcone and B. Finkbeiner and K. Havelund
            and I. Lee and G. Pace and G. Rosu and O. Sokolsky and
            N. Tillmann",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-16611-2",
  Pages =  "475--479",
  Volume = 6418,
  Year = 2010,
  Abstract = "We present a tool which performs abstract interpretation
              based static analysis of numerical variables. The
              novelty is that the analysis is parametric, and
              parameters are chosen by applying a variant of principal
              component analysis to partial execution traces of
              programs."
}

@Article{AmatoPS12,
  Author = "G. Amato and M. Parton and F. Scozzari",
  Title = "Discovering Invariants via Simple Component Analysis",
  Journal = "Journal of Symbolic Computation",
  Publisher = "Elsevier Science B.V.",
  Volume = 47,
  Number = 12,
  Year = 2012,
  Pages = "1533--1560",
  Abstract = "We propose a new technique combining dynamic and static
              analysis of programs to find linear invariants. We use a
              statistical tool, called simple component analysis, to
              analyze partial execution traces of a given program. We
              get a new coordinate system in the vector space of
              program variables, which is used to specialize numerical
              abstract domains. As an application, we instantiate our
              technique to interval analysis of simple imperative
              programs and show some experimental evaluations."
}

@Inproceedings{AmatoS12,
  Author = "G. Amato and F. Scozzari",
  Title = "Random: R-Based Analyzer for Numerical Domains",
  Booktitle = "Proceedings of the 18th International Conference
               on Logic for Programming, Artificial Intelligence,
               and Reasoning (LPAR 2012)",
  Address = "M\'erida, Venezuela",
  Series = "Lecture Notes in Computer Science",
  Editor = "N. Bj{\o}rner and A. Voronkov",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-28716-9",
  Pages =  "375--382",
  Volume = 7180,
  Year = 2012,
  Abstract = "We present the tool Random (R-based Analyzer for
              Numerical DOMains) for static analysis of imperative
              programs. The tool is based on the theory of abstract
              interpretation and implements several abstract
              domains for detecting numerical properties, in
              particular integer loop invariants.  The tool
              combines a statistical dynamic analysis with a static
              analysis on the new domain of parallelotopes.  The
              tool has a graphical interface for tuning the
              parameters of the analysis and visualizing partial
              traces."
}

@Inproceedings{AmatoS13,
  Author = "G. Amato and F. Scozzari",
  Title = "Localizing Widening and Narrowing",
  Booktitle = "Static Analysis:
               Proceedings of the 20th International Symposium",
  Address = "Seattle, USA",
  Series = "Lecture Notes in Computer Science",
  Editor = "F. Logozzo and M. F{\"a}hndrich",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-38855-2 (Print) 978-3-642-38856-9 (Online)",
  Pages =  "25--42",
  Volume = 7935,
  Year = 2013,
  Abstract = "We show two strategies which may be easily applied to
              standard abstract interpretation-based static
              analyzers. They consist in 1) restricting the scope of
              widening, and 2) intertwining the computation of
              ascending and descending chains. Using these
              optimizations it is possible to improve the precision of
              the analysis, without any change to the abstract
              domains."
}

@Inproceedings{Andre10,
  Author = "{\'E}. Andr{\'e}",
  Title = "{IMITATOR~II}:
           A Tool for Solving the Good Parameters Problem in Timed Automata",
  Booktitle = "Proceedings of the 12th International Workshop
               on Verification of Infinite State Systems (INFINITY'10)",
  Editor = "Y.-F. Chen and A. Rezine",
  Address = "Singapore",
  Pages = "91--99",
  Series = "Electronic Proceedings in Theoretical Computer Science",
  Volume = 39,
  Year = 2010,
  Abstract = "We present here \textsc{Imitator}~II, a new version of
             \textsc{Imitator}, a tool implementing the ``inverse
             method'' for parametric timed automata: given a reference
             valuation of the parameters, it synthesizes a constraint
             such that, for any valuation satisfying this constraint,
             the system behaves the same as under the reference
             valuation in terms of traces, i.e., alternating sequences
             of locations and actions. \textsc{Imitator}~II also
             implements the ``behavioral cartography algorithm'',
             allowing us to solve the following good parameters
             problem: find a set of valuations within a given bounded
             parametric domain for which the system behaves well. We
             present new features and optimizations of the tool, and
             give results of applications to various examples of
             asynchronous circuits and communication protocols."
}

@Techreport{AndreFS11TR,
  Author = "{\'E}. Andr{\'e} and L. Fribourg and R. Soulat",
  Title = "Enhancing the Inverse Method with State Merging",
  Type = "Research report",
  Number = "LSV-11-26",
  Year = 2011,
  Month = dec,
  Institution = "Laboratoire Sp\'ecification \& V\'erification",
  Address = "\'Ecole Normale Sup\'erieure de Cachan, Paris, France",
  Abstract = "Keeping the state space small is essential when
              verifying realtime systems using Timed Automata (TA). In
              the model-checker Uppaal, the merging operation has been
              used extensively in order to reduce the number of
              states. Actually, Uppaal's merging technique applies
              within the more general setting of Parametric Timed
              Automata (PTA). The Inverse Method (IM) for a PTA A is a
              procedure that synthesizes a zone around a given point
              0 (parameter valuation) over which A is guaranteed to
              behave similarly. We show that the integration of
              merging into IM leads to the synthesis of larger zones
              around 0. It also often improves the performance of
              IM, both in terms of computational space and time, as
              shown by our experimental results."
}

@Inproceedings{AndreFS12,
  Author = "{\'E}. Andr{\'e} and L. Fribourg and R. Soulat",
  Title = "Enhancing the Inverse Method with State Merging",
  Booktitle = "NASA Formal Methods:
               Proceedings of the 4th International Symposium (NFM 2012)",
  Editor = "A. E. Goodloe and S. Person",
  Address = "Norfolk, USA",
  Pages = "381--396",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7226,
  Year = 2012,
  Abstract = "Keeping the state space small is essential when
              verifying realtime systems using Timed Automata (TA). In
              the model-checker Uppaal, the merging operation has been
              used extensively in order to reduce the number of
              states. Actually, Uppaal's merging technique applies
              within the more general setting of Parametric Timed
              Automata (PTA). The Inverse Method (IM) for a PTA A is a
              procedure that synthesizes a zone around a given point
              0 (parameter valuation) over which A is guaranteed to
              behave similarly. We show that the integration of
              merging into IM leads to the synthesis of larger zones
              around 0. It also often improves the performance of
              IM, both in terms of computational space and time, as
              shown by our experimental results."
}


@Inproceedings{AndreFS13,
  Author = "{\'E}. Andr{\'e} and L. Fribourg and R. Soulat",
  Title = "Merge and Conquer: State Merging in Parametric Timed Automata",
  Booktitle = "Automated Technology for Verification and Analysis:
               Proceedings of the 11th International Symposium (ATVA 2013)",
  Editor = "D. Van Hung and M. Ogawa",
  Address = "Hanoi, Vietnam",
  Pages = "381--396",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 8172,
  Year = 2013,
  Abstract = "Parameter synthesis for real-time systems aims at
              synthesizing dense sets of valuations for the timing
              requirements, guaranteeing a good behavior. A popular
              formalism for modeling parameterized real-time systems
              is parametric timed automata (PTAs). Compacting the
              state space of PTAs as much as possible is
              fundamental. We present here a state merging reduction
              based on convex union, that reduces the state space, but
              yields an over-approximation of the executable
              paths. However, we show that it preserves the sets of
              reachable locations and executable actions. We also show
              that our merging technique associated with the inverse
              method, an algorithm for parameter synthesis, preserves
              locations as well, and outputs larger sets of parameter
              valuations."
}

@Inproceedings{AndreLSDL13,
  Author    = "E. Andr{\'e} and Y. Liu and J. Sun and J. S. Dong and {S.-W}. Lin",
  Title     = "PSyHCoS: Parameter Synthesis for Hierarchical Concurrent
               Real-Time Systems",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 25th International Conference (CAV 2013)",
  Year      = 2013,
  Pages     = "984--989",
  Editor    = "N. Sharygina and H. Veith",
  Publisher = "Springer-Verlag, Berlin",
  Series    = "Lecture Notes in Computer Science",
  Volume    = 8044,
  ISBN      = "978-3-642-39798-1",
  Abstract = "Real-time systems are often hard to control, due to
              their complicated structures, quantitative time factors
              and even unknown delays.  We present here PSyHCoS, a
              tool for analyzing parametric real-time systems
              specied using the hierarchical modeling language
              PSTCSP.  PSyHCoS supports several algorithms for
              parameter synthesis and model checking, as well as state
              space reduction techniques. Its architecture favors
              reusability in terms of syntax, semantics, and
              algorithms. It comes with a friendly user interface that
              can be used to edit, simulate and verify PSTCSP
              models. Experiments show its eciency and
              applicability."
}

@Book{AndreS13,
  Author = "{\'E}. Andr{\'e} and R. Soulat",
  Title = "The Inverse
           Method: Parametric Verification of Real-time Embedded Systems",
  Publisher = "John Wiley and Sons.",
  Series = "{FOCUS Series}",
  ISBN = "9781118569405",
  Year = 2013,
  Abstract = "This book introduces state-of-the-art verification
              techniques for real-time embedded systems, based on the
              inverse method for parametric timed automata. It reviews
              popular formalisms for the specification and
              verification of timed concurrent systems and, in
              particular, timed automata as well as several extensions
              such as timed automata equipped with stopwatches, linear
              hybrid automata and affine hybrid automata.  The inverse
              method is introduced, and its benefits for guaranteeing
              robustness in real-time systems are shown. Then, it is
              shown how an iteration of the inverse method can solve
              the good parameters problem for parametric timed
              automata by computing a behavioral cartography of the
              system. Different extensions are proposed particularly
              for hybrid systems and applications to scheduling
              problems using timed automata with stopwatches. Various
              examples, both from the literature and industry,
              illustrate the techniques throughout the book.  Various
              parametric verifications are performed, in particular of
              abstractions of a memory circuit sold by the chipset
              manufacturer ST-Microelectronics, as well as of the
              prospective flight control system of the next generation
              of spacecraft designed by ASTRIUM Space Transportation."
}

@Inproceedings{ArmandoBM07,
  Author = "A. Armando and M. Benerecetti and J. Mantovani",
  Title = "Abstraction Refinement of Linear Programs with Arrays",
  Booktitle = "Proceedings of the 13th International Conference on
               Tools and Algorithms for the Construction and Analysis
               of Systems (TACAS 2007)",
  Address = "Braga, Portugal",
  Editor = "O. Grumberg and M. Huth",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4424,
  Pages = "373--388",
  Year = 2007,
  ISBN = "3-540-71208-4",
  Abstract = "In previous work we presented a model checking procedure
              for linear programs, i.e. programs in which variables
              range over a numeric domain and expressions involve
              linear combinations of the variables. In this paper we
              lift our model checking procedure for linear programs to
              deal with arrays via iterative abstraction
              refinement. While most approaches are based on predicate
              abstraction and therefore the abstraction is relative to
              sets of predicates, in our approach the abstraction is
              relative to sets of variables and array indexes, and the
              abstract program can express complex correlations
              between program variables and array elements. Thus,
              while arrays are problematic for most of the approaches
              based on predicate abstraction, our approach treats them
              in a precise way. This is an important feature as arrays
              are ubiquitous in programming.  We provide a detailed
              account of both the abstraction and the refinement
              processes, discuss their implementation in the eureka
              tool, and present experimental results that confirm the
              effectiveness of our approach on a number of programs of
              interest."
}

@Inproceedings{AsarinDFGLGM06,
  Author = "E. Asarin and T. Dang and G. Frehse and A. Girard
            and C. {Le Guernic} and O. Maler",
  Title = "Recent Progress in Continuous and Hybrid Reachability Analysis",
  Booktitle = "Proceedings of the IEEE International Symposium
               on Computer-Aided Control Systems Design",
  Address = "Technische Universit{\"a}t M{\"u}nchen, Munich, Germany",
  Year = 2006,
  Abstract = "Set-based reachability analysis computes all possible
              states a system may attain, and in this sense provides
              knowledge about the system with a completeness, or
              coverage, that a finite number of simulation runs can
              not deliver. Due to its inherent complexity, the
              application of reachability analysis has been limited so
              far to simple systems, both in the continuous and the
              hybrid domain. In this paper we present recent advances
              that, in combination, significantly improve this
              applicability, and allow us to find better balance
              between computational cost and accuracy. The
              presentation covers, in a unified manner, a variety of
              methods handling increasingly complex types of
              continuous dynamics (constant derivative, linear,
              nonlinear). The improvements include new geometrical
              objects for representing sets, new approximation
              schemes, and more flexible combinations of graph-search
              algorithm and partition refinement. We report briefly
              some preliminary experiments that have enabled the
              analysis of systems previously beyond reach."
}

@Inproceedings{Avery06,
  Author = "J. Avery",
  Title = "Size-Change Termination and Bound Analysis",
  Booktitle = "Proceedings of the 8th International Symposium
               on Functional and Logic Programming (FLOPS 2006)",
  Address = "Fuji-Susono, Japan",
  Editor = "M. Hagiya and P. Wadler",
  Pages = "192--207",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3945,
  Year = 2006,
  ISBN = "3-540-33438-6",
  Abstract = "Despite its simplicity, the size-change termination
              principle, presented by Lee, Jones and Ben-Amram in
              [LJB01], is surprisingly strong and is able to show
              termination for a large class of programs. A significant
              limitation for its use, however, is the fact that the
              SCT requires data types to be well-founded, and that all
              mechanisms used to determine termination must involve
              decreases in these global, well-founded partial orders.
              Following is an extension of the size-change principle
              that allows for non-well founded data types, and a
              realization of this principle for integer data
              types. The extended size-change principle is realized
              through combining abstract interpretation over the
              domain of convex polyhedra with the use of size-change
              graphs. In the cases when data types \emph{are} well
              founded, the method handles every case that is handled
              by LJB size-change termination.  The method has been
              implemented in a subject language independent shared
              library, \texttt{libesct} (available at [Ave05a]), as
              well as for the ANSI C specializer
              $\texttt{C-Mix}_\texttt{II}$, handling a
              subset of its internal language \texttt{Core-C}."
}

@Inproceedings{BagnaraR-CZ05,
  Author = "R. Bagnara and E. Rodr{\'\i}guez-Carbonell and E. Zaffanella",
  Title = "Generation of Basic Semi-algebraic Invariants
           Using Convex Polyhedra",
  Booktitle = "Static Analysis:
               Proceedings of the 12th International Symposium",
  Address = "London, UK",
  Editor = "C. Hankin and I. Siveroni",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3672,
  ISBN = "3-540-28584-9",
  Year = 2005,
  Pages = "19--34",
  Abstract = "A technique for generating invariant polynomial
              \emph{inequalities} of bounded degree is presented using
              the abstract interpretation framework.  It is based on
              overapproximating basic semi-algebraic sets, i.e., sets
              defined by conjunctions of polynomial inequalities, by
              means of convex polyhedra.  While improving on the
              existing methods for generating invariant polynomial
              \emph{equalities}, since polynomial inequalities are
              allowed in the guards of the transition system, the
              approach does not suffer from the prohibitive complexity
              of the methods based on quantifier-elimination.  The
              application of our implementation to benchmark programs
              shows that the method produces non-trivial invariants in
              reasonable time.  In some cases the generated invariants
              are essential to verify safety properties that cannot be
              proved with classical linear invariants."
}

@Techreport{BagnaraR-CZ05TR,
  Author = "R. Bagnara and E. Rodr{\'\i}guez-Carbonell and E. Zaffanella",
  Title = "Generation of Basic Semi-algebraic Invariants
           Using Convex Polyhedra",
  Number = "LSI-05-14-R",
  Type = "Report de recerca",
  Institution = "Departament de Llenguatges i Sistemes Inform{\`a}tics,
                 Universitat Polit{\`e}cnica de Catalunya, Barcelona, Spain",
  Year = 2005,
  Note = "Available at \url{http://www.lsi.upc.edu/dept/techreps/techreps.html}"
}

@Incollection{BandaG09,
  Author = "G. Banda and J. P. Gallagher",
  Title = "Analysis of Linear Hybrid Systems in {CLP}",
  Booktitle = "Logic-Based Program Synthesis and Transformation",
  Editor = "M. Hanus",
  Pages = "55--70",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5438,
  Year = 2009,
  ISBN = "978-3-642-00514-5",
  Note = "Revised selected papers presented at the 18th International
          Symposium on Logic-Based Program Synthesis and Transformation
          (LOPSTR 2008), Valencia, Spain, July 17--18, 2008",
  Abstract = "In this paper we present a procedure for representing
              the semantics of linear hybrid automata (LHAs) as
              constraint logic programs (CLP); flexible and accurate
              analysis and verification of LHAs can then be performed
              using generic CLP analysis and transformation
              tools. LHAs provide an expressive notation for
              specifying real-time systems. The main contributions are
              (i) a technique for capturing the reachable states of
              the continuously changing state variables of the LHA as
              CLP constraints; (ii) a way of representing events in
              the LHA as constraints in CLP, along with a product
              construction on the CLP representation including
              synchronisation on shared events; (iii) a framework in
              which various kinds of reasoning about an LHA can be
              flexibly performed by combining standard CLP
              transformation and analysis techniques.  We give
              experimental results to support the usefulness of the
              approach and argue that we contribute to the general
              field of using static analysis tools for verification."
}

@Inproceedings{Ben-AmramG13,
 Author = "A. M. Ben-Amram and S. Genaim",
 Title = "On the Linear Ranking Problem for Integer Linear-Constraint Loops",
 Booktitle = "Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on
              Principles of Programming Languages (POPL 2013)",
 Year = 2013,
 ISBN = "978-1-4503-1832-7",
 Address = "Rome, Italy",
 Pages = "51--62",
 Publisher = "ACM Press",
 Note = "Also published in ACM SIGPLAN Notices, POPL '13, Volume 48, Issue 1",
 Abstract = "In this paper we study the complexity of the Linear
             Ranking problem: given a loop, described by linear
             constraints over a finite set of integer variables, is
             there a linear ranking function for this loop? While
             existence of such a function implies termination, this
             problem is not equivalent to termination. When the
             variables range over the rationals or reals, the Linear
             Ranking problem is known to be PTIME decidable. However,
             when they range over the integers, whether for
             single-path or multipath loops, the complexity of the
             Linear Ranking problem has not yet been determined. We
             show that it is coNP-complete. However, we point out some
             special cases of importance of PTIME complexity. We also
             present complete algorithms for synthesizing linear
             ranking functions, both for the general case and the
             special PTIME cases."
}

@Inproceedings{BerendsenJV10,
  Author = "J. Berendsen and D. N. Jansen and F. W. Vaandrager",
  Title = "Fortuna: Model Checking Priced Probabilistic Timed Automata",
  Booktitle = "Proceedings of the 7th International Conference on the
               Quantitative Evaluation of Systems (QEST 2010)",
  Address = "Williamsburg, Virginia, USA",
  Publisher = "IEEE Computer Society",
  Year = 2010,
  Pages = "273--281",
  ISBN = "978-0-7695-4188-4",
  Abstract = "Fortuna is the first tool for model checking priced
              probabilistic timed automata (PPTAs). PPTAs are an
              important model that can handle the combination of
              real-time, probabilistic and cost features. Only model
              checkers that incorporate all these features can
              address the key design trade-offs that arise in many
              practical applications such as: the Zeroconf,
              Bluetooth, IEEE802.11 and Firewire protocols, protocols
              for sensor networks, and scheduling problems with
              failures. PPTAs are an extension of probabilistic timed
              automata (PTAs), by having cost-rates and discrete cost
              increments on states. Fortuna is able to compute the
              maximal probability by which a class of states can be
              reached under a certain cost-bound (and time bound.)
              Although the problem is undecidable in general, there
              exists a semi-algorithm that produces a non-decreasing
              sequence of maximal probabilities. This paper enhances
              that algorithm. We compared the performance of Fortuna
              with existing approaches for PTAs. Surprisingly,
              although PPTAs are more general, our techniques exhibit
              superior performance.",
}

@TechReport{BeyL11TR,
  Author = "A. Bey S. Leue",
  Title = "Modeling and Analyzing Spike Timing Dependent Plasticity
           with Linear Hybrid Automata",
  Number = "soft-11-03",
  Institution = "University of Konstanz, Germany",
  Year = 2011,
  Month = may,
  Abstract = "We propose a model for synaptic plasticity according to
              the Spike Timing Dependent Plasticity (STDP) theory
              using Linear Hybrid Au- tomata (LHA). We first present a
              compositional LHA model in which each component
              corresponds to some process in STDP. We then ab- stract
              this model into a monolithic LHA model in order to
              enable formal analysis using hybrid model checking. We
              discuss how the avail- ability of an LHA model as well
              as its formal analysis using the tool PHAVer can support
              a better understanding of the dynamics of STDP."
}

@Inproceedings{BeyerG11,
  Author = "M. Beyer and S. Glesner",
  Title = "Static Run-Time Mode Extraction by State Partitioning
           in Synchronous Process Networks",
  Booktitle = "Proceedings of the 14th International Workshop on
               Software and Compilers for Embedded Systems (SCOPES 2011)",
  Year = 2011,
  ISBN = "978-1-4503-0763-5",
  Pages = "28--37",
  URL = "http://doi.acm.org/10.1145/1988932.1988938",
  Publisher = "ACM Press",
  Address = "New York, NY, USA",
  Abstract = "Process Networks (PNs) are used for modeling
              streaming-oriented applications with changing behavior,
              which must be mapped on a concurrent architecture to
              meet the performance and energy constraints of embedded
              devices. Finding an optimal mapping of Process Networks
              to the constrained architecture presumes that the
              behavior of the PN is statically known. In this paper we
              present a static analysis for synchronous PNs that
              partitions the state space according to extract run-time
              modes based on a Data Augmented Control Flow Automaton
              (DACFA). The result is a mode automaton whose nodes
              describe identified program modes and whose edges
              represent transitions among them. Optimizing back-ends
              mapping from PNs to concurrent architectures can be
              guided by these analysis results."
}

@Inproceedings{BeyerG12,
  Author = "M. Beyer and S. Glesner",
  Title = "Static Analysis of Run-Time Modes in Synchronous Process Network",
  Booktitle = "Perspectives of Systems Informatics: Proceedings of the
               8th International Andrei Ershov Memorial Conference",
  Series = "Lecture Notes in Computer Science",
  Editor = "E. Clarke and I. Virbitskaite and A. Voronkov",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-29708-3",
  Pages =  "55--67",
  Volume = 7162,
  Year = 2012,
  Abstract = "For modeling modern streaming-oriented applications,
              Process Networks (PNs) are used to describe systems with
              changing behavior, which must be mapped on a concurrent
              architecture to meet the performance and energy
              constraints of embedded devices. Finding an optimal
              mapping of Process Networks to the constrained
              architecture presumes that the behavior of the Process
              Network is statically known. In this paper we present a
              static analysis for synchronous PNs that extracts
              different run-time modes by using polyhedral
              abstraction. The result is a Mealy machine whose states
              describe different run-time modes and the edges among
              them represent transitions. This machine can be used to
              guide optimizing backend mappings from PNs to concurrent
              architectures."
}

@Inproceedings{BouchyFL08,
  Author = "F. Bouchy and A. Finkel and J. Leroux",
  Title = "Decomposition of Decidable First-Order Logics
           over Integers and Reals",
  Booktitle = "Proceedings of the 15th International Symposium on
               Temporal Representation and Reasoning (TIME '08)",
  Address = "Montreal, Canada",
  Publisher = "IEEE Computer Society Press",
  Pages = "147--155",
  Year = 2008,
  Abstract = "We tackle the issue of representing infinite sets of
              real-valued vectors. This paper introduces an
              operator for combining integer and real sets. Using
              this operator, we decompose three well-known logics
              extending Presburger with reals. Our decomposition
              splits a logic into two parts : one integer, and one
              decimal (i.e. on the interval $[0, 1[$). We also give
              a basis for an implementation of our representation."
}

@Inproceedings{BozgaGI09,
  Author = "M. Bozga and C. G\^{\i}rlea and R. Iosif",
  Title = "Iterating Octagons",
  Booktitle = "Proceedings of the 15th International Conference on
               Tools and Algorithms for the Construction and Analysis
               of Systems (TACAS 2009)",
  Address = "York, UK",
  Editor = "S. Kowalewski and A. Philippou",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5505,
  Pages = "337-351",
  Year = 2009,
  ISBN = "978-3-642-00767-5",
  Abstract = "In this paper we prove that the transitive closure of a
              nondeterministic octagonal relation using integer
              counters can be expressed in Presburger arithmetic. The
              direct consequence of this fact is that the reachability
              problem is decidable for flat counter automata with
              octagonal transition relations. This result improves the
              previous results of Comon and Jurski [Hubert Comon and
              Yan Jurski. Multiple counters automata, safety analysis
              and presburger arithmetic. In \emph{CAV}, LNCS 1427, pages
              268-279, 1998] and Bozga, Iosif and Lakhnech [Marius Bozga,
              Radu Iosif, and Yassine Lakhnech. Flat parametric counter
              automata. In \emph{ICALP}, LNCS 4052, pages 577-588.
              Springer-Verlag, 2006] concerning the computation of
              transitive closures for difference bound relations.
              The importance of this result is justified by the wide
              use of octagons to computing sound abstractions of
              real-life systems [A. Min\'e. The octagon abstract domain.
              \emph{Higher-Order and Symbolic Computation}, 19(1):31-100,
              2006]. We have implemented the octagonal transitive closure
              algorithm in a prototype system for the analysis of counter
              automata, called FLATA, and we have experimented with a
              number of test cases."
}

@Inproceedings{BramanM08,
  Title = "Safety Verification of Fault Tolerant Goal-based Control Programs
           with Estimation Uncertainty",
  Author = "J. M. B. Braman and R. M. Murray",
  Booktitle = "Proceedings of the 2008 American Control Conference",
  Address = "Seattle, Washington, USA",
  Publisher = "IEEE Press",
  Year = 2008,
  Pages = "27--32",
  ISSN = "0743-1619",
  ISBN = "978-1-4244-2078-0",
  Abstract = "Fault tolerance and safety verification of control
              systems that have state variable estimation uncertainty
              are essential for the success of autonomous robotic
              systems. A software control architecture called mission
              data system, developed at the Jet Propulsion Laboratory,
              uses goal networks as the control program for autonomous
              systems. Certain types of goal networks can be converted
              into linear hybrid systems and verified for safety using
              existing symbolic model checking software. A process for
              calculating the probability of failure of certain
              classes of verifiable goal networks due to state
              estimation uncertainty is presented. A verifiable
              example task is presented and the failure probability of
              the control program based on estimation uncertainty is
              found."
}

@Techreport{Braun12TR,
  Author = "V. Braun",
  Title = "Counting Points and {Hilbert} Series in String Theory",
  Institution = "University of Pennsylvania in Philadelphia, USA",
  Number = "arXiv:1206.2236v1 [hep-th]",
  Note = "Available from \url{http://arxiv.org/}",
  Year = 2012,
  Month = jun,
  URL = "http://arxiv.org/abs/1206.2236v1",
  Abstract = "The problem of counting points is revisited from the
              perspective of reflexive 4-dimensional polytopes. As an
              application, the Hilbert series of the 473,800,776
              reflexive polytopes (equivalently, their Calabi-Yau
              hypersurfaces) are computed."
}

@Inproceedings{BrihayeDGQRW13,
  Author = "T. Brihaye and L. Doyen and G. Geeraerts and J. Ouaknine and J.-F. Raskin and J. Worrell",
  Title = "Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points",
  Booktitle = "Automated Technology for Verification and Analysis:
               Proceedings of the 11th International Symposium (ATVA 2013)",
  Address = "Hanoi, Vietnam",
  Editor = "Dang Van Hung",
  Year = 2013,
  Pages = "55--70",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 8172,
  ISBN = "978-3-319-02443-1",
  Abstract = "We study the time-bounded reachability problem for
              monotonic hybrid automata (MHA), i.e., rectangular
              hybrid automata for which the rate of each variable is
              either always non-negative or always non-positive. In
              this paper, we revisit the decidability results
              presented in [T.~Brihaye and L.~Doyen and G.~Geeraerts
              and J.~Ouaknine. and J.-F.~Raskin and J.~Worrell: On
              reachability for hybrid automata over bounded time. In:
              ICALP 2011, Part II. LNCS, vol. 6756,
              pp. 416–427. Springer, Heidelberg (2011)] and show that
              the problem is NExpTime-complete. We also show that we
              can effectively compute fixed points that characterise
              the sets of states that are reachable
              (resp. co-reachable) within T time units from a given
              state."
}

@Techreport{CacheraM-A05,
  Author = "D. Cachera and K. Morin-Allory",
  Title = "Proving Parameterized Systems: The Use of a Widening Operator
          and Pseudo-Pipelines in Polyhedral Logic",
  Type = "Research Report",
  Number = "ISRN TIMA--RR-05/04-01--FR",
  Institution = "TIMA Laboratory",
  Address = "Grenoble, France",
  Year = 2005,
  Abstract = "We propose proof techniques and tools for the formal
              verification of regular parameterized systems. These
              systems are expressed in the polyhedral model, which
              combines affine recurrence equations with index sets of
              polyhedral shape. We extend a previously defined proof
              system based on a polyhedral logic with the detection of
              pseudo-pipelines, that are particular patterns in the
              variable definitions generalizing the notion of
              pipeline. The combination of pseudo-pipeline detection
              with the use of a simple widening operator greatly
              improves the effectiveness of our proof techniques."
}

@Article{CarloniPPS-V06,
  Author = "L. P. Carloni and R. Passerone and A. Pinto
            and A. L. Sangiovanni-Vincentelli",
  Title = "Languages and Tools for Hybrid Systems Design",
  Journal = "Foundations and Trends. in Electronic Design Automation",
  Volume = 1,
  Number = "1/2",
  Pages = "1--193",
  Year = 2006,
  Abstract = "The explosive growth of embedded electronics is bringing
              information and control systems of increasing complexity
              to every aspects of our lives. The most challenging
              designs are safety-critical systems, such as
              transportation systems (e.g., airplanes, cars, and
              trains), industrial plants and health care
              monitoring. The difficulties reside in accommodating
              constraints both on functionality and
              implementation. The correct behavior must be guaranteed
              under diverse states of the environment and potential
              failures; implementation has to meet cost, size, and
              power consumption requirements. The design is therefore
              subject to extensive mathematical analysis and
              simulation. However, traditional models of information
              systems do not interface well to the continuous evolving
              nature of the environment in which these devices
              operate.  Thus, in practice, different mathematical
              representations have to be mixed to analyze the overall
              behavior of the system. \emph{Hybrid systems} are a
              particular class of mixed models that focus on the
              combination of discrete and continuous subsystems. There
              is a wealth of tools and languages that have been
              proposed over the years to handle hybrid
              systems. However, each tool makes different assumptions
              on the environment, resulting in somewhat different
              notions of hybrid system. This makes it difficult to
              share information among tools. Thus, the community
              cannot maximally leverage the substantial amount of work
              that has been directed to this important topic. In this
              paper, we review and compare hybrid system tools by
              highlighting their differences in terms of their
              underlying semantics, expressive power and mathematical
              mechanisms.  We conclude our review with a comparative
              summary, which suggests the need for a unifying approach
              to hybrid systems design. As a step in this direction,
              we make the case for a \emph{semantic-aware interchange
              format}, which would enable the use of joint techniques,
              make a formal comparison between different approaches
              possible, and facilitate exporting and importing design
              representations."
}

@Inproceedings{CarnevaliPSV13,
 Author = "L. Carnevali and M. Paolieri and A. Santoni and E. Vicario",
 Title = "Non-Markovian Analysis for Model Driven Engineering of Real-time Software",
 Booktitle = "Proceedings of the 4th ACM/SPEC International Conference
              on Performance Engineering (ICPE '13)",
 Year = 2013,
 ISBN = "978-1-4503-1636-1",
 Address = "Prague, Czech Republic",
 Pages = "113--124",
 Publisher = "ACM, New York, USA",
 Abstract = "Quantitative evaluation of models with stochastic timings
             can decisively support schedulability analysis and
             performance engineering of real-time concurrent
             systems. These tasks require modeling formalisms and
             solution techniques that can encompass stochastic
             temporal parameters firmly constrained within a bounded
             support, thus breaking the limits of Markovian
             approaches. The problem is further exacerbated by the
             need to represent suspension of timers, which results
             from common patterns of real-time programming. This poses
             relevant challenges both in the theoretical development
             of non-Markovian solution techniques and in their
             practical integration within a viable tailoring of
             industrial processes.

             We address both issues by extending a method for
             transient analysis of non-Markovian models to encompass
             suspension of timers. The solution technique addresses
             models that include timers with bounded and deterministic
             support, which are essential to represent synchronous
             task releases, timeouts, offsets, jitters, and
             computations constrained by a Best Case Execution Time
             (BCET) and a Worst Case Execution Time (WCET). As a
             notable trait, the theory of analysis is amenable to the
             integration within a Model Driven Development (MDD)
             approach, providing specific evaluation capabilities in
             support of performance engineering without disrupting the
             flow of design and documentation of the consolidated
             practice.",
}


@Inproceedings{ChakarovS13,
  Author    = "A. Chakarov and S. Sankaranarayanan",
  Title     = "Probabilistic Program Analysis with Martingales",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 25th International Conference (CAV 2013)",
  Year      = 2013,
  Pages     = "511-526",
  Editor    = "N. Sharygina and H. Veith",
  Publisher = "Springer-Verlag, Berlin",
  Series    = "Lecture Notes in Computer Science",
  Volume    = 8044,
  ISBN      = "978-3-642-39798-1",
  Abstract = "We present techniques for the analysis of infinite state
              probabilistic programs to synthesize probabilistic
              invariants and prove almost-sure termination.  Our
              analysis is based on the notion of (super) martingales
              from probability theory. First, we define the concept of
              (super) martingales for loops in probabilistic
              programs. Next, we present the use of concentration of
              measure inequalities to bound the values of martingales
              with high probability. This directly allows us to infer
              probabilistic bounds on assertions involving the program
              variables. Next, we present the notion of a super
              martingale ranking function (SMRF) to prove almost sure
              termination of probabilistic programs. Finally, we
              extend constraint-based techniques to synthesize
              martingales and super-martingale ranking functions for
              probabilistic programs. We present some applications of
              our approach to reason about invariance and termination
              of small but complex probabilistic programs."
}

@Article{ChakrabortyMS06,
  Title = "Reasoning about Synchronization in {GALS} Systems",
  Author = "S. Chakraborty and J. Mekie and D. K. Sharma",
  Journal = "Formal Methods in System Design",
  Publisher = "Springer Netherlands",
  Volume = 28,
  Number = 2,
  Pages = "153--169",
  Year = 2006,
  Abstract = "Correct design of interface circuits is crucial for the
              development of System-on-Chips (SoC) using off-the-shelf
              IP cores. For correct operation, an interface circuit
              must meet strict synchronization timing constraints, and
              also respect sequencing constraints between events
              dictated by interfacing protocols and rational clock
              relations. In this paper, we propose a technique for
              automatically analyzing the interaction between
              independently specified synchronization constraints and
              sequencing constraints between events. We show how this
              analysis can be used to derive delay constraints for
              correct operation of interface circuits in a GALS
              system. Our methodology allows an SoC designer to mix
              and match different interfacing protocols, rational
              clock relations and synchronization constraints for
              communication between a pair of modules, and
              automatically explore their implications on correct
              interface circuit design."
}

@Inproceedings{ChenMC08,
  Author = "L. Chen and A. Min{\'e} and P. Cousot",
  Title = "A Sound Floating-Point Polyhedra Abstract Domain",
  Booktitle = "Proceedings of the 6th Asian Symposium on
               Programming Languages and Systems (APLAS 2008)",
  Address = "Bangalore, India",
  Editor = "G. Ramalingam",
  Year = 2008,
  Pages = "3--18",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5356,
  ISBN = "978-3-540-89329-5",
  Abstract = "The polyhedra abstract domain is one of the most
              powerful and commonly used numerical abstract domains in
              the field of static program analysis based on abstract
              interpretation. In this paper, we present an
              implementation of the polyhedra domain using
              floating-point arithmetic without sacrificing soundness.
              Floating-point arithmetic allows a compact memory
              representation and an efficient implementation on
              current hardware, at the cost of some loss of precision
              due to rounding. Our domain is based on a
              constraint-only representation and employs sound
              floating-point variants of Fourier-Motzkin elimination
              and linear programming. The preliminary experimental
              results of our prototype are encouraging. To our
              knowledge, this is the first time that the polyhedra
              domain is adapted to floating-point arithmetic in a
              sound way."
}

@Inproceedings{ChenKSW13,
  Author = "T. Chen and M. Kwiatkowska and A. Simaitis and C. Wiltsche",
  Title = "Synthesis for Multi-Objective Stochastic Games:
           An Application to Autonomous Urban Driving",
  Booktitle = "Quantitative Evaluation of Systems:
               Proceedings of the 10th International Conference (QEST 2013)",
  Address = "Buenos Aires, Argentina",
  Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D’Argenio",
  Year = 2013,
  Pages = "322--337",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 8054,
  ISBN = "978-3-642-40195-4 (Print) 978-3-642-40196-1 (Online)",
  Abstract = "We study strategy synthesis for stochastic two-player
              games with multiple objectives expressed as a
              conjunction of LTL and expected total reward goals. For
              stopping games, the strategies are constructed from the
              Pareto frontiers that we compute via value
              iteration. Since, in general, infinite memory is
              required for deterministic winning strategies in such
              games, our construction takes advantage of randomised
              memory updates in order to provide compact
              strategies. We implement our methods in PRISM-games, a
              model checker for stochastic multi-player games, and
              present a case study motivated by the DARPA Urban
              Challenge, illustrating how our methods can be used to
              synthesise strategies for high-level control of
              autonomous vehicles."
}

@Inproceedings{ColonS11,
  Author = "M. Col{\'o}n and S. Sankaranarayanan",
  Title = "Generalizing the Template Polyhedral Domain",
  Booktitle = "Proceedings of the 20th European Symposium on Programming
              (ESOP 2011)",
  Address = "Saarbr{\"u}cken, Germany",
  Series = "Lecture Notes in Computer Science",
  Editor = "G. Barthe",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-19717-8",
  Pages =  "176--195",
  Volume = 6602,
  Year = 2011,
  Abstract = "Template polyhedra generalize weakly relational domains
              by specifying arbitrary fixed linear expressions on the
              left-hand sides of inequalities and undetermined
              constants on the right. The domain operations required
              for analysis over template polyhedra can be computed in
              polynomial time using linear programming. In this paper,
              we introduce the generalized template polyhedral domain
              that extends template polyhedra using fixed left-hand
              side expressions with bilinear forms involving program
              variables and unknown parameters to the right. We prove
              that the domain operations over generalized templates
              can be defined as the ``best possible abstractions'' of
              the corresponding polyhedral domain operations. The
              resulting analysis can straddle the entire space of
              linear relation analysis starting from the template
              domain to the full polyhedral domain. We show that
              analysis in the generalized template domain can be
              performed by dualizing the join, post-condition and
              widening operations. We also investigate the special
              case of template polyhedra wherein each bilinear form
              has at most two parameters. For this domain, we use the
              special properties of two dimensional polyhedra and
              techniques from fractional linear programming to derive
              domain operations that can be implemented in polynomial
              time over the number of variables in the program and the
              size of the polyhedra. We present applications of
              generalized template polyhedra to strengthen previously
              obtained invariants by converting them into
              templates. We describe an experimental evaluation of an
              implementation over several benchmark systems."
}

@Inproceedings{CovaFBV06,
  Author = "M. Cova and V. Felmetsger and G. Banks and G. Vigna",
  Title = "Static Detection of Vulnerabilities in x86 Executables",
  Booktitle = "Proceedings of the 22nd Annual Computer Security Applications
               Conference (ACSAC 22)",
  Address = "Miami, Florida, USA",
  Publisher = "IEEE Computer Society Press",
  Pages = "269--278",
  Year = 2006,
  Abstract = "In the last few years, several approaches have been
              proposed to perform vulnerability analysis of
              applications written in high-level languages. However,
              little has been done to automatically identify
              security-relevant flaws in binary code.

              In this paper, we present a novel approach to the
              identification of vulnerabilities in x86 executables in
              ELF binary format. Our approach is based on static
              analysis and symbolic execution techniques. We
              implemented our approach in a proof-of-concept tool and
              used it to detect taint-style vulnerabilities in binary
              code.  The results of our evaluation show that our
              approach is both practical and effective."
}

@Article{DangT12,
  Author = "T. Dang and R. Testylier",
  Title = "Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion",
  Journal = "Reliable Computing",
  Publisher = "Kluwer Academic Publishers",
  Volume = 17,
  Number = 2,
  Year = 2012,
  ISSN = "1573-1340",
  Pages = "128--152",
  Abstract = "This paper is concerned with the reachability
              computation problem for polynomial discrete-time
              dynamical systems. Such computations con- stitute a
              crucial component in algorithmic verication tools for
              hybrid systems and embedded software with polynomial
              dynamics, which have found applications in many
              engineering domains. We describe two meth- ods for
              over-approximating the reachable sets of such systems;
              these meth- ods are based on a combination of the
              Bernstein expansion of polynomial functions and a
              representation of reachable sets by template polyhedra.
              Using a prototype implementation, the performance of the
              methods was demonstrated on a number of examples of
              control systems and biological systems."
}

@Inproceedings{DenmatGD07,
  Author = "T. Denmat and A. Gotlieb and M. Ducass{\'e}",
  Title = "An Abstract Interpretation Based Combinator for Modelling
           While Loops in Constraint Programming",
  Booktitle = "Proceedings of the 13th International Conference on
               Principles and Practice of Constraint Programming (CP 2007)",
  Address = "Providence, Rhode Island, USA",
  Editor = "C. Bessiere",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4741,
  Year = 2007,
  Pages = "241--255",
  ISBN = "978-3-540-74969-1",
  Abstract = "We present the $w$ constraint combinator that models
              while loops in Constraint Programming. Embedded in a
              finite domain constraint solver, it allows programmers
              to develop non-trivial arithmetical relations using
              loops, exactly as in an imperative language style. The
              deduction capabilities of this combinator come from
              abstract interpretation over the polyhedra abstract
              domain. This combinator has already demonstrated its
              utility in constraint-based verification and we argue
              that it also facilitates the rapid prototyping of
              arithmetic constraints (e.g. power, gcd or sum)."
}

@Inproceedings{DooseM05,
  Author = "D. Doose and Z. Mammeri",
  Title = "Polyhedra-Based Approach for Incremental Validation
           of Real-Time Systems",
  Booktitle = "Proceedings of the International Conference on
               Embedded and Ubiquitous Computing (EUC 2005)",
  Address = "Nagasaki, Japan",
  Editor = "L. T. Yang and M. Amamiya and Z. Liu and M. Guo and F. J. Rammig",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3824,
  Year = 2005,
  Pages = "184--193",
  ISBN = "3-540-30807-5",
  Abstract = "Real-time embedded systems can be used in hightly
              important or even vital tasks (avionic and medical
              systems, etc.), thus having strict temporal constraints
              that need to be validated. Existing solutions use
              temporal logic, automata or scheduling
              techniques. However, scheduling techniques are often
              pessimistic and require an almost complete knowledge of
              the system, and formal methods can be ill-fitted to
              manipulate some of the concepts involved in real-time
              systems.  In this article, we propose a method that
              gives to the designer the advantages of formal methods
              and some simplicity in manipulating real-time systems
              notions. This method is able to model and validate all
              the classical features of real-time systems, without any
              pessimism, while guaranteeing the terminaison of the
              validation process. Moreover, its formalism enables to
              study systems of which we have only a partial knowledge,
              and thus to validate or invalidate a system still under
              design. This latest point is very important, since it
              greatly decreases the cost of design backtracks."
}

@Inproceedings{DoyenHR05,
  Author = "L. Doyen and T. A. Henzinger and J.-F. Raskin",
  Title = "Automatic Rectangular Refinement of Affine Hybrid Systems",
  Booktitle = "Proceedings of the 3rd International Conference
              on Formal Modeling and Analysis of Timed Systems (FORMATS 2005)",
  Address = "Uppsala, Sweden",
  Editor = "P. Pettersson and W. Yi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3829,
  Pages = "144--161",
  Year = 2005,
  ISBN = "3-540-30946-2",
  Abstract = "We show how to automatically construct and refine
              rectangular abstractions of systems of linear
              differential equations. From a hybrid automaton whose
              dynamics are given by a system of linear differential
              equations, our method computes automatically a sequence
              of rectangular hybrid automata that are increasingly
              precise overapproximations of the original hybrid
              automaton. We prove an optimality criterion for
              successive refinements. We also show that this method
              can take into account a safety property to be verified,
              refining only relevant parts of the state space. The
              practicability of the method is illustrated on a
              benchmark case study."
}

@Techreport{DoyenHR05TR,
  Author = "L. Doyen and T. A. Henzinger and J.-F. Raskin",
  Title = "Automatic Rectangular Refinement of Affine Hybrid Systems",
  Number = "2005.47",
  Institution = "Centre F\'ed\'er\'e en V\'erification,
                 Universit\'e Libre de Bruxelles, Belgium",
  Year = 2005,
  Abstract = "We show how to automatically construct and refine
              rectangular abstractions of systems of linear
              differential equations. From a hybrid automaton whose
              dynamics are given by a system of linear differential
              equations, our method computes automatically a sequence
              of rectangular hybrid automata that are increasingly
              precise overapproximations of the original hybrid
              automaton. We prove an optimality criterion for
              successive refinements. We also show that this method
              can take into account a safety property to be verified,
              refining only relevant parts of the state space. The
              practicability of the method is illustrated on a
              benchmark case study."
}

@PhdThesis{Doyen06th,
  Author = "L. Doyen",
  Title = "Algorithmic Analysis of Complex Semantics
           for Timed and Hybrid Automata",
  School = "Universit\'e Libre de Bruxelles",
  Address = "Bruxelles, Belgium",
  Month = jun,
  Year = 2006,
  Abstract = "In the field of formal verification of real-time
              systems, major developments have been recorded in the
              last fifteen years. It is about logics, automata,
              process algebra, programming languages, etc. From the
              beginning, a formalism has played an important role:
              \emph{timed automata} and their natural extension,
              \emph{hybrid automata}. Those models allow the
              definition of real-time constraints using real-valued
              \emph{clocks}, or more generally \emph{analog variables}
              whose evolution is governed by differential
              equations. They generalize finite automata in that their
              semantics defines \emph{timed words} where each symbol
              is associated with an occurrence timestamp.

              The \emph{decidability} and \emph{algorithmic analysis}
              of timed and hybrid automata have been intensively
              studied in the literature. The central result for timed
              automata is that they are positively decidable. This is
              not the case for hybrid automata, but semi-algorithmic
              methods are known when the dynamics is relatively
              simple, namely a linear relation between the derivatives
              of the variables.  With the increasing complexity of
              nowadays systems, those models are however limited in
              their classical semantics, for modelling realistic
              implementations or dynamical systems.

              In this thesis, we study the algorithmics of
              \emph{complex semantics} for timed and hybrid automata.
              On the one hand, we propose implementable semantics for
              timed automata and we study their computational
              properties: by contrast with other works, we identify a
              semantics that is implementable and that has decidable
              properties.  On the other hand, we give new algorithmic
              approaches to the analysis of hybrid automata whose
              dynamics is given by an affine function of its
              variables."
}

@MastersThesis{Ellenbogen04th,
  Author = "R. Ellenbogen",
  Title = "Fully Automatic Verification of Absence of Errors
           via Interprocedural Integer Analysis",
  School = "School of  Computer Science, Tel-Aviv University",
  Address = "Tel-Aviv, Israel",
  Month = dec,
  Year = 2004,
  Abstract = "We present a interprocedural C String Static Verifier
              (iCSSV), a whole program analysis algorithm for
              verifying the safety of string operations in C
              programs. The algorithm automatically proves linear
              relationships among pointer expressions. The algorithm
              is conservative, i.e., it infers only valid
              relationships although it may fail to detect some of
              them. The algorithm is targeted to programs with
              ``shallow'' pointers and complex integer
              relationships. Therefore, the algorithm combines
              context-sensitive flow-insensitive pointer analysis of
              pointer updates with contextsensitive and flow-sensitive
              integer analysis of properties of allocation
              sites. Context-sensitivity is achieved by specializing
              pointer aliases to the context and functional integer
              analysis. The algorithm is powerful enough to verify the
              absence of string manipulation errors such as accesses
              beyond buffer length and null terminating
              character. Here the interprocedural analysis guarantees
              that our algorithm is fully automatic, i.e., does not
              require user annotations or any other intervention. A
              prototype of the algorithm was implemented. Several
              novel techniques are employed to make the
              interprocedural analysis of realistic programs
              feasible."
}

@Inproceedings{FagesR09,
  Author = "F. Fages and A. Rizk",
  Title = "From Model-Checking to Temporal Logic Constraint Solving",
  Booktitle = "Proceedings of the 15th International Conference
               on Principles and Practice of Constraint Programming (CP 2009)",
  Address = "Lisbon, Portugal",
  Editor = "I. P. Gent",
  Series = "Lecture Notes in Computer Science",
  Volume = 5732,
  Year = 2009,
  Pages = "319--334",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-04243-0",
  Abstract = "In this paper, we show how model-checking can be
              generalized to temporal logic constraint solving, by
              considering temporal logic formulae with free variables
              over some domain ${\mathcal D}$, and by computing a
              validity domain for the variables rather than a truth
              value for the formula. This allows us to define a
              continuous degree of satisfaction for a temporal logic
              formula in a given structure, opening up the field of
              model-checking to optimization. We illustrate this
              approach with reverse-engineering problems coming from
              systems biology, and provide some performance figures on
              parameter optimization problems with respect to temporal
              logic specifications."
}

@Inproceedings{FenacciM11,
  Author = "D. Fenacci and K. MacKenzie",
  Title = "Static Resource Analysis for {Java} Bytecode Using Amortisation
           and Separation Logic",
  Booktitle = "Proceedings of the 6th Workshop on Bytecode Semantics,
               Verification, Analysis and Transformation (Bytecode 2011)",
  Address = "Saarbrucken, Germany",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 279,
  Number = 1,
  Pages =  "19--32",
  Year = 2011,
  ISSN = "1571-0661",
  Abstract = "In this paper we describe a static analyser for Java
              bytecode which uses a combination of amortised analysis
              and Separation Logic due to Robert Atkey. With the help
              of Java annotations we are able to give precise resource
              utilisation constraints for Java methods which
              manipulate various heap-based data structures."
}

@Inproceedings{FioravantiPPS12,
  Author = "F. Fioravanti and A. Pettorossi and M. Proietti and V. Senni",
  Title = "Using Real Relaxations during Program Specialization",
  Booktitle = "Logic Program Synthesis and Transformation:
               Proceedings of the 21st International Symposium",
  Address = "Odense, Denmark",
  Editor = "G. Vidal",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7225,
  Pages = "106--122",
  Year = 2012,
  ISBN = "978-3-642-32210-5 (Print) 978-3-642-32211-2 (Online)",
  Abstract = "We propose a program specialization technique for
              locally stratified CLP(Z) programs, that is, logic
              programs with linear constraints over the set Z of the
              integer numbers. For reasons of efficiency our technique
              makes use of a relaxation from integers to reals. We
              reformulate the familiar unfold/fold transformation
              rules for CLP programs so that: (i) the applicability
              conditions of the rules are based on the satisfiability
              or entailment of constraints over the set R of the real
              numbers, and (ii) every application of the rules
              transforms a given program into a new program with the
              same perfect model constructed over Z. Then, we
              introduce a strategy which applies the transformation
              rules for specializing CLP(Z) programs with respect to a
              given query. Finally, we show that our specialization
              strategy can be applied for verifying properties of
              infinite state reactive systems specified by constraints
              over Z."
}

@Article{FioravantiPPS12-FI,
  Author = "F. Fioravanti and A. Pettorossi and M. Proietti and V. Senni",
  Title = "Improving Reachability Analysis of Infinite State Systems by Specialization",
  Journal = "Fundamenta Informaticae",
  Publisher = "IOS Press",
  Volume = 119,
  Number = "3--4",
  Pages = "281--300",
  Year = 2012,
  ISSN = "0169-2968 (Print) 1875-8681 (Online)",
  Abstract = "We consider infinite state reactive systems specified by
              using linear constraints over the integers, and we
              address the problem of verifying safety properties of
              these systems by applying reachability analysis
              techniques. We propose a method based on program
              specialization, which improves the effectiveness of the
              backward and forward reachability analyses. For backward
              reachability our method consists in: (i) specializing
              the reactive system with respect to the initial states,
              and then (ii) applying to the specialized system the
              reachability analysis that works backwards from the
              unsafe states. For reasons of efficiency, during
              specialization we make use of a relaxation from integers
              to reals. In particular, we test the satisfiability or
              entailment of constraints over the real numbers, while
              preserving the reachability properties of the reactive
              systems when constraints are interpreted over the
              integers. For forward reachability our method works as
              for backward reachability, except that the role of the
              initial states and the unsafe states are
              interchanged. We have implemented our method using the
              MAP transformation system and the ALV verification
              system. Through various experiments performed on several
              infinite state systems, we have shown that our
              specialization-based verification technique considerably
              increases the number of successful verifications without
              a significant degradation of the time performance."
}

@MastersThesis{Flexeder05th,
  Author = "A. Flexeder",
  Title = "{Interprozedurale Analyse linearer Ungleichungen}",
  Type = "Diploma thesis",
  School = "Technische {Universit\"at} {M\"unchen}",
  Address = "{M\"unchen}, Germany",
  Month = jul,
  Year = 2005,
  Note = "In German",
  Abstract = "Diese Arbeit beschreibt eine intra- und auch
              interprozedurale Datenflussanalyse, welche an jedem
              Programmpunkt statisch die Beziehungen, die zwischen den
              Programmvariablen gelten, bestimmen k\"onnen. Die
              intraprozeduralen Analyse, beruhend auf einem Modell von
              Cousot [P.~Cousot and N.~Halbwachs. Automatic discovery
              of linear restraints among variables of a program.
              Conference Record of the 5th Annunal ACM Symposium on
              Principles of Programming Languages, pages 84--96, 1978]
              interpretiert lineare Zuweisungen und Bedingungen und
              betrachtet die nicht linearen Konstrukte mit Hilfe von
              nicht linearen Zuweisungen. Mit dieser Abstraktion
              versucht man lineare Gleichheits- und
              Ungleichheitsbeziehungen zwischen den Programmvariablen
              in Form von Polyedern rauszufinden. Da man nicht nur
              eine Funktion, sondern ganze Programme als Zusammenspiel
              mehrerer Funktionen, analysieren m\"ochte, ist eine
              interprozedurale Analyse n\"otig [M.~Mueller-Olm and
              H.~Seidl.  Precise Interprocedural Analysis through
              Linear Algebra. POPL, 2004]. Diese soll mit den Mitteln
              der linearen Algebra die affinen Beziehungen, welche
              zwischen den Programmvariablen an einem bestimmten
              Programmpunkt gelten, erkennen. Die Behandlung von
              Prozeduraufrufen steht dabei im Vordergrund."
}

@Inproceedings{FouiheMP13,
  Author = "A. Fouilhe and D. Monniaux and M. P{\'e}rin,
  Title = "Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra",
  Booktitle = "Static Analysis:
               Proceedings of the 20th International Symposium",
  Address = "Seattle, USA",
  Series = "Lecture Notes in Computer Science",
  Editor = "F. Logozzo and M. F{\"a}hndrich",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-38855-2 (Print) 978-3-642-38856-9 (Online)",
  Volume = 7935,
  pages = "345--365",
  Year = 2013,
  Abstract = "Polyhedra form an established abstract domain for
              inferring runtime properties of programs using abstract
              interpretation. Computations on them need to be
              certified for the whole static analysis results to be
              trusted. In this work, we look at how far we can get
              down the road of a posteriori verification to lower the
              overhead of certification of the abstract domain of
              polyhedra. We demonstrate methods for making the cost of
              inclusion certificate generation negligible. From a
              performance point of view, our single-representation,
              constraints-based implementation compares with
              state-of-the-art implementations."
}

@MastersThesis{FrankM02th,
  Author = "S. Frank and P. R. Mai",
  Title = "Strategies for Cooperating Constraint Solvers",
  Type = "Diploma thesis",
  School = "Technische {Universit\"at} Berlin",
  Address = "Berlin, Germany",
  Month = jul,
  Year = 2002,
  Abstract = "Cooperative constraint solving has been investigated by
              several different research groups and individuals as it
              provides a comfortable mechanism to attack multi-domain
              constraint problems. The theoretical framework of
              Hofstedt [P.~Hofstedt. Cooperation and Coordination of
              Constraint Solvers. PhD thesis, Technische
              {Universit\"at} Dresden, March 2001. Shaker Verlag,
              Aachen] provided the basis for the prototypical
              implementation described in [E.~Godehardt and
              D.~Seifert.  Kooperation und Koordination von Constraint
              Solvern --- Implementierung eines Prototyps. Master's
              thesis, Technische Universit{\"a}t Berlin, January
              2001]. Taking aboard the lessons learned in the
              prototype, we introduce a revised implementation of the
              framework, to serve as a flexible basis for the
              conception and evaluation of advanced strategies for
              solver cooperation. Several additional enhancements and
              optimisations over the preceding implementation or the
              underlying theoretical framework are described, proving
              the correctness of those changes where necessary. Using
              the newly implemented framework, we propose and
              benchmark a set of new cooperation strategies,
              iteratively refining them to the point where we can
              offer a set of generally useful (i.e. non-problem
              specific) strategies. Finally we introduce a strategy
              language, that allows the user to define
              problem-specific strategies, either from scratch or
              derived from other strategies, and demonstrate the
              effectiveness of the language on a well-known example
              problem."
}

@Inproceedings{Frehse04,
  Author = "G. Frehse",
  Title = "Compositional Verification of Hybrid Systems
           with Discrete Interaction Using Simulation Relations",
  Booktitle = "Proceedings of the IEEE Conference on Computer Aided
               Control Systems Design (CACSD 2004)",
  Address = "Taipei, Taiwan",
  Year = 2004,
  Abstract = "Simulation relations can be used to verify refinement
              between a system and its specification, or between
              models of different complexity. It is known that for the
              verification of safety properties, simulation between
              hybrid systems can be defined based on their labeled
              transition system semantics. We show that for hybrid
              systems without shared variables, which therefore only
              interact at discrete events, this simulation preorder is
              compositional, and present assume-guarantee rules that
              help to counter the state explosion problem. Some
              experimental results for simulation checking of linear
              hybrid automata are provided using a prototype tool with
              exact arithmetic and unlimited digits."
}

@Inproceedings{FrehseHK04,
  Author = "G. Frehse and Z. Han and B. Krogh",
  Title = "Assume-Guarantee Reasoning for Hybrid {I/O}-Automata
           by Over-Approximation of Continuous Interaction",
  Booktitle = "Proceedings of the
               43rd IEEE Conference on Decision and Control (CDC 2004)",
  Address = "Atlantis, Paradise Island, Bahamas",
  Year = 2004,
  Abstract = "This paper extends assume-guarantee reasoning (AGR) to
              hybrid dynamic systems that interact through continuous
              state variables. We use simulation relations for timed
              transition systems to analyze compositions of hybrid I/O
              automata. This makes it possible to perform
              compositional reasoning that is conservative in the
              sense of over approximating the composed behaviors. In
              contrast to previous approaches that require global
              receptivity conditions, circularity is broken in our
              approach by a state-based nonblocking condition that can
              be checked in the course of computing the AGR simulation
              relations. The proposed procedures for AGR are
              implemented in a computational tool for the case of
              linear hybrid I/O automata, and the approach is
              illustrated with a simple example."
}

@Inproceedings{Frehse05,
  Author = "G. Frehse",
  Title = "{PHAVer}: Algorithmic Verification of Hybrid Systems Past {HyTech}",
  Booktitle = "Hybrid Systems: Computation and Control:
               Proceedings of the 8th International Workshop (HSCC 2005)",
  Address = "Z{\"u}rich, Switzerland",
  Editor = "M. Morari and L. Thiele",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3414,
  Pages = "258--273",
  Year = 2005,
  Abstract = "In 1995, HyTech broke new ground as a potentially
              powerful tool for verifying hybrid systems --- yet it has
              remained severely limited in its applicability to more
              complex systems.  We address the main problems of HyTech
              with PHAVer, a new tool for the exact verification of
              safety properties of hybrid systems with piecewise
              constant bounds on the derivatives.  Affine dynamics are
              handled by on-the-fly overapproximation and by
              partitioning the state space based on user-definable
              constraints and the dynamics of the system.  PHAVer's
              exact arithmetic is robust due to the use of the Parma
              Polyhedra Library, which supports arbitrarily large
              numbers. To manage the complexity of the polyhedral
              computations, we propose methods to conservatively limit
              the number of bits and constraints of polyhedra.
              Experimental results for a navigation benchmark and a
              tunnel diode circuit show the effectiveness of the
              approach."
}

@PhdThesis{Frehse05th,
  Author = "G. Frehse",
  Title = "Compositional Verification of Hybrid Systems
           using Simulation Relations",
  School = "Radboud Universiteit Nijmegen",
  Address = "Nijmegen, The Netherlands",
  Month = oct,
  Year = 2005,
}

@Article{Frehse08,
  Author = "G. Frehse",
  Title = "{PHAVer}: Algorithmic Verification of Hybrid Systems Past {HyTech}",
  Journal = "Software Tools for Technology Transfer",
  Publisher = "Springer-Verlag, Berlin",
  Volume = 10,
  Number = 3,
  Year = 2008,
  Pages = "263--279",
  Abstract = "In 1995, HyTech broke new ground as a potentially
              powerful tool for verifying hybrid systems --- yet its
              appicability remains limited to relatively simple
              systems. We address the main problems of HyTech with
              PHAVer, a new tool for the exact verification of safety
              properties of hybrid systems with piecewise constant
              bounds on the derivatives. Affine dynamics are handled
              by on-the-fly overapproximation, partitioning the state
              space based on user-definable constraints and the
              dynamics of the system. PHAVer features exact arithmetic
              in a robust implementation that, based on the Parma
              Polyhedra Library, supports arbitrarily large
              numbers. To manage the complexity of the polyhedral
              computations, we propose methods to conservatively limit
              the number of bits and constraints of
              polyhedra. Experimental results for a navigation
              benchmark and a tunnel diode circuit show the
              effectiveness of the approach."
}

@Inproceedings{FrehseKRM06,
  Author = "G. Frehse and B. H. Krogh and R. A. Rutenbar and O. Maler",
  Title = "Time Domain Verification of Oscillator Circuit Properties",
  Booktitle = "Proceedings of the First Workshop on Formal Verification
               of Analog Circuits (FAC 2005)",
  Address = "Edinburgh, Scotland",
  Pages = "9--22",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 153,
  Number = 3,
  Year = 2006,
  Abstract = "The application of formal methods to analog and mixed
              signal circuits requires efficient methods for
              constructing abstractions of circuit behaviors. This
              paper concerns the verification of properties of
              oscillator circuits. Generic monitor automata are
              proposed to facilitate the application of hybrid system
              reachability computations to characterize time domain
              features of oscillatory behavior, such as bounds on the
              signal amplitude and jitter. The approach is illustrated
              for a nonlinear tunnel-diode circuit model using PHAVer,
              a hybrid system analysis tool that provides sound
              verification results based on linear hybrid automata
              approximations and infinite precision computations."
}

@Inproceedings{FrehseKR06,
  Author = "G. Frehse and B. H. Krogh and R. A. Rutenbar",
  Title = "Verifying Analog Oscillator Circuits Using Forward/Backward
           Refinement",
  Booktitle = "Proceedings of the 9th Conference on Design, Automation
               and Test in Europe (DATE 06)",
  Address = "Munich, Germany",
  Publisher = "ACM SIGDA",
  Year = 2006,
  Note = "{CD-ROM} publication",
  Abstract = "Properties of analog circuits can be verified formally
              by partitioning the continuous state space and applying
              hybrid system verification techniques to the resulting
              abstraction.  To verify properties of oscillator
              circuits, cyclic invariants need to be computed. Methods
              based on forward reachability have proven to be
              inefficient and in some cases inadequate in constructing
              these invariant sets. In this paper we propose a novel
              approach combining forward- and backward-reachability
              while iteratively refining partitions at each step. The
              technique can yield dramatic memory and runtime
              reductions. We illustrate the effectiveness by
              verifying, for the first time, the limit cycle
              oscillation behavior of a third-order model of a
              differential VCO circuit."
}

@Inproceedings{FribourgK11,
  author    = "L. Fribourg and U. K{\"u}hne",
  title     = "Parametric Verification and Test Coverage for Hybrid Automata
               Using the Inverse Method",
  Booktitle = "In Proceedings of the 5th International Workshop
               on Reachability Problems (RP 2011)",
  Address = "Genova, Italy",
  Series = "Lecture Notes in Computer Science",
  Editor = "G. Delzanno and I. Potapov",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-24287-8",
  Pages =  "191--204",
  Volume = 6945,
  Year = 2011,
  Abstract = "Hybrid systems combine continuous and discrete
              behavior.  Hybrid Automata are a powerful formalism for
              the modeling and verification of such systems. A common
              problem in hybrid system verification is the good
              parameters problem, which consists in identifying a set
              of parameter valuations which guarantee a certain
              behavior of a system. Recently, a method has been
              presented for attacking this problem for Timed
              Automata. In this paper, we show the extension of this
              methodology for hybrid automata with linear and affine
              dynamics. The method is demonstrated with a hybrid
              system benchmark from the literature."
}

@Inproceedings{Fu14,
  Author = "Z. Fu",
  Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java",
  Booktitle = "Verification, Model Checking, and Abstract Interpretation:
               Proceedings of the 15th International Conference (VMCAI 2014)",
  Address = "San Diego, US",
  Editor = "K. McMillan and X. Rival",
  Publisher = "Springer-Verlag, Berlin",
  Year = 2014,
  Abstract = "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."
}

@Article{GallardoP13,
  Author = "{M.-d.-M}. Gallardo and L.Panizo",
  Title = "Extending model checkers for hybrid system verification: the case study of SPIN.",
  Journal = "Software Testing, Verification and Reliability",
  Publisher = "John Wiley & Sons, Ltd.",
  DOI = "10.1002/stvr.1505",
  ISSN ="1099-1689 (online)",
  Year = 2013,
  Note = "Early View (Online Version of Record published before inclusion in an issue)",
  Abstract = "A hybrid system is a system that evolves following a
              continuous dynamic, which may instantaneously change
              when certain internal or external events occur. Because
              of this combination of discrete and continuous dynamics,
              the behaviour of a hybrid system is, in general,
              difficult to model and analyse. Model checking
              techniques have been proven to be an excellent approach
              to analyse critical properties of complex systems. This
              paper presents a new methodology to extend explicit
              model checkers for hybrid systems analysis. The explicit
              model checker is integrated, in a non-intrusive way,
              with some external structures and existing abstraction
              libraries, which store and manipulate the abstraction of
              the continuous behaviour irrespective of the underlying
              model checker. The methodology is applied to SPIN using
              Parma Polyhedra Library. In addition, the authors are
              currently working on the extension of other model
              checkers."
}
@Inproceedings{MihailaSS13,
  Author = "{P.-L}. Garoche and T. Kahsai and C. Tinelli",
  Title = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers",
  Booktitle = "Proceedings of the 5th International Symposium on {NASA} Formal Methods, {NFM} 2013",
  Editor = "G. Brat and N. Rungta and A. Venet",
  Address = "Moffett Field, CA, USA",
  Pages = "139--154",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7871,
  Year = 2013,
  Abstract = "Formal analysis tools for system models often require or
              benefit from the availability of auxiliary system
              invariants. Abstract interpretation is currently one of
              the best approaches for discovering useful invariants,
              in particular numerical ones. However, its application
              is limited by two orthogonal issues: (i) developing an
              abstract interpretation is often non-trivial; each
              transfer function of the system has to be represented at
              the abstract level, depending on the abstract domain
              used; (ii) with precise but costly abstract domains, the
              information computed by the abstract interpreter can be
              used only once a post fix point has been reached; this
              may take a long time for large systems or when widening
              is delayed to improve precision. We propose a new,
              completely automatic, method to build abstract
              interpreters which, in addition, can provide sound
              invariants of the system under analysis before reaching
              the end of the post fix point computation. In effect,
              such interpreters act as on-the-fly invariant generators
              and can be used by other tools such as logic-based model
              checkers. We present some experimental results that
              provide initial evidence of the practical usefulness of
              our method."
}

@PhdThesis{Gobert07th,
  Author = "F. Gobert",
  Title = "Towards putting abstract interpretation of {Prolog} into practice:
           design, implementation, and evaluation of a tool to verify
           and optimise Prolog programs",
  School = "Universit\'e catholique de Louvain",
  Address = "Louvain-la-Neuve, Belgium",
  Month = dec,
  Year = 2007,
  Abstract = "Logic programming is an attractive paradigm that allows
              the programmer to concentrate on the meaning (the logic)
              of the problem to be solved - the \emph{declarative layer}.
              An execution model is then used as the problem solver - the
              \emph{operational layer}. In practice, for efficiency reasons,
              the semantics of the two layers do not always match. For
              instance, in Prolog, the computation of solutions is based
              on an incomplete depth-first search rule, unifications and
              negations may be unsound, some builtin language primitives
              are not multidirectional, and there exist extralogical
              features like the cut or dynamic predicates. A large number
              of work has been realised to reconcile the declarative and
              operational features of Prolog. Methodologies have been
              proposed to construct operationally correct and efficient
              Prolog code. Researchers have designed methods to automate
              the verification of specific operational properties on which
              optimisation of logic programs can be based. A few tools have
              been implemented but there is a lack of a unified framework.
              The goal and topic of this thesis is the design, implementation,
              and evaluation of a static analyser of Prolog programs to
              integrate `state-of-the-art' techniques into a unified abstract
              interpretation framework. Abstract interpretation is an
              adequate methodology to design, justify, and combine complex
              analyses. The analyser that we present in this thesis is based
              on a non-implemented original proposal. The original framework
              defines the notion of \emph{abstract sequence}, which allows
              one to verify many desirable operational properties of a logic
              procedure. The properties include verifying type, mode, and
              sharing of terms, proving termination, sure success or failure,
              and determinacy of logic procedures, as well as linear
              relations between the size of input/output terms and the
              number of solutions to a call. An abstract sequence maintains
              information about the input and output terms, as well as the
              non-failure conditions on input terms, and the number of
              solutions for such inputs. The domains of abstract sequences
              cooperate together and improve each other. The abstract
              execution is performed during a single global analysis,
              and abstract sequences are derived at each program point
              (the information of the various domains are computed
              simultaneously). The intended operational properties of a
              procedure are written in formal specifications.
              The original framework is an interesting starting point for
              combining several analyses inside a unified framework.
              However, it is limited and inaccurate in many ways: it is
              not implemented, and therefore, it has not been validated
              by experiments, it accepts only a subset of Prolog (without
              negation, cut, conditional and disjunctive constructs), and
              some of the proposed domains are not precise enough.
              The basic framework is only oriented towards the verification
              of Prolog programs, but it cannot always prove the desirable
              properties. In this thesis, we implement and evaluate the
              basic framework, and, more importantly, we overcome its
              limitations to make it accurate and usable in practice:
              the improved framework accepts any Prolog program with modules,
              new abstract domains and operations are added, and the
              language of specifications is more expressive. We also
              design and implement an optimiser that generates specialised
              code. Optimisation is essential in Prolog, but it is not easy
              to perform by hand and it is error prone. The optimiser uses
              the information to safely apply source-to-source
              transformations. Code transformations include clause and
              literal reordering, introduction of cuts, and removal
              of redundant literals. The optimiser follows a precise
              strategy to choose the most rewarding transformations in best
              order.
              This thesis shows the feasibility of a unified framework
              that integrates many complex analyses in a single global
              analysis. Practically and theoretically, a single global
              analysis is more attractive than a combination of a lot of
              separate analyses and frameworks. Many extensions have been
              performed to obtain an accurate and usable tool devoted to
              verification and optimisation of Prolog programs."
}

@Inproceedings{GobertLC07,
  Author = "F. Gobert and B. {Le Charlier}",
  Title = "A System to Check Operational Properties of Logic Programs",
  Pages = "245--259",
  Booktitle = "Approches Formelles dans l'Assistance au D\'eveloppement
               de Logiciels: Actes de la 8e conf\'erence",
  Publisher = "Universit\'e de Namur, Belgium",
  Editor = "M.-L. Potet and P.-Y. Schobbens and H. Toussaint and G. Saval",
  Year = 2007,
  ISBN = "978-2-87037-559-4",
  Abstract = "An implemented static analyser of logic programs is presented.
              The system is based on a unied abstract interpretation
              framework, which allows the integration of several analyses
              devoted to verication and optimisation. The analyser is able
              to verify many desirable properties of logic programs executed
              with the search-rule and other specic features of Prolog.
              Such operational properties include verifying type, mode,
              sharing, and linearity of terms, proving termination,
              occur-check freeness, sure success or failure, and determinacy
              of logic procedures, as well as linear relations between the
              size of input/output terms and the number of solutions to a
              call. It is emphasized how each analysis may contribute to
              each other.",
}

@Inproceedings{GonnordH06,
  Author = "L. Gonnord and N. Halbwachs",
  Title = "Combining Widening and Acceleration in Linear Relation Analysis",
  Booktitle = "Static Analysis:
               Proceedings of the 13th International Symposium",
  Address = "Seoul, Korea",
  Editor = "K. Yi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4134,
  Pages = "144--160",
  Year = 2006,
  ISBN = "3-540-37756-5",
  Abstract = "Linear Relation Analysis [CH78,Hal79] is one of the
              first, but still one of the most powerful, abstract
              interpretations working in an infinite lattice. As such,
              it makes use of a widening operator to enforce the
              convergence of fixpoint computations. While the
              approximation due to widening can be arbitrarily refined
              by delaying the application of widening, the analysis
              quickly becomes too expensive with the increase of
              delay. Previous attempts at improving the precision of
              widening are not completely satisfactory, since none of
              them is guaranteed to improve the precision of the
              result, and they can nevertheless increase the cost of
              the analysis. In this paper, we investigate an
              improvement of Linear Relation Analysis consisting in
              computing, when possible, the exact (abstract) effect of
              a loop. This technique is fully compatible with the use
              of widening, and whenever it applies, it improves both
              the precision and the performance of the analysis.",
}

@PhdThesis{Gopan07th,
  Author = "D. Gopan",
  Title = "Numeric Program Analysis Techniques with Applications
           to Array Analysis and Library Summarization",
  School = "University of Wisconsin",
  Address = "Madison, Wisconsin, USA",
  Month = aug,
  Year = 2007,
  Abstract = "Numeric program analysis is of great importance for the
              areas of software engineering, software
              verification, and security: to identify many program
              errors, such as out-of-bounds array accesses and
              integer overflows, which constitute the lion's share
              of security vulnerabilities reported by CERT, an
              analyzer needs to establish numeric properties of
              program variables. Many important program analyses,
              such as low-level code analysis, memory-cleanness
              analysis, and shape analysis, rely in some ways on
              numeric-program-analysis techniques. However,
              existing numeric abstractions are complex (numeric
              abstract domains are typically non-distributive, and
              form infinite-height lattices); thus, obtaining
              precise numeric-analysis results is by no means a
              trivial undertaking.
              In this thesis, we develop a suite of techniques with
              the common goal of improving the precision and applicability
              of numeric program analysis. The techniques address
              various aspects of numeric analysis, such as
              handling dynamically-allocated memory, dealing with
              programs that manipulate arrays, improving the
              precision of extrapolation (widening), and
              performing interprocedural analysis. The techniques
              use existing numeric abstractions as building
              blocks. The communication with existing abstractions
              is done strictly through a generic abstract-domain
              interface. The abstractions constructed by our
              techniques also expose that same interface, and
              thus, are compatible with existing analysis
              engines. As a result, our techniques are independent
              from specific abstractions and specific analysis
              engines, can be easily incorporated into existing
              program-analysis tools, and should be readily
              compatible with new abstractions to be introduced in
              the future.
              A practical application of numeric analysis that we consider
              in this thesis is the automatic generation of summaries for
              library functions from their low-level
              implementation (that is, from a library's
              binary). The source code for library functions is
              typically not available. This poses a stumbling
              block for many source-level program
              analyses. Automatic generation of summary functions
              will both speed up and improve the accuracy of
              library-modeling, a process that is currently
              carried out by hand. This thesis addresses the
              automatic generation of summaries for memory-safety
              analysis."
}

@Inproceedings{GopanR06,
  Author = "D. Gopan and T. W. Reps",
  Title = "Lookahead Widening",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 18th International Conference (CAV 2006)",
  Address = "Seattle, Washington, USA",
  Editor = "T. Ball and R. B. Jones",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4144,
  Pages = "452--466",
  Year = 2006,
  Abstract = "We present \emph{lookahead widening}, a novel technique
              for using existing widening and narrowing operators to
              improve the precision of static analysis. This technique
              is both self-contained and fully-automatic in the sense
              that it does not rely on separate analyzes or human
              involvement. We show how to integrate lookahead widening
              into existing analyzers with minimal
              effort. Experimental results indicate that the technique
              is able to achieve sizable precision improvements at
              reasonable costs.",
}

@Inproceedings{GopanR07a,
  Author = "D. Gopan and T. W. Reps",
  Title = "Low-Level Library Analysis and Summarization",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 19th International Conference (CAV 2007)",
  Address = "Berlin, Germany",
  Editor = "W. Damm and H. Holger",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4590,
  Pages = "68--81",
  Year = 2007,
  ISBN = "3-540-73367-6",
  Abstract = "Programs typically make extensive use of libraries,
              including dynamically linked libraries, which are often
              not available in source-code form, and hence not
              analyzable by tools that work at source level (i.e.,
              that analyze intermediate representations created from
              source code). A common approach is to write
              \emph{library models} by hand. A library model is a
              collection of function stubs and variable declarations
              that capture some aspect of the library code's
              behavior. Because these are hand-crafted, they are
              likely to contain errors, which may cause an analysis to
              return incorrect results.

              This paper presents a method to construct summary
              information for a library function automatically by
              analyzing its low-level implementation (i.e., the
              library's binary).",
}

@Inproceedings{GopanR07b,
  Author = "D. Gopan and T. W. Reps",
  Title = "Guided Static Analysis",
  Booktitle = "Static Analysis:
               Proceedings of the 14th International Symposium",
  Address = "Kongens Lyngby, Denmark",
  Editor = "G. Fil\'e and H. R. Nielson",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4634,
  ISBN = "978-3-540-74060-5",
  Pages = "349--365",
  Year = 2007,
  Abstract = "In static analysis, the semantics of the program is
              expressed as a set of equations. The equations are
              solved iteratively over some abstract domain. If the
              abstract domain is distributive and satisfies the
              ascending-chain condition, an iterative technique yields
              the most precise solution for the equations. However, if
              the above properties are not satisfied, the solution
              obtained is typically imprecise. Moreover, due to
              the properties of widening operators, the precision loss
              is sensitive to the order in which the state-space is
              explored.

              In this paper, we introduce \emph{guided static analysis},
              a framework for controlling the exploration of the
              state-space of a program. The framework guides the
              state-space exploration by applying standard
              static-analysis techniques to a sequence of modified
              versions of the analyzed program. As such, the framework
              does not require any modifications to existing analysis
              techniques, and thus can be easily integrated into
              existing static-analysis tools.

              We present two instantiations of the framework, which
              improve the precision of widening in (i) loops with
              multiple phases and (ii) loops in which the transformation
              performed on each iteration is chosen non-deterministically.",
}

@Inproceedings{GopanRS05,
  Author = "D. Gopan and T. W. Reps and M. Sagiv",
  Title = "A Framework for Numeric Analysis of Array Operations",
  Booktitle = "Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium
               on Principles of Programming Languages",
  Address = "Long Beach, California, USA",
  Pages = "338--350",
  Year = 2005,
  Abstract = "Automatic discovery of relationships among values of
              array elements is a challenging problem due to the
              unbounded nature of arrays. We present a framework for
              analyzing array operations that is capable of capturing
              numeric properties of array elements. In particular, the
              analysis is able to establish that all array elements
              are initialized by an array-initialization loop, as well
              as to discover numeric constraints on the values of
              initialized elements.  The analysis is based on the
              combination of canonical abstraction and summarizing
              numeric domains. We describe a prototype implementation
              of the analysis and discuss our experience with applying
              the prototype to several examples, including the
              verification of correctness of an insertion-sort
              procedure."
}

@Inproceedings{BandaG10a,
  Author = "G. Banda and J. P. Gallagher",
  Title = "Constraint-Based Abstraction of a Model Checker
           for Infinite State Systems",
  Booktitle = "Proceedings of the 23rd Workshop on (Constraint)
               Logic Programming (WLP 2009)",
  Editor = "U. Geske and A. Wolf",
  Address = "Potsdam, Germany",
  Publisher = "Potsdam Universit{\"a}tsverlag",
  Year = 2010,
  Pages = "109--124",
  Abstract = "Abstract interpretation-based model checking provides an
              approach to verifying properties of infinite-state
              systems. In practice, most previous work on abstract
              model checking is either restricted to verifying
              universal properties, or develops special techniques for
              temporal logics such as modal transition systems or
              other dual transition systems. By contrast we apply
              completely standard techniques for constructing abstract
              interpretations to the abstraction of a CTL semantic
              function, without restricting the kind of properties
              that can be verified.  Furthermore we show that this
              leads directly to implementation of abstract model
              checking algorithms for abstract domains based on
              constraints, making use of an SMT solver."
}

@Inproceedings{BandaG10b,
  Author = "G. Banda and J. P. Gallagher",
   Title = "Constraint-Based Abstract Semantics for Temporal Logic:
            A Direct Approach to Design and Implementation",
   Booktitle = "Proceedings of the 17th International Conference
                on Logic for Programming,
                Artificial Intelligence, and Reasoning (LPAR 2010)",
   Address = "Yogyakarta, Indonesia",
   Series = "Lecture Notes in Computer Science",
   Editor = "E. Clarke and A. Voronkov",
   Publisher = "Springer-Verlag, Berlin",
   ISBN = "978-3-642-17510-7",
   Year = 2010,
   Pages =  "27--45",
   Volume = 6355,
   Abstract = "Abstract interpretation provides a practical approach
               to verifying properties of infinite-state systems. We
               apply the framework of abstract interpretation to
               derive an abstract semantic function for the modal ?
               -calculus, which is the basis for abstract model
               checking. The abstract semantic function is constructed
               directly from the standard concrete semantics together
               with a Galois connection between the concrete
               state-space and an abstract domain. There is no need
               for mixed or modal transition systems to abstract
               arbitrary temporal properties, as in previous work in
               the area of abstract model checking. Using the modal ?
               -calculus to implement CTL, the abstract semantics
               gives an over-approximation of the set of states in
               which an arbitrary CTL formula holds. Then we show that
               this leads directly to an effective implementation of
               an abstract model checking algorithm for CTL using
               abstract domains based on linear constraints. The
               implementation of the abstract semantic function makes
               use of an SMT solver. We describe an implemented system
               for proving properties of linear hybrid automata and
               give some experimental results."
}

@Inproceedings{Grosser09,
  Author = "T. Grosser",
  Title = "Optimization opportunities based on the polyhedral model in
           {GRAPHITE}. How much impact has {GRAPHITE} already?",
  Booktitle = "Proceedings of the {GCC} Developers' Summit",
  Address = "Montreal, Quebec, Canada",
  Year = 2009,
  Month = jun,
  Pages = "33--46",
  URL = "http://www.gccsummit.org/2009/gcc09-proceedings.pdf",
  Abstract = "The polytope model is used since many years to describe
              standard loop optimizations like blocking, interchange
              or fusion, but also advanced memory access optimizations
              and automatic parallelization. Its exact mathematical
              description of memory accesses and loop iterations
              allows to concentrate on the optimization problem and to
              take advantage of professional problem solving tools
              developed for operational research.  Up to today the
              polytope model was limited to research compilers or
              source to source transformations. Graphite generates a
              polytope description of all programs compiled by the
              gcc. Therefore polytope optimization techniques are not
              limited anymore to hand selected code pieces, but can
              actually be applied in large scale on real world
              programs. By showing the impact of GRAPHITE on important
              benchmarks --- ``How much runtime is actually spent in
              code, that can be optimized by polytope optimization
              techniques?'' --- we invite people to base their current
              polytope research on GRAPHITE to make these
              optimizations available to the large set of gcc compiled
              applications."
}

@Inproceedings{GulavaniR06,
  Author = "B. S. Gulavani and S. K. Rajamani",
  Title = "Counterexample Driven Refinement for Abstract Interpretation",
  Booktitle = "Proceedings of the 12th International Conference on
               Tools and Algorithms for the Construction and Analysis
               of Systems (TACAS 2006)",
  Address = "Vienna, Austria",
  Editor = "H. Hermanns and J. Palsberg",
  Pages = "474--488",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3920,
  Year = 2006,
  ISBN = "3-540-33056-9",
  Abstract = "Abstract interpretation techniques prove properties of
              programs by computing abstract fixpoints. All such
              analyses suffer from the possibility of false errors. We
              present a new counterexample driven refinement technique
              to reduce false errors in abstract interpretations.  Our
              technique keeps track of the precision losses during
              forward fixpoint computation, and does a precise
              backward propagation from the error to either confirm
              the error as a true error, or identify a refinement so
              as to avoid the false error.  Our technique is quite
              simple, and is independent of the specific abstract
              domain used. An implementation of our technique for
              affine transition systems is able to prove invariants
              generated by the StInG tool [19] without doing any
              specialized analysis for linear relations. Thus, we hope
              that the technique can work for other abstract domains
              as well.We sketch how our technique can be used to
              perform shape analysis by simply defining an appropriate
              widening operator over shape graphs."
}

@Inproceedings{GulwaniL-AS09,
  Author = "S. Gulwani and T. Lev-Ami and S. Sagiv",
  Title = "A Combination Framework for Tracking Partition Sizes",
  Booktitle = "Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages (POPL 2009)",
  Address = "Savannah, Georgia, USA",
  Editor = "Z. Shao and B. C. Pierce",
  Publisher = "ACM Press",
  Pages = "239--251",
  Year = 2009,
  ISBN = "978-1-60558-379-2",
  Abstract = "We describe an abstract interpretation based framework
              for proving relationships between sizes of memory
              partitions. Instances of this framework can prove
              traditional properties such as memory safety and program
              termination but can also establish upper bounds on usage
              of dynamically allocated memory. Our framework also
              stands out in its ability to prove properties of
              programs manipulating both heap and arrays which is
              considered a difficult task.  Technically, we define an
              abstract domain that is parameterized by an abstract
              domain for tracking memory partitions (sets of memory
              locations) and by a numerical abstract domain for
              tracking relationships between cardinalities of the
              partitions. We describe algorithms to construct the
              transfer functions for the abstract domain in terms of
              the corresponding transfer functions of the
              parameterized abstract domains.  A prototype of the
              framework was implemented and used to prove interesting
              properties of realistic programs, including programs
              that could not have been automatically analyzed before."
}

@Article{HalbwachsMG06,
  Author = "N. Halbwachs and D. Merchat and L. Gonnord",
  Title = "Some Ways To Reduce the Space Dimension in Polyhedra Computations",
  Journal = "Formal Methods in System Design",
  Publisher = "Springer Netherlands",
  Volume = 29,
  Number = 1,
  Pages = "79--95",
  Year = 2006,
  Abstract = "Convex polyhedra are often used to approximate sets of
              states of programs involving numerical variables. The
              manipulation of convex polyhedra relies on the so-called
              \emph{double description}, consisting of viewing a
              polyhedron both as the set of solutions of a system of
              linear inequalities, and as the convex hull of a
              \emph{system of generators}, i.e., a set of vertices and
              rays. The cost of these manipulations is highly
              dependent on the number of numerical variables, since
              the size of each representation can be exponential in
              the dimension of the space. In this paper, we
              investigate some ways for reducing the dimension: On one
              hand, when a polyhedron satisfies \emph{affine
              equations}, these equations can obviously be used to
              eliminate some variables. On the other hand, when groups
              of variables are unrelated with each other, this means
              that the polyhedron is in fact a \emph{Cartesian
              product} of polyhedra of lower dimensions. Detecting
              such Cartesian factoring is not very difficult, but we
              adapt also the operations to work on Cartesian
              products. Finally, we extend the applicability of
              Cartesian factoring by applying suitable \emph{variable
              change}, in order to maximize the factoring."
}

@Inproceedings{HalbwachsMP-V03,
  Author = "N. Halbwachs and D. Merchat and C. Parent-Vigouroux",
  Title = "Cartesian Factoring of Polyhedra in Linear Relation Analysis",
  Booktitle = "Static Analysis:
               Proceedings of the 10th International Symposium",
  Address = "San Diego, California, USA",
  Editor = "R. Cousot",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 2694,
  Year = 2003,
  Pages = "355--365",
  Abstract = "Linear Relation Analysis [CH78] suffers from the cost of
              operations on convex polyhedra, which can be exponential
              with the number of involved variables. In order to
              reduce this cost, we propose to detect when a polyhedron
              is a Cartesian product of polyhedra of lower dimensions,
              i.e., when groups of variables are unrelated with each
              other. Classical operations are adapted to work on such
              factored polyhedra. Our implementation shows encouraging
              experimental results."
}

@Inproceedings{HenriksenG06,
  Author = "K. S. Henriksen and J. P. Gallagher",
  Title = "Abstract Interpretation of {PIC} Programs
           through Logic Programming",
  Booktitle = "Proceedings of the 6th IEEE International Workshop
               on Source Code Analysis and Manipulation",
  Address = "Sheraton Society Hill, Philadelphia, PA, USA",
  Publisher = "IEEE Computer Society Press",
  Pages = "184--196",
  Year = 2006,
  Abstract = "A logic based general approach to abstract
              interpretation of low-level machine programs is
              reported. It is based on modelling the behavior of the
              machine as a logic program.  General purpose program
              analysis and transformation of logic programs, such as
              partial evaluation and convex hull analysis, are applied
              to the logic based model of the machine.

              A small PIC microcontroller is used as a case study. An
              emulator for this microcontroller is written in Prolog,
              and standard programming transformations and analysis
              techniques are used to specialise this emulator with
              respect to a given PIC program. The specialised emulator
              can now be further analysed to gain insight into the
              given program for the PIC microcontroller.

              The method describes a general framework for applying
              abstractions, illustrated here by linear constraints and
              convex hull analysis, to logic programs. Using these
              techniques on the specialised PIC emulator, it is
              possible to obtain constraints on and linear relations
              between data registers, enabling detection of for
              instance overflows, branch conditions and so on."
}

@PhdThesis{Henriksen07th,
  Author = "K. S. Henriksen",
  Title = "A Logic Programming Based Approach to Applying
           Abstract Interpretation to Embedded Software",
  School = "Computer Science, Roskilde University",
  Month = oct,
  Address = "Roskilde, Denmark",
  Year = 2007,
  Note = "Published as Computer Science Research Report \#117",
  Abstract = "Abstract interpretation is a general framework for
              static program analysis. In recent years this framework
              has been used outside academia for verification of
              embedded and real-time systems. Airbus and the European
              Space Agency are examples of organisations that have
              successfully adapted this analysis framework
              for verification of critical components.
              Logic programming is a programming paradigm with a sound
              mathematical foundation. One of its characteristics is
              the separation of logic (the meaning of a program) and
              control (how it is executed); hence logic programming,
              and in particular its extension with constraints, is a
              language comparatively well suited for program analysis.
              In this thesis logic programming is used to analyse
              software developed for embedded systems. The particular
              embedded system is modeled as an emulator written as a
              constraint logic program. The emulator is specialised
              with respect to some object program in order to obtain
              a constraint logic program isomorphic to this object
              program. Applying abstract interpretation based
              analysers to the specialised emulator will provide
              analysis results that can directly be related back
              to the object program due to the isomorphism maintained
              between the object program and the specialised emulator.
              Two abstract interpretation based analysers for logic
              programs have been developed.  The first is a convex
              polyhedron analyser for constraint logic programs
              implementing a set of widening techniques for improved
              precision of the analysis.  The second analyser is a type
              analysis tool for logic programs that automatically
              derives a pre-interpretation from a regular type definition.
              Additionallly, a framework for using a restricted form of
              logic programming, namely Datalog, to express and check
              program properties is described.  At the end of the thesis
              it is shown how instrumenting the semantics of the emulator
              can be used to obtain, for instance, a fully automatic
              Worst Case Execution Time analysis by applying the convex
              polyhedron analyser to the instrumented and specialised
              emulator.  The tools developed in this thesis have all
              been made available online for demonstration."
}

@Inproceedings{HenryMM12,
  Author = "J. Henry and D. Monniaux and M. Moy",
  Title = "Succinct Representations for Abstract Interpretation",
  Booktitle = "Static Analysis:
               Proceedings of the 19th International Symposium",
  Address = "Deauville, France",
  Editor = "A. Mine and D. Schmidt",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7460,
  Year = 2012,
  Pages = "283--299",
  Abstract = "Abstract interpretation techniques can be made more
              precise by distinguishing paths inside loops, at the
              expense of possibly exponential complexity. SMT-solving
              techniques and sparse representations of paths and sets
              of paths avoid this pitfall.

              We improve previously proposed techniques for guided
              static analysis and the generation of disjunctive
              invariants by combining them with techniques for
              succinct representations of paths and symbolic
              representations for transitions based on static single
              assignment.

              Because of the non-monotonicity of the results of
              abstract interpretation with widening operators, it is
              difficult to conclude that some abstraction is more
              precise than another based on theoretical local
              precision results. We thus conducted extensive
              comparisons between our new techniques and previous
              ones, on a variety of open-source packages."
}

@Inproceedings{HoweK12,
  Author = "J. M. Howe and A. King",
  Title = "Polyhedral Analysis Using Parametric Objectives",
  Booktitle = "Static Analysis:
               Proceedings of the 19th International Symposium",
  Address = "Deauville, France",
  Editor = "A. Mine and D. Schmidt",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7460,
  Year = 2012,
  Pages = "41--57",
  Abstract = "The abstract domain of polyhedra lies at the heart of
              many program analysis techniques. However, its
              operations can be expensive, precluding their
              application to polyhedra that involve many
              variables. This paper describes a new approach to
              computing polyhedral domain operations. The core of this
              approach is an algorithm to calculate variable
              elimination (projection) based on parametric linear
              programming. The algorithm enumerates only non-redundant
              inequalities of the projection space, hence permits
              anytime approximation of the output."
}

@Inproceedings{HymansU04,
  Author = "C. Hymans and E. Upton",
  Title = "Static Analysis of Gated Data Dependence Graphs",
  Booktitle = "Static Analysis:
               Proceedings of the 11th International Symposium",
  Address = "Verona, Italy",
  Editor = "R. Giacobazzi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3148,
  Year = 2004,
  Pages = "197--211",
  Abstract = "Several authors have advocated the use of the gated data
              dependence graph as a compiler intermediate
              representation. If this representation is to gain
              acceptance, it is important to show that we may
              construct static analyses which operate directly on
              it. In this paper we present the first example of such
              an analysis, developed using the methodology of abstract
              interpretation.  The analysis is shown to be sound with
              respect to a concrete semantics for the representation.
              Experimental results are presented which indicate that
              the analysis performs well in comparison to conventional
              techniques."
}

@Article{JhalaM09,
  Author = "R. Jhala and R. Majumdar",
  Title = "Software Model Checking",
  Journal = "ACM Computing Surveys",
  Volume = 41,
  Number = 4,
  Year = 2009,
  Pages = "1--54",
  Publisher = "ACM Press",
  Address = "New York, NY, USA",
  Abstract = "We survey recent progress in software model checking."
}

@Inproceedings{Jeannet10,
  Author = "B. Jeannet",
  Title = "Some Experience on the Software Engineering of
           Abstract Interpretation Tools",
  Booktitle = "Proceedings of Tools for Automatic Program AnalysiS
               (TAPAS 2010)",
  Address = "Perpignan, France",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 267,
  Number = 2,
  Pages =  "29--42",
  Year = 2010,
  ISSN = "1571-0661",
  Abstract = "The ``right'' way of writing and structuring compilers is
              well-known. The situation is a bit less clear for static
              analysis tools. It seems to us that a static analysis
              tool is ideally decomposed into three building blocks:
              (1) a front-end, which parses programs, generates
              semantic equations, and supervises the analysis process;
              (2) a fixpoint equation solver, which takes equations
              and solves them; (3) and an abstract domain, on which
              equations are interpreted. The expected advantages of
              such a modular structure is the ability of sharing
              development efforts between analyzers for different
              languages, using common solvers and abstract
              domains. However putting in practice such ideal concepts
              is not so easy, and some static analyzers merge for
              instance the blocks (1) and (2).

              We show how we instantiated these principles with three
              different static analyzers (addressing resp. imperative
              sequential programs, imperative concurrent programs, and
              synchronous dataflow programs), a generic fixpoint
              solver (Fixpoint), and two different abstract
              domains. We discussed our experience on the advantages
              and the limits of this approach compared to related
              work."
}

@Inproceedings{JeannetM09,
  Author = "B. Jeannet and A. Min{\'e}",
  Title = "Apron: A Library of Numerical Abstract Domains for Static
           Analysis",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 21st International Conference (CAV 2009)",
  Address = "Grenoble, France",
  Editor = "A. Bouajjani and O. Maler",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5643,
  Pages = "661--667",
  Year = 2009,
  ISBN = "978-3-642-02657-7",
  Abstract = "This article describes \textsc{Apron}, a freely
              available library dedicated to the static analysis of
              the numerical variables of programs by abstract
              interpretation. Its goal is threefold: provide analysis
              implementers with ready-to-use numerical abstractions
              under a unified API, encourage the research in numerical
              abstract domains by providing a platform for integration
              and comparison, and provide teaching and demonstration
              tools to disseminate knowledge on abstract
              interpretation."
}

@Incollection {KhalilGP09,
  Author = "G. Khalil and E. Goubault and S. Putot",
  Title = "The Zonotope Abstract Domain {Taylor1+}",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 21st International Conference (CAV 2009)",
  Address = "Grenoble, France",
  Editor = "A. Bouajjani and O. Maler",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5643,
  Pages = "627--633",
  Year = 2009,
  ISBN = "978-3-642-02657-7",
  Abstract = "Static analysis by abstract interpretation [1] aims it
              automatically inferring properties on the behaviour of
              programs. We focus here on a specific kind of numerical
              invariants: the set of values taken by numerical
              variables, with a real numbers semantics, at each
              control point of a program."
}
@Incollection{KimGR07,
  Author = "D. Kim and G. Gupta and S. V. Rajopadhye",
  Title = "On Control Signals for Multi-Dimensional Time",
  Booktitle = "Languages and Compilers for Parallel Computing",
  Editor = "G. Alm{\'a}si and C. Ca\c{s}caval and P. Wu",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Year = 2007,
  Volume = 4382,
  Pages = "141--155",
  ISBN = "978-3-540-72520-6",
  Note = "Revised papers presented at the 19th International Workshop
          on Languages and Compilers for Parallel Computing (LCPC 2006),
          New Orleans, Louisiana, USA, November 2--4, 2006",
  Abstract = "Affine control loops (ACLs) comprise an important class
              of compute- and data-intensive computations. The
              theoretical framework for the automatic parallelization
              of ACLs is well established. However, the hardware
              compilation of arbitrary ACLs is still in its
              infancy. An important component for an efficient
              hardware implementation is a control mechanism that
              informs each processing element (PE) which computation
              needs to be performed and when.  We formulate this
              \emph{control signal problem} in the context of
              compiling arbitrary ACLs parallelized with a
              multi-dimensional schedule into hardware.  We
              characterize the logical time instants when PEs need a
              control signal indicating which particular computations
              need to be performed.  Finally, we present an algorithm
              to compute the minimal set of logical time instants for
              these control signals."
}

@Inproceedings{KopfE13,
  Author = "B. K{\"o}pf and A. Rybalchenko ",
  Title = "Automation of Quantitative Information-Flow Analysis",
  Booktitle = "Formal Methods for Dynamical Systems:
               13th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, {SFM} 2013",
  Address = "Bertinoro, Italy",
  Series = "Lecture Notes in Computer Science",
  Editor = "M. Bernardo and E. de Vink and A. Di Pierro and H. Wiklicky",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "7938",
  Pages =  "1--28",
  Volume = 7938,
  Year = 2013,
  Abstract = "Quantitative information-flow analysis (QIF) is an
              emerging technique for establishing
              information-theoretic confidentiality
              properties. Automation of QIF is an important step
              towards ensuring its practical applicability, since
              manual reasoning about program security has been shown
              to be a tedious and expensive task. In this chapter we
              describe a approximation and randomization techniques to
              bear on the challenge of sufficiently precise, yet
              efficient computation of quantitative information flow
              properties."
}

@Inproceedings{KruegelKMRV05,
  Author = "C. Kruegel and E. Kirda and D. Mutz and W. Robertson and G. Vigna",
  Title = "Automating Mimicry Attacks Using Static Binary Analysis",
  Booktitle = "Proceedings of Security~'05,
               the 14th USENIX Security Symposium",
  Address = "Baltimore, MD, USA",
  Year = 2005,
  Pages = "161--176",
  Abstract = "Intrusion detection systems that monitor sequences of
              system calls have recently become more sophisticated in
              defining legitimate application behavior. In particular,
              additional information, such as the value of the program
              counter and the configuration of the program's call
              stack at each system call, has been used to achieve
              better characterization of program behavior. While there
              is common agreement that this additional information
              complicates the task for the attacker, it is less clear
              to which extent an intruder is constrained.
              In this paper, we present a novel technique to evade the
              extended detection features of state-of-the-art
              intrusion detection systems and reduce the task of the
              intruder to a traditional mimicry attack. Given a
              legitimate sequence of system calls, our technique
              allows the attacker to execute each system call in the
              correct execution context by obtaining and relinquishing
              the control of the application's execution flow through
              manipulation of code pointers.
              We have developed a static analysis tool for Intel x86
              binaries that uses symbolic execution to automatically
              identify instructions that can be used to redirect
              control flow and to compute the necessary modifications
              to the environment of the process. We used our tool to
              successfully exploit three vulnerable programs and evade
              detection by existing state-of-the-art system call
              monitors. In addition, we analyzed three real-world
              applications to verify the general applicability of our
              techniques."
}

@Inproceedings{LagoonMS03,
  Author = "V. Lagoon and F. Mesnard and P. J. Stuckey",
  Title = "Termination Analysis with Types Is More Accurate",
  Booktitle = "Logic Programming: Proceedings of the
               19th International Conference (ICLP 2003)",
  Address = "Mumbai, India",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 2916,
  Year = 2003,
  Pages = "254--268",
  Abstract = "In this paper we show how we can use size and groundness
              analyses lifted to regular and (polymorphic)
              Hindley/Milner typed programs to determine more accurate
              termination of (type correct) programs. Type information
              for programs may be either inferred automatically or
              declared by the programmer. The analysis of the typed
              logic programs is able to completely reuse a framework
              for termination analysis of untyped logic programs by
              using abstract compilation of the type abstraction. We
              show that our typed termination analysis is uniformly
              more accurate than untyped termination analysis for
              regularly typed programs, and demonstrate how it is able
              to prove termination of programs which the untyped
              analysis can not."
}

@Article{LarsenLTW13,
  Author = "K. G. Larsen and A. Legay and L.-M. Traonouez and A. Wasowski",
  Title = "Robust synthesis for real-time systems",
  Journal = "Theoretical Computer Science",
  Publisher = "Elsevier",
  Volume = 515,
  Pages =  "96--122",
  Year = 2013,
  Abstract = "Specification theories for real-time systems allow
              reasoning about interfaces and their implementation
              models, using a set of operators that includes
              satisfaction, refinement, logical and parallel
              composition. To make such theories applicable throughout
              the entire design process from an abstract specification
              to an implementation, we need to reason about the
              possibility to effectively implement the theoretical
              specifications on physical systems, despite their
              limited precision. In the literature, this
              implementation problem has been linked to the robustness
              problem that analyzes the consequences of introducing
              small perturbations into formal models."
}

@Inproceedings{LavironL09,
  Author = "V. Laviron and F. Logozzo",
  Title = "SubPolyhedra: A (More) Scalable Approach to Infer Linear
           Inequalities",
  Booktitle = "Verification, Model Checking, and Abstract Interpretation:
               Proceedings of the 10th International Conference (VMCAI 2009)",
  Address = "Savannah, Georgia, USA",
  Editor = "N. D. Jones and M. M{\"u}ller-Olm",
  Pages = "229--244",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5403,
  Year = 2009,
  ISBN = "978-3-540-93899-6",
  Abstract = "We introduce Subpolyhedra (\textsf{SubPoly}) a new
              numerical abstract domain to infer and propagate linear
              inequalities. \textsf{SubPoly} is as expressive as
              Polyhedra, but it drops some of the deductive power to
              achieve scalability. \textsf{SubPoly} is based on the
              insight that the reduced product of linear equalities
              and intervals produces powerful yet scalable analyses.
              Precision can be recovered using hints. Hints can be
              automatically generated or provided by the user in the
              form of annotations.  We implemented \textsf{SubPoly} on
              the top of \texttt{Clousot}, a generic abstract
              interpreter for \texttt{.Net}. \texttt{Clousot} with
              \textsf{SubPoly} analyzes very large and complex code
              bases in few minutes. \textsf{SubPoly} can efficiently
              capture linear inequalities among hundreds of variables,
              a result well-beyond state-of-the-art implementations of
              Polyhedra."
}

@Inproceedings{LeconteB06,
  Author = "M. Leconte and B. Berstel",
  Title = "Extending a {CP} Solver with Congruences
           as Domains for Program Verification",
  Booktitle = "Proceedings of the 1st workshop on Constraints
               in Software Testing, Verification and Analysis (CSTVA '06)",
  Address = "Nantes, France",
  Editor = "B. Blanc and A. Gotlieb and C. Michel",
  Publisher = "IEEE Computer Society Press",
  Pages = "22--33",
  Year = 2006,
  Abstract = "Constraints generated for Program Verification tasks
              very often involve integer variables ranging on all the
              machine-representable integer values. Thus, if the
              propagation takes a time that is linear in the size of
              the domains, it will not reach a fix point in practical
              time.  Indeed, the propagation time needed to reduce the
              interval domains for as simple equations as $x = 2y + 1$
              and $x = 2z$ is proportional to the size of the initial
              domains of the variables. To avoid this \emph{slow
              convergence} phenomenon, we propose to enrich a
              Constraint Programming Solver (CP Solver) with
              \emph{congruence domains}. This idea has been introduced
              by [Granger, P.: Static analysis of arithmetic congruences.
              International Journal of Computer Math (1989) 165--199]
              in the abstract interpretation community and we show how
              a CP Solver can benefit from it, for example in
              discovering immediately that $12x + |y| = 3$ and
              $4z + 7y = 0$ have no integer solution.",
  Note = "Available at
          \url{http://www.irisa.fr/manifestations/2006/CSTVA06/}."
}

@Inproceedings{LimeRST09,
  Author = "D. Lime and O. H. Roux and C. Seidner and L.-M. Traonouez",
  Title = "Romeo: A Parametric Model-Checker for {Petri} Nets
           with Stopwatches",
  Booktitle = "Proceedings of the 15th International Conference
               Tools and Algorithms for the Construction and Analysis
               of Systems (TACAS 2009)",
  Address = "York, UK",
  Editor = "S. Kowalewski and A. Philippou",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5505,
  Pages = "54--57",
  Year = 2009,
  ISBN = "978-3-642-00767-5",
  Abstract = "Last time we reported on Romeo, analyses with this tool
              were mostly based on translations to other tools. This
              new version provides an integrated TCTL model-checker
              and has gained in expressivity with the addition of
              parameters. Although there exists other tools to compute
              the state-space of stopwatch models, Romeo is the first
              one that performs TCTL model-checking on stopwatch
              models. Moreover, it is the first tool that performs
              TCTL model-checking on timed parametric models. Indeed,
              Romeo now features an efficient model-checking of time
              Petri nets using the Uppaal DBM Library, the
              model-checking of stopwatch Petri nets and parametric
              stopwatch Petri nets using the Parma Polyhedra Library
              and a graphical editor and simulator of these
              models. Furthermore, its audience has increased leading
              to several industrial contracts. This paper reports on
              these recent developments of Romeo."
}

@Article{LimeMR13,
  Author = "D. Lime and C. Martinez and O. H. Roux",
  Title = "Shrinking of Time Petri nets",
  Journal = "Discrete Event Dynamic Systems",
  Publisher = "Springer-Verlag, Berlin",
  Volume = 23,
  Number = 4,
  Pages = "419--438",
  Year = 2013,
  ISSN = "0924-6703 (Print) 1573-7594 (Online)",
  Abstract = "The problem of the synthesis of time bounds enforcing
              good properties for reactive systems has been much
              studied in the literature. These works mainly rely on
              dioid algebra theory and require important restrictions
              on the structure of the model (notably by restricting to
              timed event graphs). In this paper, we address the
              problems of existence and synthesis of shrinkings of the
              bounds of the time intervals of a time Petri net, such
              that a given property is verified. We show that this
              problem is decidable for CTL properties on bounded time
              Petri nets. We then propose a symbolic algorithm based
              on the state class graph for a fragment of CTL. If the
              desired property ``include'' k-boundedness, the proposed
              algorithm terminates even if the net is unbounded. A
              prototype has been implemented in our tool Romeo and the
              method is illustrated on a small case study from the
              literature."
}

@Inproceedings{LogozzoF08,
  Author = "F. Logozzo and M. F{\"a}hndrich",
  Title = "Pentagons: A Weakly Relational Abstract Domain for the
           Efficient Validation of Array Accesses",
  Booktitle = "Proceedings of the 2008 ACM Symposium on Applied Computing
               (SAC 2008)",
  Address = "Fortaleza, Cear\'a, Brazil",
  Aditor = "R. L. Wainwright and H. Haddad",
  Year = 2008,
  Pages = "184--188",
  Publisher = "ACM Press",
  ISBN = "978-1-59593-753-7",
  Abstract = "We introduce Pentagons (\textsf{Pntg}), a weakly
              relational numerical abstract domain useful for the
              validation of array accesses in byte-code and
              intermediate languages (IL). This abstract domain
              captures properties of the form of
              $x \in [a. b] \wedge x < y$. It is more precise than the
              well known Interval domain, but it is less precise than
              the Octagon domain.  The goal of \textsf{Pntg} is to be
              a lightweight numerical domain useful for adaptive
              static analysis, where \textsf{Pntg} is used to quickly
              prove the safety of most array accesses, restricting the
              use of more precise (but also more expensive) domains to
              only a small fraction of the code.  We implemented the
              \textsf{Pntg} abstract domain in \texttt{Clousot}, a
              generic abstract interpreter for .NET assemblies. Using
              it, we were able to validate 83\% of array accesses in
              the core runtime library \texttt{mscorlib.dll} in less
              than 8 minutes."
}

@Inproceedings{MakhloufK06,
  Author = "I. B. Makhlouf and S. Kowalewski",
  Title = "An Evaluation of Two Recent Reachability Analysis Tools
           for Hybrid Systems",
  Booktitle = "Proceedings of the 2nd IFAC Conference on Analysis
               and Design of Hybrid Systems",
  Address = "Alghero, Italy",
  Editor = "C. Cassandras and A. Giua and C. Seatzu and J. Zaytoon",
  Publisher = "Elsevier Science B.V.",
  Year = 2006,
  Abstract = "The hybrid systems community is still struggling to
              provide practically applicable verification
              tools. Recently, two new tools, PHAVer and Hsolver, were
              introduced which promise to be a further step in this
              direction. We evaluate and compare both tools with the
              help of several benchmark examples. The results show
              that both have their strengths and weaknesses, and that
              there still is no all-purpose reachability analysis tool
              for hybrid systems."
}

@Inproceedings{ManevichSRF04,
  Author = "R. Manevich and M. Sagiv and G. Ramalingam and J. Field",
  Title = "Partially Disjunctive Heap Abstraction",
  Booktitle = "Static Analysis:
               Proceedings of the 11th International Symposium",
  Address = "Verona, Italy",
  Editor = "R. Giacobazzi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3148,
  Year = 2004,
  Pages = "265--279",
  Abstract = "One of the continuing challenges in abstract
              interpretation is the creation of abstractions that
              yield analyses that are both tractable and precise
              enough to prove interesting properties about real-world
              programs. One source of difficulty is the need to handle
              programs with different behaviors along different
              execution paths. Disjunctive (powerset) abstractions
              capture such distinctions in a natural way. However, in
              general, powerset abstractions increase the space and
              time by an exponential factor. Thus, powerset
              abstractions are generally perceived as being very
              costly. In this paper we partially address this
              challenge by presenting and empirically evaluating a new
              heap abstraction. The new heap abstraction works by
              merging shape descriptors according to a partial
              isomorphism similarity criteria, resulting in a
              partially disjunctive abstraction. We implemented this
              abstraction in TVLA --- a generic system for
              implementing program analyses. We conducted an empirical
              evaluation of the new abstraction and compared it with
              the powerset heap abstraction. The experiments show that
              analyses based on the partially disjunctive abstraction
              are as precise as the ones based on the fully
              disjunctive abstraction. In terms of performance,
              analyses based on the partially disjunctive abstraction
              are often superior to analyses based on the fully
              disjunctive heap abstraction. The empirical results show
              considerable speedups, up to 2 orders of magnitude,
              enabling previously non-terminating analyses, such as
              verification of the Deutsch-Schorr-Waite marking
              algorithm, to terminate with no negative effect on the
              overall precision. Indeed, experience indicates that the
              partially disjunctive shape abstraction improves
              performance across all TVLA analyses uniformly, and in
              many cases is essential for making precise shape
              analysis feasible."
}

@Techreport{McCloskeyS09TR,
  Author = "B. McCloskey and M. Sagiv",
  Title = "Combining Quantified Domains",
  Number = "EECS-2009-106",
  Year = 2009,
  Month = jul,
  Institution = "EECS Department University of California",
  Address = "Berkeley USA",
  URL = "http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-106.pdf",
  Abstract = "We develop general algorithms for reasoning about
              numerical properties of programs manipulating the heap
              via pointers. We automatically infer quantified
              invariants regarding unbounded sets of memory locations
              and unbounded numeric values. As an example, we can
              infer that for every node in a data structure, the
              node's length field is less than its capacity field. We
              can also infer per-node statements about cardinality,
              such as that each node's count field is equal to the
              number of elements reachable from it. This additional
              power allows us to prove properties about reference
              counted data structures and B-trees that were previously
              unattainable. Besides the ability to verify more
              programs, we believe that our work sheds new light on
              the interaction between heap and numerical reasoning.

              Our algorithms are parametric in the heap and the
              numeric abstractions. They permit heap and numerical
              abstractions to be combined into a single abstraction
              while maintaining correlations between these
              abstractions. In certain combinations not involving
              cardinality, we prove that our combination technique is
              complete, which is surprising in the presence of
              quantification."
}

@PhdThesis{Meijer10th,
  Author = "S. Meijer",
  Title = "Transformations for Polyhedral Process Networks",
  School = "Leiden Institute of Advanced Computer Science (LIACS),
            Faculty of Science, Leiden University",
  Address = "Leiden, The Netherlands",
  Year = 2010,
  ISBN = "978-90-9025792-1",
  Abstract = "We use the polyhedral process network (PPN) model of
              computation to program and map streaming applications
              onto embedded Multi-Processor Systems on Chip (MPSoCs)
              platforms. The PPNs, which can be automatically derived
              from sequential program applications, do not necessarily
              meet the performance/resource constraints. A designer
              can therefore apply the process splitting
              transformations to increase program performance, and the
              process merging transformation to reduce the number of
              processes in a PPN. These transformations were defined,
              but a designer had many possibilities to apply a
              particular transformation, and these transformations can
              also be ordered in many different ways. In this
              dissertation, we define compile-time solution approaches
              that assist the designer in evaluating and applying
              process splitting and merging transformations in the
              most effective way."
}

@Article{MesnardB05TPLP,
  Author = "F. Mesnard and R. Bagnara",
  Title = "{cTI}: A Constraint-Based Termination Inference Tool
           for {ISO-Prolog}",
  Journal = "Theory and Practice of Logic Programming",
  Publisher = "Cambridge University Press",
  Address = "New York",
  Volume = 5,
  Number = "1{\&}2",
  Pages = "243--257",
  Year = 2005,
  Abstract = "We present cTI, the first system for universal
              left-termination inference of logic programs.
              Termination inference generalizes termination analysis
              and checking.  Traditionally, a termination analyzer
              tries to prove that a given class of queries terminates.
              This class must be provided to the system, for instance
              by means of user annotations.  Moreover, the analysis
              must be redone every time the class of queries of
              interest is updated.  Termination inference, in
              contrast, requires neither user annotations nor
              recomputation.  In this approach, terminating classes
              for all predicates are inferred at once.  We describe
              the architecture of cTI and report an extensive
              experimental evaluation of the system covering many
              classical examples from the logic programming
              termination literature and several Prolog programs of
              respectable size and complexity."
}

@Inproceedings{MonniauxG11,
  Author = "D. Monniaux and J. {Le Guen}",
  Title = "Stratified Static Analysis Based on Variable Dependencies",
  Booktitle = "Proceedings of the Third International Workshop on
               Numerical and Symbolic Abstract Domains (NSAD 2011)",
  Address = "Venice, Italy",
  Year = 2011,
  URL = "http://arxiv.org/abs/1109.2405",
  Abstract = "In static analysis by abstract interpretation, one often
              uses \emph{widening operators} in order to enforce
              convergence within finite time to an inductive
              invariant. Certain widening operators, including the
              classical one over finite polyhedra, exhibit an
              unintuitive behavior: analyzing the program over a
              subset of its variables may lead a more precise result
              than analyzing the original program! In this article, we
              present simple workarounds for such behavior."

}

@Inproceedings{MihailaSS13,
  Author = "B. Mihaila and A. Sepp and A. Simon",
  Title = "Widening as Abstract Domain",
  Booktitle = "Proceedings of the 5th International Symposium on {NASA} Formal Methods, {NFM} 2013",
  Editor = "G. Brat and N. Rungta and A. Venet",
  Address = "Moffett Field, CA, USA",
  Pages = "170--174",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 7871,
  Year = 2013,
  Abstract = "Verification using static analysis often hinges on
              precise numeric invariants. Numeric domains of infinite
              height can infer these invariants, but require
              widening/narrowing which complicates the fixpoint
              computation and is often too imprecise. As a
              consequence, several strategies have been proposed to
              prevent a precision loss during widening or to narrow in
              a smarter way. Most of these strategies are difficult to
              retrofit into an existing analysis as they either
              require a pre-analysis, an on-the-fly modification of
              the CFG, or modifications to the fixpoint algorithm. We
              propose to encode widening and its various refinements
              from the literature as cofibered abstract domains that
              wrap standard numeric domains, thereby providing a
              modular way to add numeric analysis to any static
              analysis, that is, without modifying the fixpoint
              engine. Since these domains cannot make any assumptions
              about the structure of the program, our approach is
              suitable to the analysis of executables, where the
              (potentially irreducible) CFG is re-constructed
              on-the-fly. Moreover, our domain-based approach not only
              mirrors the precision of more intrusive approaches in
              the literature but also requires fewer iterations to
              find a fixpoint of loops than many heuristics that
              merely aim for precision."
}

@Inproceedings{MoserKK07,
  Author = "A. Moser and C. Kr{\"u}gel and E. Kirda",
  Title = "Exploring Multiple Execution Paths for Malware Analysis",
  Booktitle = "Proceedings of the 2007 IEEE Symposium on Security and Privacy
               (S{\&}P 2007)",
  Address = "Oakland, California, USA",
  Publisher = "IEEE Computer Society Press",
  Pages = "231--245",
  Year = 2007,
  Abstract = "Malicious code (or malware) is defined as software that
              fulfills the deliberately harmful intent of an
              attacker. Malware analysis is the process of determining
              the behavior and purpose of a given malware sample (such
              as a virus, worm, or Trojan horse). This process is a
              necessary step to be able to develop effective detection
              techniques and removal tools. Currently, malware
              analysis is mostly a manual process that is tedious and
              time-intensive. To mitigate this problem, a number of
              analysis tools have been proposed that automatically
              extract the behavior of an unknown program by executing
              it in a restricted environment and recording the
              operating system calls that are invoked.  The problem of
              dynamic analysis tools is that only a single program
              execution is observed. Unfortunately, however, it is
              possible that certain malicious actions are only
              triggered under specific circumstances (e.g., on a
              particular day, when a certain file is present, or when
              a certain command is received). In this paper, we
              propose a system that allows us to explore multiple
              execution paths and identify malicious actions that are
              executed only when certain conditions are met. This
              enables us to automatically extract a more complete view
              of the program under analysis and identify under which
              circumstances suspicious actions are carried out. Our
              experimental results demonstrate that many malware
              samples show different behavior depending on input read
              from the environment. Thus, by exploring multiple
              execution paths, we can obtain a more complete picture
              of their actions."
}

@Inproceedings{NavasMH09,
  Author = "J. Navas and M. M{\'e}ndez-Lojo and M. V. Hermenegildo",
  Title = "User-Definable Resource Usage Bounds Analysis for {Java} Bytecode",
  Booktitle = "Proceedings of the 4th Workshop on Bytecode Semantics,
               Verification, Analysis and Transformation (Bytecode 2009)",
  Address = "York, UK",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 253,
  Number = 5,
  Pages =  "65--82",
  Year = 2009,
  ISSN = "1571-0661",
  Abstract = "Automatic cost analysis of programs has been
              traditionally concentrated on a reduced number of
              resources such as execution steps, time, or
              memory. However, the increasing relevance of analysis
              applications such as static debugging and/or
              certification of user-level properties (including for
              mobile code) makes it interesting to develop analyses
              for resource notions that are actually
              application-dependent. This may include, for example,
              bytes sent or received by an application, number of
              files left open, number of SMSs sent or received, number
              of accesses to a database, money spent, energy
              consumption, etc. We present a fully automated analysis
              for inferring upper bounds on the usage that a Java
              bytecode program makes of a set of application
              programmer-definable resources. In our context, a
              resource is defined by programmer-provided annotations
              which state the basic consumption that certain program
              elements make of that resource. From these definitions
              our analysis derives functions which return an upper
              bound on the usage that the whole program (and
              individual blocks) make of that resource for any given
              set of input data sizes. The analysis proposed is
              independent of the particular resource. We also present
              some experimental results from a prototype
              implementation of the approach covering a significant
              set of interesting resources."
}

@Article{PanizoG12,
  Author = "L.Panizo and {M.-d.-M}. Gallardo",
  Title = "An extension of Java PathFinder for hybrid systems",
  Booktitle = "ACM SIGSOFT Software Engineering Notes",
  Volume = 37,
  Number = 6,
  Year = 2012,
  ISSN = "0163-5948",
  Pages = "1--5",
  Publisher = "ACM New York, USA",
  Abstract = "Hybrid systems are characterized by combining discrete
              and continuous behaviors. Verification of hybrid systems
              is, in general, a diffcult task due to the potential
              complexity of the continuous dynamics. Currently, there
              are different formalisms and tools which are able to
              analyze specific types of hybrid systems, model checking
              being one of the most used approaches. In this paper, we
              describe an extension of Java PathFinder in order to
              analyze hybrid systems. We apply a general methodology
              which has been successfully used to extend Spin. This
              methodology is non-intrusive, and uses external
              libraries, such as the Parma Polyhedra Library, to
              abstract the continuous behavior of the hybrid system."
}

@Inproceedings{CuervoParrinoNVM12,
  Author = "B. {Cuervo Parrino} and J. Narboux and E. Violard and N. Magaud",
  Title = "Dealing with Arithmetic Overflows in the Polyhedral Model",
  Booktitle = "Proceedings of the 2nd International Workshop
               on Polyhedral Compilation Techniques (IMPACT 2012)",
  Address = "Paris, France",
  Editor = "U. Bondhugula and V. Loechner ",
  Year = 2012,
  URL = "http://hal.inria.fr/hal-00655485",
  Abstract = "The polyhedral model provides techniques to optimize
              Static Control Programs (SCoP) using some complex
              transforma- tions which improve data-locality and which
              can exhibit parallelism. These advanced
              transformations are now available in both GCC and
              LLVM. In this paper, we focus on the cor- rectness of
              these transformations and in particular on the problem
              of integer overflows. Indeed, the strength of the
              polyhedral model is to produce an abstract mathematical
              representation of a loop nest which allows high-level
              trans- formations. But this abstract representation is
              valid only when we ignore the fact that our integers are
              only machine integers. In this paper, we present a
              method to deal with this problem of mismatch between the
              mathematical and concrete representations of loop
              nests. We assume the exis- tence of polyhedral
              optimization transformations which are proved to be
              correct in a world without overflows and we provide a
              self-verifying compilation function. Rather than
              verifying the correctness of this function, we use an
              approach based on a validator, which is a tool that is
              run by the com- piler after the transformation itself
              and which confirms that the code produced is equivalent
              to the original code. As we aim at the formal proof of
              the validator we implement this validator using the Coq
              proof assistant as a programming language [4]."

}

@Inproceedings{PayetS07,
  Author = "E. Payet and F. Spoto",
  Title = " Magic-Sets Transformation for the Analysis of {Java} Bytecode",
  Booktitle = "Static Analysis:
               Proceedings of the 14th International Symposium",
  Address = "Kongens Lyngby, Denmark",
  Editor = "G. Fil\'e and H. R. Nielson",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4634,
  ISBN = "978-3-540-74060-5",
  Pages = "452--467",
  Year = 2007,
  Abstract = "Denotational static analysis of Java bytecode has a nice
              and clean compositional definition and an efficient
              implementation with binary decision diagrams. But it
              models only the \emph{functional} i.e., input/output
              behaviour of a program $P$, not enough if one needs $P$'s
              \emph{internal} behaviours i.e., from the input to some
              internal program points. We overcome this limitation
              with a technique used up to now for logic programs
              only. It adds new \emph{magic} blocks of code to P, whose
              functional behaviours are the internal behaviours of
              $P$. We prove this transformation correct with an
              operational semantics. We define an equivalent
              denotational semantics, whose denotations for the
              magic blocks are hence the internal behaviours of
              $P$. We implement our transformation and instantiate
              it with abstract domains modelling \emph{sharing} of two
              variables and \emph{non-cyclicity} of variables. We get a
              static analyser for full Java bytecode that is
              faster and scales better than another operational
              pair-sharing analyser and a constraint-based pointer
              analyser."
}

@Inproceedings{PerezRS09,
  Author = "J. A. {Navarro P{\'e}rez} and A. Rybalchenko and A. Singh",
  Title = "Cardinality Abstraction for Declarative Networking Applications",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 21st International Conference (CAV 2009)",
  Address = "Grenoble, France",
  Editor = "A. Bouajjani and O. Maler",
  Publisher = "Springer",
  Series = "Lecture Notes in Computer Science",
  Volume = 5643,
  Pages = "584--598",
  Year = 2009,
  ISBN = "978-3-642-02657-7",
  Abstract = "Declarative Networking is a recent, viable approach to
              make distributed programming easier, which is becoming
              increasingly popular in systems and networking
              community. It offers the programmer a declarative,
              rule-based language, called P2, for writing distributed
              applications in an abstract, yet expressive way. This
              approach, however, imposes new challenges on analysis
              and verification methods when they are applied to P2
              programs. Reasoning about P2 computations is beyond the
              scope of existing tools since it requires handling of
              program states defined in terms of collections of
              relations, which store the application data, together
              with multisets of tuples, which represent communication
              events in-flight. In this paper, we propose a
              cardinality abstraction technique that can be used to
              analyze and verify P2 programs. It keeps track of the
              size of relations (together with projections thereof)
              and multisets defining P2 states, and provides an
              appropriate treatment of declarative operations, e.g.,
              indexing, unification, variable binding, and
              negation. Our cardinality abstraction-based verifier
              successfully proves critical safety properties of a P2
              implementation of the Byzantine fault tolerance protocol
              Zyzzyva, which is a representative and complex
              declarative networking application."
}

@Inproceedings{PhamTTC11,
  Author = "T.-H. Pham and M.-T. Trinh and A.-H. Truong and W.-N. Chin",
  Title = "{FixBag:} A Fixpoint Calculator for Quantified Bag Constraints",
  Booktitle = "Computer Aided Verification:
               Proceedings of the 23rd International Conference (CAV 2011)",
  Address = "Snowbird, UT, USA",
  Series = "Lecture Notes in Computer Science",
  Editor = "G. Gopalakrishnan and S. Qadeer",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-22109-5",
  Pages =  "656--662",
  Volume = 6806,
  Year = 2011,
  Abstract = "Abstract interpretation techniques have played a major
              role in advancing the state-of-the-art in program
              analysis. Traditionally, stand-alone tools for these
              techniques have been developed for the numerical domains
              which may be sufficient for lower levels of program
              correctness. To analyze a wider range of programs, we
              have developed a tool to compute symbolic fixpoints for
              quantified bag domain . This domain is useful for
              programs that deal with collections of values. Our tool
              is able to derive both loop invariants and method
              pre/post conditions via fixpoint analysis of recursive
              bag constraints. To support better precision, we have
              allowed disjunctive formulae to be inferred, where
              appropriate. As a stand-alone tool, we have tested it on
              a range of small but challenging examples with
              acceptable precision and performance."
}

@Techreport{Pop06,
  Author = "S. Pop and G.-A. Silber and A. Cohen and C. Bastoul
            and S. Girbal and N. Vasilache",
  Title = "{GRAPHITE}: Polyhedral Analyses and Optimizations for {GCC}",
  Number = "A/378/CRI",
  Institution = "Centre de Recherche en Informatique,
                 \'Ecole des Mines de Paris",
  Address = "Fontainebleau, France",
  Year = 2006,
  Note = "Contribution to the GNU Compilers Collection Developers Summit 2006
          (GCC Summit 06), Ottawa, Canada, June 28--30, 2006",
  Abstract = "We present a plan to add loop nest optimizations in GCC
              based on polyhedral representations of loop nests. We
              advocate a static analysis approach based on a hierarchy
              of interchangeable abstractions with solvers that range
              from the exact solvers such as OMEGA, to faster but less
              precise solvers based on more coarse abstractions. The
              intermediate representation GRAPHITE (GIMPLE Represented
              as Polyhedra with Interchangeable Envelopes), built on
              GIMPLE and the natural loops, hosts the high level loop
              transformations. We base this presentation on the
              WRaP-IT project developed in the Alchemy group at INRIA
              Futurs and Paris-Sud University, on the PIPS compiler
              developed at \'Ecole des mines de Paris, and on a joint
              work with several members of the static analysis and
              polyhedral compilation community in France.

              The main goal of this project is to bring more high
              level loop optimizations to GCC: loop fusion, tiling,
              strip mining, etc. Thanks to the WRaP-IT experience, we
              know that the polyhedral analyzes and transformations
              are affordable in a production compiler. A second goal
              of this project is to experiment with compile time
              reduction versus attainable precision when replacing
              operations on polyhedra with faster operations on more
              abstract domains. However, the use of a too coarse
              representation for computing might also result in an
              over approximated solution that cannot be used in
              subsequent computations. There exists a trade off
              between speed of the computation and the attainable
              precision that has not yet been analyzed for real world
              programs."
}

@Incollection{PopeeaC08,
  Author = "C. Popeea and W.-N. Chin",
  Title = "Inferring Disjunctive Postconditions",
  Booktitle = "Advances in Computer Science --- ASIAN 2006. Secure Software
               and Related Issues",
  Editor = "M. Okada and I. Satoh",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Year = 2008,
  Volume = 4435,
  Pages = "331--345",
  ISBN = "978-3-540-77504-1",
  Note = "Revised selected papers presented at the 11th Asian Computing
          Science Conference, Tokyo, Japan, December 6--8, 2006",
  Abstract = "Polyhedral analysis [9] is an abstract interpretation
              used for automatic discovery of invariant linear
              inequalities among numerical variables of a
              program. Convexity of this abstract domain allows
              efficient analysis but also loses precision via
              convex-hull and widening operators. To selectively
              recover the loss of precision, sets of polyhedra
              (disjunctive elements) may be used to capture more
              precise invariants. However a balance must be struck
              between precision and cost.
              We introduce the notion of affinity to characterize how
              closely related is a pair of polyhedra. Finding related
              elements in the polyhedron (base) domain allows the
              formulation of precise hull and widening operators
              lifted to the disjunctive (powerset extension of the)
              polyhedron domain. We have implemented a modular static
              analyzer based on the disjunctive polyhedral analysis
              where the relational domain and the proposed operators
              can progressively enhance precision at a reasonable
              cost."
}

@Article{RizkBFS09,
  Author = "A. Rizk and G. Batt and F. Fages and S. Soliman",
  Title = "A General Computational Method for Robustness Analysis
           with Applications to Synthetic Gene Networks",
  Journal = "Bioinformatics",
  Publisher = "Oxford University Press",
  Volume = 25,
  Number = "12",
  Pages = "i169--i178",
  Year = 2009,
  Note = "Paper accepted for presentation at the 2009 ISMB/ECCB Conference,
          Stockholm, Sweden, June 27--July 2, 2009.
          Available at
          \url{http://bioinformatics.oxfordjournals.org/cgi/content/abstract/25/12/i169}",
  Abstract = "\textbf{Motivation:} Robustness is the capacity of a
             system to maintain a function in the face of
             perturbations. It is essential for the correct
             functioning of natural and engineered biological
             systems. Robustness is generally defined in an \emph{ad hoc},
             problem-dependent manner, thus hampering the fruitful
             development of a theory of biological robustness,
             recently advocated by Kitano.

             \textbf{Results:} In this article, we propose a general
             definition of robustness that applies to any biological
             function expressible in temporal logic LTL (linear
             temporal logic), and to broad model classes and
             perturbation types. Moreover, we propose a computational
             approach and an implementation in BIOCHAM 2.8 for the
             automated estimation of the robustness of a given
             behavior with respect to a given set of
             perturbations. The applicability and biological relevance
             of our approach is demonstrated by testing and improving
             the robustness of the timed behavior of a synthetic
             transcriptional cascade that could be used as a
             biological timer for synthetic biology applications.

             \textbf{Availability:} Version 2.8 of BIOCHAM and the
             transcriptional cascade model are available at
             \url{http://contraintes.inria.fr/BIOCHAM/}"
}

@Article{RizkBFS11,
  Author = "A. Rizk and G. Batt and F. Fages and S. Soliman",
  Title = "Continuous Valuations of Temporal Logic Specifications with
           Applications to Parameter Optimization and Robustness
           Measures",
  Journal = "Theoretical Computer Science",
  Publisher = "Elsevier",
  Volume = 412,
  Number = 26,
  Pages =  "2827--2839",
  Year = 2011,
  ISSN = "0304-3975",
  Abstract = "Finding mathematical models satisfying a specification
              built from the formalization of biological experiments,
              is a common task of the modeler that techniques like
              model-checking help solving, in the qualitative but also
              in the quantitative case. In this article we define a
              continuous degree of satisfaction of temporal logic
              formulae with constraints. We show how such a
              satisfaction measure can be used as a fitness function
              with state-of-the-art evolutionary optimization methods
              in order to find biochemical kinetic parameter values
              satisfying a set of biological properties formalized in
              temporal logic. We also show how it can be used to
              define a measure of robustness of a biological model
              with respect to some temporal specification. These
              methods are evaluated on models of the cell cycle and of
              the MAPK signaling cascade."
}

@Inproceedings{SankaranarayananIG07,
  Author = "S. Sankaranarayanan and F. Ivancic and A. Gupta",
  Title = "Program Analysis Using Symbolic Ranges",
  Booktitle = "Static Analysis:
               Proceedings of the 14th International Symposium",
  Address = "Kongens Lyngby, Denmark",
  Editor = "G. Fil\'e and H. R. Nielson",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4634,
  ISBN = "978-3-540-74060-5",
  Pages = "366--383",
  Year = 2007,
  Abstract = "Interval analysis seeks static lower and upper bounds on
              the values of program variables. These bounds are
              useful, especially for inferring invariants to prove buffer
              overflow checks. In practice, however, intervals by
              themselves are often inadequate as invariants due to the
              lack of relational information among program variables.
              In this paper, we present a technique for deriving symbolic
              bounds on variable values. We study a restricted class of
              polyhedra whose constraints are stratified with respect to
              some variable ordering provided by the user, or chosen
              heuristically. We define a notion of normalization for
              such constraints and demonstrate polynomial time domain
              operations on the resulting domain of symbolic range
              constraints. The abstract domain is intended to complement
              widely used domains such as intervals and octagons
              for use in buffer overflow analysis. Finally, we study
              the impact of our analysis on commercial software using
              an overflow analyzer for the C language."
}

@Inproceedings{SankaranarayananSM04,
  Author = "S. Sankaranarayanan and H. B. Sipma and Z. Manna",
  Title = "Constraint-Based Linear-Relations Analysis",
  Booktitle = "Static Analysis:
               Proceedings of the 11th International Symposium",
  Address = "Verona, Italy",
  Editor = "R. Giacobazzi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3148,
  Year = 2004,
  Pages = "53--68",
  Abstract = "Linear-relations analysis of transition systems
              discovers linear invariant relationships among the
              variables of the system. These relationships help
              establish important safety and liveness
              properties. Efficient techniques for the analysis of
              systems using polyhedra have been explored, leading to
              the development of successful tools like
              HyTech. However, existing techniques rely on the use of
              approximations such as widening and extrapolation in
              order to ensure termination. In an earlier paper, we
              demonstrated the use of Farkas' Lemma to provide a
              translation from the linear-relations analysis problem
              into a system of constraints on the unknown coefficients
              of a candidate invariant. However, since the constraints
              in question are non-linear, a naive application of the
              method does not scale. In this paper, we show that by
              some efficient simplifications and approximations to the
              quantifier elimination, not only does the method scale
              to higher dimensions, but also enjoys performance
              advantages for some larger examples."
}

@Inproceedings{SankaranarayananSM05,
  Author = "S. Sankaranarayanan and H. B. Sipma and Z. Manna",
  Title = "Scalable Analysis of Linear Systems using Mathematical Programming",
  Booktitle = "Verification, Model Checking and Abstract Interpretation:
               Proceedings of the 6th International Conference (VMCAI 2005)",
  Address = "Paris, France",
  Editor = "R. Cousot",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3385,
  Year = 2005,
  Pages = "25--41",
  Abstract = "We present a method for generating linear invariants for
              large systems. The method performs forward propagation
              in an abstract domain consisting of arbitrary polyhedra
              of a predefined fixed shape. The basic operations on the
              domain like abstraction, intersection, join and
              inclusion tests are all posed as linear optimization
              queries, which can be solved efficiently by existing LP
              solvers. The number and dimensionality of the LP queries
              are polynomial in the program dimensionality, size and
              the number of target invariants. The method generalizes
              similar analyses in the interval, octagon, and octahedra
              domains, without resorting to polyhedral
              manipulations. We demonstrate the performance of our
              method on some benchmark programs."
}

@Inproceedings{SankaranarayananCSM06,
  Author = "S. Sankaranarayanan and M. Col{\'o}n
            and H. B. Sipma and Z. Manna",
  Title = "Efficient Strongly Relational Polyhedral Analysis",
  Booktitle = "Verification, Model Checking and Abstract Interpretation:
               Proceedings of the 7th International Conference (VMCAI 2006)",
  Address = "Charleston, SC, USA",
  Editor = "E. A. Emerson and K. S. Namjoshi",
  Pages = "111--125",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3855,
  Year = 2006,
  ISBN = "3-540-31139-4",
  Abstract = "Polyhedral analysis infers invariant linear equalities
              and inequalities of imperative programs. However, the
              exponential complexity of polyhedral operations such as
              image computation and convex hull limits the
              applicability of polyhedral analysis. Weakly relational
              domains such as intervals and octagons address the
              scalability issue by considering polyhedra whose
              constraints are drawn from a restricted, user-specified
              class. On the other hand, these domains rely solely on
              candidate expressions provided by the user. Therefore,
              they often fail to produce strong invariants.  We
              propose a polynomial time approach to strongly
              relational analysis. We provide efficient
              implementations of join and post condition operations,
              achieving a trade off between performance and
              accuracy. We have implemented a strongly relational
              polyhedral analyzer for a subset of the C
              language. Initial experimental results on benchmark
              examples are encouraging."
}

@Inproceedings{SankaranarayananSM06,
  Author = "S. Sankaranarayanan and H. B. Sipma and Z. Manna",
  Title = "Fixed Point Iteration for Computing the Time Elapse Operator",
  Booktitle = "Hybrid Systems: Computation and Control:
               Proceedings of the 9th International Workshop (HSCC 2006)",
  Address = "Santa Barbara, CA, USA",
  Editor = "J. Hespanha and A. Tiwari",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 3927,
  Pages = "537--551",
  Year = 2006,
  ISBN = "3-540-33170-0",
  Abstract = "We investigate techniques for automatically generating
              symbolic approximations to the time solution of a system
              of differential equations. This is an important
              primitive operation for the safety analysis of
              continuous and hybrid systems. In this paper we design a
              \emph{time elapse} operator that computes a symbolic
              over-approximation of time solutions to a continuous
              system starting from a given initial region. Our
              approach is iterative over the cone of functions (drawn
              from a suitable universe) that are non negative over the
              initial region. At each stage, we iteratively remove
              functions from the cone whose Lie derivatives do not lie
              inside the current iterate. If the iteration converges,
              the set of states defined by the final iterate is shown
              to contain all the time successors of the initial
              region. The convergence of the iteration can be forced
              using abstract interpretation operations such as
              widening and narrowing.  We instantiate our technique to
              linear hybrid systems with piecewise-affine dynamics to
              compute polyhedral approximations to the time
              successors. Using our prototype implementation TimePass,
              we demonstrate the performance of our technique on
              benchmark examples."
}

@Inproceedings{SankaranarayananISG06,
  Author = "S. Sankaranarayanan and F. Ivan\v{c}i\'{c}
            and I. Shlyakhter and A. Gupta",
  Title = "Static Analysis in Disjunctive Numerical Domains",
  Booktitle = "Static Analysis:
               Proceedings of the 13th International Symposium",
  Address = "Seoul, Korea",
  Editor = "K. Yi",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4134,
  Pages = "3--17",
  Year = 2006,
  ISBN = "3-540-37756-5",
  Abstract = "The convexity of numerical domains such as polyhedra,
              octagons, intervals and linear equalities enables
              tractable analysis of software for buffer overflows,
              null pointer dereferences and floating point
              errors. However, convexity also causes the analysis to
              fail in many common cases. Powerset extensions can
              remedy this shortcoming by considering disjunctions of
              predicates. Unfortunately, analysis using powerset
              domains can be exponentially more expensive as compared
              to analysis on the base domain. In this paper, we prove
              structural properties of fixed points computed in
              commonly used powerset extensions. We show that a fixed
              point computed on a powerset extension is also a fixed
              point in the base domain computed on an ``elaboration''
              of the program's CFG structure. Using this insight, we
              build analysis algorithms that approach path sensitive
              static analysis algorithms by performing the fixed point
              computation on the base domain while discovering an
              ``elaboration'' on the fly. Using restrictions on the
              nature of the elaborations, we design algorithms that
              scale polynomially in terms of the number of
              disjuncts. We have implemented a light-weight static
              analyzer for C programs with encouraging initial
              results."
}

@Article{SchrammelJ12,
  Author = "P. Schrammel and B. Jeannet",
  Title = "Applying Abstract Acceleration to (Co-)Reachability Analysis of Reactive Programs",
  Journal = "Journal of Symbolic Computation",
  Publisher = "Elsevier Science B.V.",
  Volume = 47,
  Number = 12,
  Year = 2012,
  Pages = "1512--1532",
  Abstract = "We propose a new technique combining dynamic and static
              analysis of programs to find linear invariants. We use a
              statistical tool, called simple component analysis, to
              analyze partial execution traces of a given program. We
              get a new coordinate system in the vector space of
              program variables, which is used to specialize numerical
              abstract domains. As an application, we instantiate our
              technique to interval analysis of simple imperative
              programs and show some experimental evaluations."
}

@Inproceedings{Simon10a,
  Author = "A. Simon",
  Title = "A Note on the Inversion Join for Polyhedral Analysis",
  Booktitle = "Proceedings of the 2nd International Workshop on
               Numerical and Symbolic Abstract Domains (NSAD 2010)",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 267,
  Pages =  "115--126",
  Year = 2010,
  ISSN = "1571-0661",
  Abstract = "Linear invariants are essential in many optimization and
              verification tasks. The domain of convex polyhedra (sets
              of linear inequalities) has the potential to infer all
              linear relationships. Yet, it is rarely applied to
              larger problems due to the join operation whose most
              precise result is given by the convex hull of two
              polyhedra which, in turn, may be of exponential
              size. Recently, Sankaranarayanan et al. proposed an
              operation called inversion join to efficiently
              approximate the convex hull. While their proposal has an
              ad-hoc flavour, we show that it is quite principled and,
              indeed, complete for planar polyhedra and, for general
              polyhedra, complete on over 70% of our benchmarks."
}

@Inproceedings{Simon10b,
  Author = "A. Simon",
  Title = "Speeding up Polyhedral Analysis by Identifying Common Constraints",
  Booktitle = "Proceedings of the 2nd International Workshop on
               Numerical and Symbolic Abstract Domains (NSAD 2010)",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 267,
  Pages =  "127--138",
  Year = 2010,
  ISSN = "1571-0661",
  Abstract = "Sets of linear inequalities are an expressive reasoning
              tool for approximating the reachable states of a
              program. However, the most precise way to join two
              states is to calculate the convex hull of the two
              polyhedra that are represented by the inequality sets,
              an operation that is exponential in the dimension of the
              polyhedra. We investigate how similarities in the two
              input polyhedra can be exploited to improve the
              performance of this costly operation. In particular, we
              discuss how common equalities and certain inequalities
              can be omitted from the calculation without affecting
              the result. We expose a maximum of common equalities and
              inequalities by converting the polyhedra into a normal
              form and give experimental evidence of the merit of our
              method."
}

@Inproceedings{SimonL10,
  Author = "A. Simon and L. Chen",
  Title = "Simple and Precise Widenings for {H-Polyhedra}",
  Booktitle = "Proceedings of the 8th Asian Symposium
               on the Programming Languages and Systems (APLAS 2010)",
  Address = "Shanghai, China",
  Series = "Lecture Notes in Computer Science",
  Editor = "K. Ueda",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-17163-5",
  Pages =  "139--155",
  Volume = 6461,
  Year = 2010,
  Abstract = "While the definition of the revised widening for
              polyhedra is defined in terms of inequalities, most
              implementations use the double description method as a
              means to an efficient implementation. We show how
              standard widening can be implemented in a simple and
              efficient way using a normalized H -representation
              (constraint-only) which has become popular in recent
              approximations to polyhedral analysis. We then detail a
              novel heuristic for this representation that is tuned
              to capture linear transformations of the state space
              while ensuring quick convergence for non-linear
              transformations for which no precise linear invariants
              exist."
}

@Techreport{SlaninaSSM07TR,
  Author = "M. Slanina and S. Sankaranarayanan and H. B. Sipma and Z. Manna",
  Title = "Controller Synthesis of Discrete Linear Plants Using Polyhedra",
  Number = "REACT-TR-2007-01",
  Institution = "Computer Science Department, Stanford University",
  Address = "Stanford, California, USA",
  Year = 2007,
  Abstract = "We study techniques for synthesizing synchronous
              controllers for affine plants with disturbances, based
              on safety specifications. Our plants are modeled in
              terms of discrete linear systems whose variables are
              partitioned into system, control, and disturbance
              variables. We synthesize non-blocking controllers that
              satisfy a user-provided safety specification by means of
              a fixed point iteration over the control precondition
              state transformer. Using convex polyhedra to represent
              sets of states, we present both precise and approximate
              algorithms for computing control preconditions and
              discuss strategies for forcing convergence of the
              iteration. We present technique for automatically
              deriving controllers from the result of the analysis,
              and demonstrate our approach on examples."
}

@TechReport{Soffia08TR,
  Author = "S. Soffia",
  Title = "Definition and Implementation of a Points-To Analysis
           for C-like Languages",
  Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy",
  Number = "arXiv:cs.PL/0810.0753",
  Year = 2008,
  Note = "Available from \url{http://arxiv.org/}",
  Abstract = "The points-to problem is the problem of determining the
              possible run-time targets of pointer variables and is
              usually considered part of the more general aliasing
              problem, which consists in establishing whether and when
              different expressions can refer to the same memory address.
              Aliasing information is essential to every tool that needs
              to reason about the semantics of programs.  However, due to
              well-known undecidability results, for all interesting
              languages that admit aliasing, the exact solution of
              nontrivial aliasing problems is not generally computable.
              This work focuses on approximated solutions to this problem
              by presenting a store-based, flow-sensitive points-to
              analysis, for applications in the field of automated software
              verification.  In contrast to software testing procedures,
              which heuristically check the program against a finite set
              of executions, the methods considered in this work are static
              analyses, where the computed results are valid for all the
              possible executions of the analyzed program.  We present a
              simplified programming language and its execution model;
              then an approximated execution model is developed using the
              ideas of abstract interpretation theory.  Finally, the
              soundness of the approximation is formally proved.  The aim
              of developing a realistic points-to analysis is pursued by
              presenting some extensions to the initial simplified model
              and discussing the correctness of their formulation.
              This work contains original contributions to the issue of
              points-to analysis, as it provides a formulation of a filter
              operation on the points-to abstract domain and a formal proof
              of the soundness of the defined abstract operations:
              these, as far as we now, are lacking from the previous
              literature."
}

@Inproceedings{Starynkevitch07,
  Author = "B. Starynkevitch",
  Title = "Multi-Stage Construction of a Global Static Analyzer",
  Booktitle = "Proceedings of the 2007 {GCC} Developers' Summit",
  Address = "Ottawa, Canada",
  Pages = "143--151",
  Year = 2007,
  Abstract = "We describe ongoing work about global static analysis
              for GCC4 within the GlobalGCC European project,
              funded thru the ITEA Programme.  The aim of this
              work is to provide global (whole program) static
              analysis, notably based upon abstract interpretation
              and knowledge based techniques, within the GCC
              compiler, targeted for analysis of medium sized C,
              Fortran or C++ programs. This will facilitate the
              adoption of GCC in the area of safetycritical
              software development, by providing features found in
              a few expensive commercial tools (PolySpace, AbsInt)
              or research prototypes (Astree). In this
              perspective, the emphasis is on the quality of
              analysis, at the expense of much bigger compilation
              times, without sacrificing scalability. Such
              analysis can be used for several purposes:
              statically compute some interesting properties of
              the program at most control points (possibly
              reporting them the user); provide clever,
              contextual, warnings about possible hazards in the
              user program (null pointer dereferences, zero
              divide, conversion loss, out of bound array access,
              \dots) while avoiding too much false alarms; enable
              additional optimisations, like conditional
              contextual constant folding, C++ method call
              devirtualization, an other contextual optimizations.
              The compiler's rich program manipulation
              infrastructure facilitates the development of these
              advanced analysis capabilities.  To facilitate the
              development high-level semantical analyses, a domain
              specific language has been developped, and is
              translated (thru C) into dynamically loaded code. It
              uses the Parma Polyhedra Library (also used in the
              GRAPHITE project) for relational analysis on scalars
              and gives more expressivity to develop analaysis
              algorithms. It permits multi-staged generation of
              the specific analysis tailored to the analyzed
              source code. Presenting this work at the 2007 GCC
              summit will allow us to stress the importance of all
              outputs of the compiler, not only object-code, and
              to expose the complementary contribution of static
              analyses and dynamic/instrumentation approaches like
              mudflap."
}

@Inproceedings{SongCR06,
  Author = "H. Song and K. J. Compton and W. C. Rounds",
  Title = "{SPHIN:} A Model Checker for Reconfigurable Hybrid Systems
           Based on {SPIN}",
  Booktitle = "Proceedings of the 5th International Workshop on
               Automated Verification of Critical Systems",
  Address = "University of Warwick, UK",
  Editor = "R. Lazic and R. Nagarajan",
  Series = "Electronic Notes in Theoretical Computer Science",
  Publisher = "Elsevier Science B.V.",
  Volume = 145,
  Pages = "167--183",
  Year = 2006,
  Abstract = "We present SPHIN, a model checker for reconfigurable
              hybrid systems based on the model checker SPIN. We
              observe that physical (analog) mobility can be modeled
              in the same way as logical (discrete) mobility is
              modeled in the $\pi$-calculus by means of channel name
              passing. We chose SPIN because it supports channel name
              passing and can model reconfigurations. We extend the
              syntax of PROMELA and the verification algorithms based
              on the expected semantics. We demonstrate the tool's
              capabilities by modeling and verifying a reconfigurable
              hybrid system."
}

@Inproceedings{TraonouezLR08,
  Author = "L.-M. Traonouez and D. Lime and O. H. Roux",
  Title = "Parametric Model-Checking of Time {Petri} Nets with Stopwatches
           Using the State-Class Graph",
  Booktitle = "Proceedings of the 6th International Conference on
               Formal Modeling and Analysis of Timed Systems (FORMATS 2008)",
  Editor = "F. Cassez and C. Jard",
  Address = "Saint Malo, France",
  Pages = "280--294",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 5215,
  Year = 2008,
  ISBN = "978-3-540-85777-8",
  Abstract = "In this paper, we propose a new framework for the
              parametric verification of time Petri nets with
              stopwatches controlled by inhibitor arcs. We first
              introduce an extension of time Petri nets with inhibitor
              arcs (ITPNs) with temporal parameters. Then, we define a
              symbolic representation of the parametric state space
              based on the classical state class graph method. The
              parameters of the model are embedded into the firing
              domains of the classes, that are represented by convex
              polyhedra. Finally, we propose semi-algorithms for the
              parametric model-checking of a subset of parametric TCTL
              formulae on ITPNs. We can thus generate the set of the
              parameter valuations that satisfy the formulae."
}

@Article{TraonouezLR09,
  Author = "L.-M. Traonouez and D. Lime and O. H. Roux",
  Title = "Parametric Model-Checking of Stopwatch Petri Nets",
  Journal = "Journal of Universal Computer Science",
  Year = 2009,
  Volume = 15,
  Number = 17,
  Pages = "3273--3304",
  Abstract = "At the border between control and verification,
              parametric verification can be used to synthesize
              constraints on the parameters to ensure that a system
              verifies given specifications. In this paper we propose
              a new framework for the parametric verification of time
              Petri nets with stopwatches. We first introduce a
              parametric extension of time Petri nets with inhibitor
              arcs (ITPNs) with temporal parameters and we define a
              symbolic representation of the parametric state-space
              based on the classical state-class graph method. Then,
              we propose semi-algorithms for the parametric
              modelchecking of a subset of parametric TCTL formulae on
              ITPNs. These results have been implemented in the tool
              Romeo and we illustrate them in a case-study based on a
              scheduling problem.", } Abstract: At the border between
              control and verification, parametric verification can be
              used to synthesize constraints on the parameters to
              ensure that a system verifies given specifications. In
              this paper we propose a new framework for the parametric
              verification of time Petri nets with stopwatches. We
              first introduce a parametric extension of time Petri
              nets with inhibitor arcs (ITPNs) with temporal
              parameters and we define a symbolic representation of
              the parametric state-space based on the classical
              state-class graph method. Then, we propose
              semi-algorithms for the parametric modelchecking of a
              subset of parametric TCTL formulae on ITPNs. These
              results have been implemented in the tool Romeo and we
              illustrate them in a case-study based on a scheduling
              problem."
}

@Inproceedings{TrifunovicCEFG+10,
  Author = "K. Trifunovic and A. Cohen and D. Edelsohn and L. Feng
           and T. Grosser and H. Jagasia and R. Ladelsky and S. Pop
           and J. Sj{\"o}din and R. Upadrasta",
  Title = "{GRAPHITE} Two Years After:
           First Lessons Learned From Real-World Polyhedral Compilation",
  Booktitle = "Proceedings of the 2nd International Workshop on
               GCC Research Opportunities (GROW'10)",
  Address = "Pisa, Italy",
  Year = 2010,
  Pages = "4--19",
  Abstract = "Modern compilers are responsible for adapting the
              semantics of source programs into a form that makes
              efficient use of a highly complex, heterogeneous
              machine. This adaptation amounts to solve an
              optimization problem in a huge and unstructured search
              space, while predicting the performance outcome of
              complex sequences of program transformations. The
              polyhedral model of compilation is aimed at these
              challenges. Its geometrical, non-inductive semantics
              enables the construction of better-structured
              optimization problems and precise analytical
              models. Recent work demonstrated the scalability of the
              main polyhedral algorithms to real-world programs. Its
              integration into production compilers is under way,
              pioneered by the graphite branch of the GNU Compiler
              Collection (GCC). Two years after the effective
              beginning of the project, this paper reports on original
              questions and innovative solutions that arose during the
              design and implementation of \textsc{graphite}."
}

@Techreport{UchoaFLPPdAA06TR,
  Author = "E. Uchoa and R. Fukasawa and J. Lysgaard and A. Pessoa
            and M. {Poggi de Arag\~ao} and D. Andrade",
  Title = "Robust Branch-Cut-and-Price for the Capacitated
           Minimum Spanning Tree Problem over a Large Extended Formulation",
  Number = "RPEP, Vol.~6, No.~9",
  Institution = "Universidade Federal Fluminense, Engenharia de Produ\c{c}ao",
  Address = "Niteroi, Brazil",
  Year = 2006,
  Abstract = "This paper presents a robust branch-cut-and-price
              algorithm for the Capacitated Minimum Spanning Tree
              Problem (CMST). The variables are associated to
              $q$-arbs, a structure that arises from a relaxation of
              the capacitated prize-collecting arborescence probem in
              order to make it solvable in pseudo-polynomial
              time. Traditional inequalities over the arc formulation,
              like Capacity Cuts, are also used. Moreover, a novel
              feature is introduced in such kind of
              algorithms. Powerful new cuts expressed over a very
              large set of variables could be added, without
              increasing the complexity of the pricing subproblem or
              the size of the LPs that are actually
              solved. Computational results on benchmark instances
              from the OR-Library show very significant improvements
              over previous algorithms. Several open instances could
              be solved to optimality."
}

@Inproceedings{UpadrastaC13,
 Author = "R. Upadrasta and A. Cohen",
 Title = "Sub-polyhedral Scheduling Using (Unit-)Two-variable-per-inequality Polyhedra",
 Booktitle = "Proceedings of the 40th Annual {ACM SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL '13}",
 Year = 2013,
 ISBN = "978-1-4503-1832-7",
 Address = "Rome, Italy",
 Pages = "483--496",
 Publisher = "ACM Press, New York, USA",
 Note = "Also published in SIGPLAN Notices, Volume 48, Number 1.",
 Abstract = "Polyhedral compilation has been successful in the design
             and implementation of complex loop nest optimizers and
             parallelizing compilers. The algorithmic complexity and
             scalability limitations remain one important weakness. We
             address it using sub-polyhedral under-aproximations of
             the systems of constraints resulting from affine
             scheduling problems. We propose a sub-polyhedral
             scheduling technique using
             (Unit-)Two-Variable-Per-Inequality or (U)TVPI
             Polyhedra. This technique relies on simple polynomial
             time algorithms to under-approximate a general polyhedron
             into (U)TVPI polyhedra. We modify the state-of-the-art
             PLuTo compiler using our scheduling technique, and show
             that for a majority of the Polybench (2.0) kernels, the
             above under-approximations yield polyhedra that are
             non-empty. Solving the under-approximated system leads to
             asymptotic gains in complexity, and shows practically
             significant improvements when compared to a traditional
             LP solver. We also verify that code generated by our
             sub-polyhedral parallelization prototype matches the
             performance of PLuTo-optimized code when the
             under-approximation preserves feasibility."
}

@Inproceedings{vanHeeOSV06,
  Author = "K. {van Hee} and O. Oanea and N. Sidorova and M. Voorhoeve",
  Title = "Verifying Generalized Soundness for Workflow Nets",
  Booktitle = "Perspectives of System Informatics: Proceedings of the
               6th International Andrei Ershov Memorial Conference",
  Address = "Akademgorodok, Novosibirsk, Russia",
  Editor = "I. Virbitskaite and A. Voronkov",
  Publisher = "Springer-Verlag, Berlin",
  Series = "Lecture Notes in Computer Science",
  Volume = 4378,
  Pages = "231--244",
  Year = 2006,
  Abstract = "We improve the decision procedure from [K. van Hee,
              N. Sidorova, and M. Voorhoeve. Generalized soundness of
              workflow nets is decidable. In Proc. of ICATPN'2004,
              volume 3099 of LNCS, pages 197--216, 2004] for the
              problem of generalized soundness for workflow nets:
              ``Every marking reachable from an initial marking with
              $k$ tokens on the initial place terminates properly,
              i.e. it can reach a marking with $k$ tokens on the final
              place, for an arbitrary natural number $k$''. Moreover,
              our new decision procedure returns a counterexample in
              case the workflow net is not generalized sound. We also
              report on experimental results obtained with the
              prototype we made and explain how the procedure can be
              used for the compositional verification of large
              workflows."
}

@PhdThesis{Vasconcelos08th,
  Author = "P. B. Vasconcelos",
  Title = "Space Cost Analysis Using Sized Types",
  School = "School of Computer Science, University of St Andrews",
  Address = "St Andrews, UK",
  Month = aug,
  Year = 2008,
  Abstract = "Programming resource-sensitive systems, such as
              real-time embedded systems, requires guaranteeing both
              the functional correctness of computations and also that
              time and space usage fit within constraints imposed
              by hardware limits or the environment.  Functional
              programming languages have proved very good at
              meeting the former logical kind of guarantees but
              not the latter resource guarantees.

              This thesis contributes to demonstrate the applicability
              of functional programming in resource-sensitive
              systems with an automatic program analysis for
              obtaining guaranteed upper bounds on dynamic space
              usage of functional programs.

              Our analysis is developed for a core subset of
              \emph{Hume}, a domain-specific functional language
              targeting resource-sensitive systems (Hammond et
              al. 2007), and presented as a type and effeect
              system that builds on previous sized type systems
              (Hughes et al. 1996, Chin and Khoo 2001) and effeect
              systems for costs (Dornic et al. 1992, Reistad and
              Gifford 1994, Hughes and Pareto 1999). It extends
              previous approaches by using abstract interpretation
              techniques to \emph{automatically} infer linear
              approximations of the sizes of recursive data types
              and the stack and heap costs of recursive functions.

              The correctness of the analysis is formally proved with
              respect to an operational semantics for the language
              and an inferrence algorithm that automatically
              reconstructs size and cost bounds is presented.

              A prototype implementation of the analysis and
              operational semantics has been constructed and used
              to experimentally assess the quality of the cost
              bounds with some examples, including implementations
              of textbook functional programming algorithms and
              simplified embedded systems."
}

@Inproceedings{Verdoolaege10,
  Author = "S. Verdoolaege",
  Title = "An Integer Set Library for the Polyhedral Model",
  Booktitle = "Proceedings of the 3rd International Congress
               on Mathematical Software (ICMS 2010)",
  Address = "Kobe, Japan",
  Series = "Lecture Notes in Computer Science",
  Editor = "K. Fukuda and J. Hoeven and M. Joswig and N. Takayama",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-15581-9",
  Pages =  "299--302",
  Volume = 6327,
  ISBN = "978-3-642-15581-9",
  Year = 2010,
  Abstract = "In compiler research, polytopes and related mathematical
              objects have been successfully used for several decades
              to represent and manipulate computer programs in an
              approach that has become known as the polyhedral
              model. The key insight is that the kernels of many
              compute-intensive applications are composed of loops
              with bounds that are affine combinations of symbolic
              constants and outer loop iterators. The iterations of a
              loop nest can then be represented as the integer points
              in a (parametric) polytope and manipulated as a whole,
              rather than as individual iterations. A similar
              reasoning holds for the elements of an array and for
              mappings between loop iterations and array elements."
}

@Incollection{Vigna07,
  Author = "G. Vigna",
  Editor = "M. Christodorescu and S. Jha and D. Maughan
            and D. Song and C. Wang",
  Booktitle = "Malware Detection",
  Title = "Static Disassembly and Code Analysis",
  Publisher = "Springer-Verlag, Berlin",
  Year = 2007,
  Series = "Advances in Information Security",
  Volume = 27,
  ISBN = "0-387-32720-4",
  Abstract = "The classification of an unknown binary program as
              malicious or benign requires two steps. In the first
              step, the stream of bytes that constitutes the program
              has to be transformed (or disassembled) into the
              corresponding sequence of machine instructions. In the
              second step, based on this machine code representation,
              static or dynamic code analysis techniques can be
              applied to determine the properties and function of the
              program.  Both the disassembly and code analysis steps
              can be foiled by techniques that obfuscate the binary
              representation of a program. Thus, robust techniques are
              required that deliver reliable results under such
              adverse circumstances. In this chapter, we introduce a
              disassemble technique that can deal with obfuscated
              binaries. Also, we introduce a static code analysis
              approach that can identify high-level semantic
              properties of code that are difficult to conceal."
}

@Inproceedings{YangWGI06,
  Author = "Z. Yang and C. Wang and A. Gupta and F. Ivan\v{c}i\'{c}",
  Title = "Mixed Symbolic Representations for Model Checking
           Software Programs",
  Booktitle = "Proceedings of the 4th ACM {\&} IEEE International Conference
               on Formal Methods and Models for Co-Design (MEMOCODE 2006)",
  Address = "Embassy Suites, Napa, California, USA",
  Pages = "17--26",
  Publisher = "IEEE Press",
  Year = 2006,
  ISBN = "1-4244-0421-5",
  Abstract = "We present an efficient symbolic search algorithm for
              software model checking. The algorithm combines multiple
              symbolic representations to efficiently represent the
              transition relation and reachable states and uses a
              combination of decision procedures for Boolean and
              integer representations. Our main contributions include:
              (1) mixed symbolic representations to model C programs
              with rich data types and complex expressions; and (2)
              new symbolic search strategies and optimization
              techniques specific to sequential programs that can
              significantly improve the scalability of model checking
              algorithms. Our controlled experiments on real-world
              software programs show that the new symbolic search
              algorithm can achieve several orders-of-magnitude
              improvements over existing methods. The proposed
              techniques are extremely competitive in handling
              sequential models of non-trivial sizes, and also compare
              favorably to popular Boolean-level model checking
              algorithms based on BDDs and SAT.",
}

@Article{YangWGI09,
  Author = "Z. Yang and C. Wang and A. Gupta and F. Ivan\v{c}i\'{c}",
  Title = "Model Checking Sequential Software Programs
           Via Mixed Symbolic Analysis",
  Journal = "ACM Transactions on Design Automation of Electronic Systems",
  Volume = 14,
  Number = 1,
  Pages = "1--26",
  Year = 2009,
  ISSN = "1084-4309",
  Publisher = "ACM Press",
  Address = "New York, NY, USA",
  Abstract = "We present an efficient symbolic search algorithm for
              software model checking. Our algorithms perform
              word-level reasoning by using a combination of decision
              procedures in Boolean and integer and real domains, and
              use novel symbolic search strategies optimized
              specifically for sequential programs to improve
              scalability. Experiments on real-world C programs show
              that the new symbolic search algorithms can achieve
              several orders-of-magnitude improvements over existing
              methods based on bit-level (Boolean) reasoning."
}

@Incollection{ZanioliC11,
  Author = "M. Zanioli and A. Cortesi",
  Title = "Information Leakage Analysis by Abstract Interpretation",
  Booktitle = "SOFTSEM 2011: Theory and Practice of Computer Science",
  Series = "Lecture Notes in Computer Science",
  Editor = "I. Cern{\'a} and T. Gyim{\'o}thy and J. Hromkovic and K. Jefferey
            and R. Kr{\'a}lovic and M. Vukolic and S. Wolf",
  Publisher = "Springer-Verlag, Berlin",
  ISBN = "978-3-642-18380-5",
  Pages =  "545--557",
  Volume = 6543,
  Year = 2011,
  Abstract = "Protecting the confidentiality of information stored in
              a computer system or transmitted over a public network
              is a relevant problem in computer security. The
              approach of information flow analysis involves
              performing a static analysis of the program with the
              aim of proving that there will not be leaks of
              sensitive information. In this paper we propose a new
              domain that combines variable dependency analysis,
              based on propositional formulas, and variables' value
              analysis, based on polyhedra. The resulting analysis is
              strictly more accurate than the state of the art
              abstract interpretation based analyses for information
              leakage detection. Its modular construction allows to
              deal with the tradeoff between efficiency and accuracy
              by tuning the granularity of the abstraction and the
              complexity of the abstract operators."
}

==============================================================================

<h2>ODC Attribution License (ODC-By)</h2>

### Preamble

The Open Data Commons Attribution License is a license agreement
intended to allow users to freely share, modify, and use this Database
subject only to the attribution requirements set out in Section 4.

Databases can contain a wide variety of types of content (images,
audiovisual material, and sounds all in the same database, for example),
and so this license only governs the rights over the Database, and not
the contents of the Database individually. Licensors may therefore wish
to use this license together with another license for the contents.

Sometimes the contents of a database, or the database itself, can be
covered by other rights not addressed here (such as private contracts,
trademark over the name, or privacy rights / data protection rights
over information in the contents), and so you are advised that you may
have to consult other documents or clear other rights before doing
activities not covered by this License.

------

The Licensor (as defined below)

and

You (as defined below)

agree as follows:

### 1.0 Definitions of Capitalised Words

"Collective Database" - Means this Database in unmodified form as part
of a collection of independent databases in themselves that together are
assembled into a collective whole. A work that constitutes a Collective
Database will not be considered a Derivative Database.

"Convey" - As a verb, means Using the Database, a Derivative Database,
or the Database as part of a Collective Database in any way that enables
a Person to make or receive copies of the Database or a Derivative
Database.  Conveying does not include interaction with a user through a
computer network, or creating and Using a Produced Work, where no
transfer of a copy of the Database or a Derivative Database occurs.

"Contents" - The contents of this Database, which includes the
information, independent works, or other material collected into the
Database. For example, the contents of the Database could be factual
data or works such as images, audiovisual material, text, or sounds.

"Database" - A collection of material (the Contents) arranged in a
systematic or methodical way and individually accessible by electronic
or other means offered under the terms of this License.

"Database Directive" - Means Directive 96/9/EC of the European
Parliament and of the Council of 11 March 1996 on the legal protection
of databases, as amended or succeeded.

"Database Right" - Means rights resulting from the Chapter III ("sui
generis") rights in the Database Directive (as amended and as transposed
by member states), which includes the Extraction and Re-utilisation of
the whole or a Substantial part of the Contents, as well as any similar
rights available in the relevant jurisdiction under Section 10.4.

"Derivative Database" - Means a database based upon the Database, and
includes any translation, adaptation, arrangement, modification, or any
other alteration of the Database or of a Substantial part of the
Contents. This includes, but is not limited to, Extracting or
Re-utilising the whole or a Substantial part of the Contents in a new
Database.

"Extraction" - Means the permanent or temporary transfer of all or a
Substantial part of the Contents to another medium by any means or in
any form.

"License" - Means this license agreement and is both a license of rights
such as copyright and Database Rights and an agreement in contract.

"Licensor" - Means the Person that offers the Database under the terms
of this License.

"Person" - Means a natural or legal person or a body of persons
corporate or incorporate.

"Produced Work" -  a work (such as an image, audiovisual material, text,
or sounds) resulting from using the whole or a Substantial part of the
Contents (via a search or other query) from this Database, a Derivative
Database, or this Database as part of a Collective Database.

"Publicly" - means to Persons other than You or under Your control by
either more than 50% ownership or by the power to direct their
activities (such as contracting with an independent consultant).

"Re-utilisation" - means any form of making available to the public all
or a Substantial part of the Contents by the distribution of copies, by
renting, by online or other forms of transmission.

"Substantial" - Means substantial in terms of quantity or quality or a
combination of both. The repeated and systematic Extraction or
Re-utilisation of insubstantial parts of the Contents may amount to the
Extraction or Re-utilisation of a Substantial part of the Contents.

"Use" - As a verb, means doing any act that is restricted by copyright
or Database Rights whether in the original medium or any other; and
includes without limitation distributing, copying, publicly performing,
publicly displaying, and preparing derivative works of the Database, as
well as modifying the Database as may be technically necessary to use it
in a different mode or format.

"You" - Means a Person exercising rights under this License who has not
previously violated the terms of this License with respect to the
Database, or who has received express permission from the Licensor to
exercise rights under this License despite a previous violation.

Words in the singular include the plural and vice versa.

### 2.0 What this License covers

2.1. Legal effect of this document. This License is:

  a. A license of applicable copyright and neighbouring rights;

  b. A license of the Database Right; and

  c. An agreement in contract between You and the Licensor.

2.2 Legal rights covered. This License covers the legal rights in the
Database, including:

  a. Copyright. Any copyright or neighbouring rights in the Database.
  The copyright licensed includes any individual elements of the
  Database, but does not cover the copyright over the Contents
  independent of this Database. See Section 2.4 for details. Copyright
  law varies between jurisdictions, but is likely to cover: the Database
  model or schema, which is the structure, arrangement, and organisation
  of the Database, and can also include the Database tables and table
  indexes; the data entry and output sheets; and the Field names of
  Contents stored in the Database;

  b. Database Rights. Database Rights only extend to the Extraction and
  Re-utilisation of the whole or a Substantial part of the Contents.
  Database Rights can apply even when there is no copyright over the
  Database. Database Rights can also apply when the Contents are removed
  from the Database and are selected and arranged in a way that would
  not infringe any applicable copyright; and

  c. Contract. This is an agreement between You and the Licensor for
  access to the Database. In return you agree to certain conditions of
  use on this access as outlined in this License.

2.3 Rights not covered.

  a. This License does not apply to computer programs used in the making
  or operation of the Database;

  b. This License does not cover any patents over the Contents or the
  Database; and

  c. This License does not cover any trademarks associated with the
  Database.

2.4 Relationship to Contents in the Database. The individual items of
the Contents contained in this Database may be covered by other rights,
including copyright, patent, data protection, privacy, or personality
rights, and this License does not cover any rights (other than Database
Rights or in contract) in individual Contents contained in the Database.
For example, if used on a Database of images (the Contents), this
License would not apply to copyright over individual images, which could
have their own separate licenses, or one single license covering all of
the rights over the images.

### 3.0 Rights granted

3.1 Subject to the terms and conditions of this License, the Licensor
grants to You a worldwide, royalty-free, non-exclusive, terminable (but
only under Section 9) license to Use the Database for the duration of
any applicable copyright and Database Rights. These rights explicitly
include commercial use, and do not exclude any field of endeavour. To
the extent possible in the relevant jurisdiction, these rights may be
exercised in all media and formats whether now known or created in the
future.

The rights granted cover, for example:

  a. Extraction and Re-utilisation of the whole or a Substantial part of
  the Contents;

  b. Creation of Derivative Databases;

  c. Creation of Collective Databases;

  d. Creation of temporary or permanent reproductions by any means and
  in any form, in whole or in part, including of any Derivative
  Databases or as a part of Collective Databases; and

  e. Distribution, communication, display, lending, making available, or
  performance to the public by any means and in any form, in whole or in
  part, including of any Derivative Database or as a part of Collective
  Databases.

3.2 Compulsory license schemes. For the avoidance of doubt:

  a. Non-waivable compulsory license schemes. In those jurisdictions in
  which the right to collect royalties through any statutory or
  compulsory licensing scheme cannot be waived, the Licensor reserves
  the exclusive right to collect such royalties for any exercise by You
  of the rights granted under this License;

  b. Waivable compulsory license schemes. In those jurisdictions in
  which the right to collect royalties through any statutory or
  compulsory licensing scheme can be waived, the Licensor waives the
  exclusive right to collect such royalties for any exercise by You of
  the rights granted under this License; and,

  c. Voluntary license schemes. The Licensor waives the right to collect
  royalties, whether individually or, in the event that the Licensor is
  a member of a collecting society that administers voluntary licensing
  schemes, via that society, from any exercise by You of the rights
  granted under this License.

3.3 The right to release the Database under different terms, or to stop
distributing or making available the Database, is reserved. Note that
this Database may be multiple-licensed, and so You may have the choice
of using alternative licenses for this Database. Subject to Section
10.4, all other rights not expressly granted by Licensor are reserved.

### 4.0 Conditions of Use

4.1 The rights granted in Section 3 above are expressly made subject to
Your complying with the following conditions of use. These are important
conditions of this License, and if You fail to follow them, You will be
in material breach of its terms.

4.2 Notices. If You Publicly Convey this Database, any Derivative
Database, or the Database as part of a Collective Database, then You
must:

  a. Do so only under the terms of this License;

  b. Include a copy of this License or its Uniform Resource Identifier (URI)
  with the Database or Derivative Database, including both in the
  Database or Derivative Database and in any relevant documentation;

  c. Keep intact any copyright or Database Right notices and notices
  that refer to this License; and

  d. If it is not possible to put the required notices in a particular
  file due to its structure, then You must include the notices in a
  location (such as a relevant directory) where users would be likely to
  look for it.

4.3 Notice for using output (Contents). Creating and Using a Produced
Work does not require the notice in Section 4.2. However, if you
Publicly Use a Produced Work, You must include a notice associated with
the Produced Work reasonably calculated to make any Person that uses,
views, accesses, interacts with, or is otherwise exposed to the Produced
Work aware that Content was obtained from the Database, Derivative
Database, or the Database as part of a Collective Database, and that it
is available under this License.

  a. Example notice. The following text will satisfy notice under
  Section 4.3:

        Contains information from DATABASE NAME which is made available
        under the ODC Attribution License.

DATABASE NAME should be replaced with the name of the Database and a
hyperlink to the location of the Database. "ODC Attribution License"
should contain a hyperlink to the URI of the text of this License. If
hyperlinks are not possible, You should include the plain text of the
required URI's with the above notice.

4.4 Licensing of others. You may not sublicense the Database. Each time
You communicate the Database, the whole or Substantial part of the
Contents, or any Derivative Database to anyone else in any way, the
Licensor offers to the recipient a license to the Database on the same
terms and conditions as this License. You are not responsible for
enforcing compliance by third parties with this License, but You may
enforce any rights that You have over a Derivative Database. You are
solely responsible for any modifications of a Derivative Database made
by You or another Person at Your direction. You may not impose any
further restrictions on the exercise of the rights granted or affirmed
under this License.

### 5.0 Moral rights

5.1 Moral rights. This section covers moral rights, including any rights
to be identified as the author of the Database or to object to treatment
that would otherwise prejudice the author's honour and reputation, or
any other derogatory treatment:

  a. For jurisdictions allowing waiver of moral rights, Licensor waives
  all moral rights that Licensor may have in the Database to the fullest
  extent possible by the law of the relevant jurisdiction under Section
  10.4;

  b. If waiver of moral rights under Section 5.1 a in the relevant
  jurisdiction is not possible, Licensor agrees not to assert any moral
  rights over the Database and waives all claims in moral rights to the
  fullest extent possible by the law of the relevant jurisdiction under
  Section 10.4; and

  c. For jurisdictions not allowing waiver or an agreement not to assert
  moral rights under Section 5.1 a and b, the author may retain their
  moral rights over certain aspects of the Database.

Please note that some jurisdictions do not allow for the waiver of moral
rights, and so moral rights may still subsist over the Database in some
jurisdictions.

### 6.0 Fair dealing, Database exceptions, and other rights not affected

6.1 This License does not affect any rights that You or anyone else may
independently have under any applicable law to make any use of this
Database, including without limitation:

  a. Exceptions to the Database Right including: Extraction of Contents
  from non-electronic Databases for private purposes, Extraction for
  purposes of illustration for teaching or scientific research, and
  Extraction or Re-utilisation for public security or an administrative
  or judicial procedure.

  b. Fair dealing, fair use, or any other legally recognised limitation
  or exception to infringement of copyright or other applicable laws.

6.2 This License does not affect any rights of lawful users to Extract
and Re-utilise insubstantial parts of the Contents, evaluated
quantitatively or qualitatively, for any purposes whatsoever, including
creating a Derivative Database (subject to other rights over the
Contents, see Section 2.4). The repeated and systematic Extraction or
Re-utilisation of insubstantial parts of the Contents may however amount
to the Extraction or Re-utilisation of a Substantial part of the
Contents.

### 7.0 Warranties and Disclaimer

7.1 The Database is licensed by the Licensor "as is" and without any
warranty of any kind, either express, implied, or arising by statute,
custom, course of dealing, or trade usage. Licensor specifically
disclaims any and all implied warranties or conditions of title,
non-infringement, accuracy or completeness, the presence or absence of
errors, fitness for a particular purpose, merchantability, or otherwise.
Some jurisdictions do not allow the exclusion of implied warranties, so
this exclusion may not apply to You.

### 8.0 Limitation of liability

8.1 Subject to any liability that may not be excluded or limited by law,
the Licensor is not liable for, and expressly excludes, all liability
for loss or damage however and whenever caused to anyone by any use
under this License, whether by You or by anyone else, and whether caused
by any fault on the part of the Licensor or not. This exclusion of
liability includes, but is not limited to, any special, incidental,
consequential, punitive, or exemplary damages such as loss of revenue,
data, anticipated profits, and lost business. This exclusion applies
even if the Licensor has been advised of the possibility of such
damages.

8.2 If liability may not be excluded by law, it is limited to actual and
direct financial loss to the extent it is caused by proved negligence on
the part of the Licensor.

### 9.0 Termination of Your rights under this License

9.1 Any breach by You of the terms and conditions of this License
automatically terminates this License with immediate effect and without
notice to You. For the avoidance of doubt, Persons who have received the
Database, the whole or a Substantial part of the Contents, Derivative
Databases, or the Database as part of a Collective Database from You
under this License will not have their licenses terminated provided
their use is in full compliance with this License or a license granted
under Section 4.8 of this License.  Sections 1, 2, 7, 8, 9 and 10 will
survive any termination of this License.

9.2 If You are not in breach of the terms of this License, the Licensor
will not terminate Your rights under it.

9.3 Unless terminated under Section 9.1, this License is granted to You
for the duration of applicable rights in the Database.

9.4 Reinstatement of rights. If you cease any breach of the terms and
conditions of this License, then your full rights under this License
will be reinstated:

  a. Provisionally and subject to permanent termination until the 60th
  day after cessation of breach;

  b. Permanently on the 60th day after cessation of breach unless
  otherwise reasonably notified by the Licensor; or

  c.  Permanently if reasonably notified by the Licensor of the
  violation, this is the first time You have received notice of
  violation of this License from  the Licensor, and You cure the
  violation prior to 30 days after your receipt of the notice.

9.5 Notwithstanding the above, Licensor reserves the right to release
the Database under different license terms or to stop distributing or
making available the Database. Releasing the Database under different
license terms or stopping the distribution of the Database will not
withdraw this License (or any other license that has been, or is
required to be, granted under the terms of this License), and this
License will continue in full force and effect unless terminated as
stated above.

### 10.0 General

10.1 If any provision of this License is held to be invalid or
unenforceable, that must not affect the validity or enforceability of
the remainder of the terms and conditions of this License and each
remaining provision of this License shall be valid and enforced to the
fullest extent permitted by law.

10.2 This License is the entire agreement between the parties with
respect to the rights granted here over the Database. It replaces any
earlier understandings, agreements or representations with respect to
the Database.

10.3 If You are in breach of the terms of this License, You will not be
entitled to rely on the terms of this License or to complain of any
breach by the Licensor.

10.4 Choice of law. This License takes effect in and will be governed by
the laws of the relevant jurisdiction in which the License terms are
sought to be enforced. If the standard suite of rights granted under
applicable copyright law and Database Rights in the relevant
jurisdiction includes additional rights not granted under this License,
these additional rights are granted in this License in order to meet the
terms of this License.