[PPL-devel] [GIT] ppl/ppl(master): Abstracts fixed. Avoided non-ASCII characters.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: 3ccd08df85d78ef507fd2a359251a009559fe110
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3ccd08df85d78ef507fd2a359251a009559fe110

Author: Roberto Bagnara <roberto.bagnara at bugseng.com>
Date:   Sun Dec 29 11:01:13 2013 +0100

Abstracts fixed.  Avoided non-ASCII characters.

---

 doc/ppl_citations.bib |   18 +++++++++---------
 1 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 9ef85bc..32e3a39 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -618,14 +618,14 @@ Summarizing:
               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
+              specified 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
+              models. Experiments show its efficiency and
               applicability."
 }
 
@@ -1178,7 +1178,7 @@ Summarizing:
               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
+              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
@@ -1401,7 +1401,7 @@ Summarizing:
   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",
+  Editor = "K. Joshi and M. Siegle and M. Stoelinga and P. R. D'Argenio",
   Year = 2013,
   Pages = "322--337",
   Publisher = "Springer-Verlag, Berlin",
@@ -3202,8 +3202,8 @@ Summarizing:
   Abstract = "Geometric heuristics for the quantifier elimination
               approach presented by Kapur (2004) are investigated to
               automatically derive loop invariants expressing weakly
-              relational numerical properties (such as $l \leq x \leq h$ or
-              $l \leq  \pm x \pm y \leq h)$ for imperative programs.
+              relational numerical properties (such as $l \leq x \leq h$ or
+              $l \leq \pm x \pm y \leq h)$ for imperative programs.
               Such properties
               have been successfully used to analyze commercial
               software consisting of hundreds of thousands of lines of
@@ -3217,7 +3217,7 @@ Summarizing:
               approach has been generalized to consider disjunctive
               invariants of the similar form, expressed using maximum
               function (such as
-              $\max(x + a, y + b, z + c, d) \leq \max (x + e, y + f, z + g, h)$),
+              $\max(x+a, y+b, z+c, d) \leq \max (x+e, y+f, z+g, h)$),
               thus enabling automatic generation of a subclass of
               disjunctive invariants for imperative programs as well."
 }
@@ -3472,7 +3472,7 @@ Summarizing:
   Year = 2013,
   ISBN = "978-3-319-02443-1 (Print) 978-3-319-02444-8 (Online)",
   Abstract = "PyEcdar is an open source implementation for reasoning
-              on timed systems. PyEcdar’s main objective is not
+              on timed systems. PyEcdar's main objective is not
               efficiency, but rather flexibility to test and implement
               new results on timed systems"
 }
@@ -4566,7 +4566,7 @@ Summarizing:
               verification can be regarded as geometric concepts in
               machine learning. Safety properties define bad states:
               states a program should not reach. Program verification
-              explains why a program’s set of reachable states is
+              explains why a program's set of reachable states is
               disjoint from the set of bad states. In Hoare Logic,
               these explanations are predicates that form inductive
               assertions. Using samples for reachable and bad states