Module: ppl/ppl
Branch: master
Commit: 8111848b5253df59ff180c8f50f0f68d1847d686
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8111848b5253…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 09:25:09 2013 +0100
Fixed more book titles.
---
doc/ppl_citations.bib | 20 ++++++++++++--------
1 files changed, 12 insertions(+), 8 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 8e3f722..1b2c218 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -528,7 +528,8 @@ Summarizing:
@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)",
+ 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",
@@ -1042,8 +1043,8 @@ Summarizing:
@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}",
+ Booktitle = "Automated Technology for Verification and Analysis:
+ Proceedings of the 11th International Symposium (ATVA 2013)",
Address = "Hanoi, Vietnam",
Editor = "Dang Van Hung",
Year = 2013,
@@ -1144,8 +1145,9 @@ Summarizing:
@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",
+ 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",
@@ -1278,8 +1280,10 @@ Summarizing:
@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",
+ 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,
@@ -1726,7 +1730,7 @@ Summarizing:
Month = jul,
Year = 2005,
Note = "In German",
- Abstract = "{Diese Arbeit beschreibt eine intra- und auch
+ 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
Module: ppl/ppl
Branch: master
Commit: 42bfafc4ea27bc05ab5e2fc26df980786589a848
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=42bfafc4ea27…
Author: Patricia Hill <patricia.hill(a)bugseng.com>
Date: Sat Dec 28 08:07:21 2013 +0000
More references added.
---
doc/ppl_citations.bib | 95 +++++++++++++++++++++++++++++++++++++++++++++++++
1 files changed, 95 insertions(+), 0 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index f00982c..f8a7461 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -376,6 +376,7 @@ Summarizing:
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,
@@ -494,6 +495,7 @@ 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",
@@ -2070,6 +2072,41 @@ Summarizing:
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",
@@ -3379,6 +3416,44 @@ Summarizing:
}
+@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",
@@ -3992,6 +4067,26 @@ Summarizing:
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",
Module: ppl/ppl
Branch: master
Commit: f9ccf58636a2ff7f1f8b911b4acf51ed93eb492d
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f9ccf58636a2…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 09:01:10 2013 +0100
Removed duplicate entry.
---
doc/ppl_citations.bib | 31 -------------------------------
1 files changed, 0 insertions(+), 31 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 9782924..f00982c 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -824,37 +824,6 @@ Summarizing:
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",
Module: ppl/ppl
Branch: master
Commit: 375dc91eab14dd1c7cd50c351fd3d3852e21c758
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=375dc91eab14…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 09:00:50 2013 +0100
Book title fixed.
---
doc/ppl_citations.bib | 7 ++++---
1 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 2b3f807..9782924 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -797,14 +797,15 @@ Summarizing:
@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",
+ 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",
+ 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
Module: ppl/ppl
Branch: master
Commit: 0aa1d092fc001b1aa6accad3a78d8fd7c81377e8
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0aa1d092fc00…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 08:58:20 2013 +0100
Title fixed and abstract added.
---
doc/ppl_citations.bib | 26 +++++++++++++++++++++++++-
1 files changed, 25 insertions(+), 1 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index d25ae10..2b3f807 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -581,11 +581,35 @@ Summarizing:
@Book{AndreS13,
Author = "{\'E}. Andr{\'e} and R. Soulat",
- Title = "The Inverse Method: Parametric Verification of Real-time Unbedded Systems",
+ 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,
Module: ppl/ppl
Branch: master
Commit: e4c47c3d6ded048c8fb8bc477beb5fa18ef50088
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4c47c3d6ded…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 08:55:17 2013 +0100
Fixed more book titles.
---
doc/ppl_citations.bib | 28 ++++++++++++++++------------
1 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 834ea42..d25ae10 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -526,7 +526,7 @@ Summarizing:
@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}",
+ 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",
@@ -555,7 +555,8 @@ Summarizing:
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",
+ Booktitle = "Computer Aided Verification:
+ Proceedings of the 25th International Conference (CAV 2013)",
Year = 2013,
Pages = "984--989",
Editor = "N. Sharygina and H. Veith",
@@ -1189,7 +1190,8 @@ Summarizing:
@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",
+ Booktitle = "Computer Aided Verification:
+ Proceedings of the 25th International Conference (CAV 2013)",
Year = 2013,
Pages = "511-526",
Editor = "N. Sharygina and H. Veith",
@@ -2849,11 +2851,11 @@ Summarizing:
Author = "B. Jeannet and A. Min{\'e}",
Title = "Apron: A Library of Numerical Abstract Domains for Static
Analysis",
- Booktitle = "Computer Aided Verification,
+ Booktitle = "Computer Aided Verification:
Proceedings of the 21st International Conference (CAV 2009)",
Address = "Grenoble, France",
Editor = "A. Bouajjani and O. Maler",
- Publisher = "Springer",
+ Publisher = "Springer-Verlag, Berlin",
Series = "Lecture Notes in Computer Science",
Volume = 5643,
Pages = "661--667",
@@ -2874,14 +2876,16 @@ Summarizing:
@Incollection {KhalilGP09,
Author = "G. Khalil and E. Goubault and S. Putot",
Title = "The Zonotope Abstract Domain {Taylor1+}",
- Booktitle = "Computer Aided Verification",
- Series = "Lecture Notes in Computer Science",
+ 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",
- ISBN = "978-3-642-02657-7",
- Pages = "627--633",
+ 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
@@ -3566,7 +3570,7 @@ Summarizing:
@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,
+ Booktitle = "Computer Aided Verification:
Proceedings of the 21st International Conference (CAV 2009)",
Address = "Grenoble, France",
Editor = "A. Bouajjani and O. Maler",
@@ -3606,8 +3610,8 @@ Summarizing:
@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 = "Proceedings of the 23rd International Conference on
- Computer Aided Verification (CAV 2011)",
+ 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",
Module: ppl/ppl
Branch: master
Commit: f6149a7984b927ae3941871a5efd3d115b5b314a
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6149a7984b9…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 08:47:59 2013 +0100
Book title fixed.
---
doc/ppl_citations.bib | 3 ++-
1 files changed, 2 insertions(+), 1 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 7543961..834ea42 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -497,7 +497,8 @@ Summarizing:
@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",
+ 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",
Module: ppl/ppl
Branch: master
Commit: cdb6ec47f9cb79e3b3d8af4aee9b8c4c97195e5e
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cdb6ec47f9cb…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 08:43:25 2013 +0100
Fixed several typos.
---
doc/ppl_citations.bib | 22 ++++++++++++----------
1 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index d6f4673..7543961 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -190,18 +190,18 @@ Summarizing:
}
@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,
+ 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 finding tight bounds for the cost of each of its
+ 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
@@ -258,8 +258,10 @@ Summarizing:
@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)",
+ 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",
@@ -346,7 +348,7 @@ Summarizing:
demo model from Mathworks."
}
-@Inproceedings {AmatoPS10,
+@Inproceedings{AmatoPS10,
Author = "G. Amato and M. Parton and F. Scozzari",
Title = "A Tool Which Mines Partial Execution Traces to Improve
Static Analysis",
