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

Author: Roberto Bagnara roberto.bagnara@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