Added recently published papers citing the PPL.

Added papers are books, journal articles or conference proceedings
published in 2012-2013 that cite "The Parma Polyhedra Library: Toward
a complete set of numerical abstractions for the analysis and
verification of hardware and software systems."

Theses, workshop papers and technical reports have not been added in
this commit.

1 files changed, 764 insertions, 2 deletions

diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 9b11cbe07..793cc8272 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -166,6 +166,58 @@ Summarizing:
               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 (TOCL)",
+  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 finding 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}",
@@ -204,6 +256,39 @@ Summarizing:
               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",
@@ -331,6 +416,29 @@ Summarizing:
               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}:
@@ -384,6 +492,97 @@ Summarizing:
               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 = "Proceedings of the 4th International Symposium on {NASA} Formal Methods, {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 = "Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis, {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 = "Proceedings of Computer Aided Verification - 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 Unbedded Systems",
+  Publisher = "John Wiley and Sons.",
+  Series = "{FOCUS Series}",
+  ISBN = "9781118569405",
+  Year = 2013,
+}
 
 @Inproceedings{ArmandoBM07,
   Author = "A. Armando and M. Benerecetti and J. Mantovani",
@@ -568,6 +767,65 @@ Summarizing:
               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 = "{POPL '13} Proceedings of the 40th Annual {ACM SIGPLAN-SIGACT} Symposium on Principles of Programming Languages",
+ 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."
+}
+
+@Article{benerecettiFM13,
+  Author= "M. Benerecetti and M. Faella and S. Minopoli",
+  Title = "Automatic synthesis of switching controllers for linear hybrid systems: Safety control",
+  Journal = "Theoretical Computer Science",
+  Year = 2013,
+  Volume = 493,
+  Pages = "116--138",
+  DOI = "10.1016/j.tcs.2012.10.042",
+  Publisher="Elsevier Science B.V.",
+  Abstract = "In this paper we study the problem of automatically
+              generating switching con- trollers for the class of
+              Linear Hybrid Automata, with respect to safety
+              objectives. While the same problem has been already
+              considered in the literature, no sound and complete
+              solution has been provided so far. We identify and solve
+              inaccuracies contained in previous characterizations of
+              the problem, providing a sound and complete symbolic
+              xpoint procedure to compute the set of states from which
+              a controller can keep the system in a given set of
+              desired states.  While the overall procedure may not
+              terminate, we prove the termination of each iteration,
+              thus paving the way to an effective implementation.  The
+              techniques needed to effectively and efficiently
+              implement the proposed solution procedure, based on
+              polyhedral abstractions of the state space, are
+              thoroughly illustrated and discussed. Finally, some
+              supporting and promising experimental results, based on
+              the implementation of the proposed techniques on top of
+              the tool PHAVer, are presented."
+}
+
 @Inproceedings{BerendsenJV10,
   Author = "J. Berendsen and D. N. Jansen and F. W. Vaandrager",
   Title = "Fortuna: Model Checking Priced Probabilistic Timed Automata",
@@ -781,6 +1039,35 @@ Summarizing:
               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,
+               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",
@@ -855,6 +1142,78 @@ Summarizing:
               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 = "{ICPE '13} Proceedings of the 4th {ACM/SPEC} International Conference on Performance Engineering",
+ 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 = "Proceedings of Computer Aided Verification - 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",
@@ -916,6 +1275,34 @@ Summarizing:
               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 = "Proceedings of the 10th International Conference on Quantitative Evaluation of Systems, {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",
@@ -987,6 +1374,32 @@ Summarizing:
               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,
+  ISBN = "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
@@ -1231,6 +1644,78 @@ Summarizing:
               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}",
@@ -1263,7 +1748,34 @@ Summarizing:
               der linearen Algebra die affinen Beziehungen, welche
               zwischen den Programmvariablen an einem bestimmten
               Programmpunkt gelten, erkennen. Die Behandlung von
-              Prozeduraufrufen steht dabei im Vordergrund.}"
+              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,
@@ -1507,6 +2019,59 @@ Summarizing:
               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 = "{VMCAI} - 15th International Conference on Verification, Model Checking, and Abstract Interpretation - 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."
+}
+
 @PhdThesis{Gobert07th,
   Author = "F. Gobert",
   Title = "Towards putting abstract interpretation of {Prolog} into practice:
@@ -2139,6 +2704,65 @@ Summarizing:
               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",
@@ -2295,6 +2919,32 @@ Summarizing:
               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",
@@ -2361,6 +3011,29 @@ Summarizing:
               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
@@ -2461,6 +3134,35 @@ Summarizing:
               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
@@ -2759,6 +3461,31 @@ Summarizing:
               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",
@@ -3617,6 +4344,41 @@ Summarizing:
               over previous algorithms. Several open instances could
               be solved to optimality."
 }
+[download]
+
+@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",
@@ -3843,7 +4605,7 @@ Summarizing:
 ==============================================================================
 
 <h2>ODC Attribution License (ODC-By)</h2>
-
+and,
 ### Preamble
 
 The Open Data Commons Attribution License is a license agreement