Module: ppl/ppl
Branch: master
Commit: fdcab35567fd8b9031b4dff2e968476485f74ebd
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdcab35567fd…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sun Dec 29 10:12:27 2013 +0100
Fixed KapurZHZLN13.
---
doc/ppl_citations.bib | 25 ++++++++++++++-----------
1 files changed, 14 insertions(+), 11 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 1df5397..1c0c7fa 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -3183,8 +3183,10 @@ Summarizing:
}
@InCollection{KapurZHZLN13,
- Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen",
- Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants",
+ Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu
+ and T. Nguyen",
+ Title = "Geometric Quantifier Elimination Heuristics
+ for Automatically Generating Octagonal and Max-plus Invariants",
Booktitle = "Automated Reasoning and Mathematics:
Essays in Memory of William W. McCune",
Editor = "M. P. Bonacina and M. E. Stickel",
@@ -3197,26 +3199,27 @@ 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 =< x =< h or
- l =< +/- x +/- y =< h) for imperative programs. Such properties
+ 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
code (using for example, the Astr\'ee tool based on
abstract interpretation framework proposed by Cousot and
his group). The main attraction of the proposed approach
is its much lower complexity in contrast to the abstract
- interpretation approach (O(n^2) in contrast to O(n^4),
- where n is the number of variables) with the ability to
+ interpretation approach ($O(n^2)$ in contrast to $O(n^4)$,
+ where $n$ is the number of variables) with the ability to
still generate invariants of comparable strength. This
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) ≤ max
- (x + e,y + f,z + g,h)), thus enabling automatic
- generation of a subclass of disjunctive invariants for
- imperative programs as well."
+ function (such as
+ $\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."
}
-@Incollection {KhalilGP09,
+@Incollection{KhalilGP09,
Author = "G. Khalil and E. Goubault and S. Putot",
Title = "The Zonotope Abstract Domain {Taylor1+}",
Booktitle = "Computer Aided Verification:
Module: ppl/ppl
Branch: master
Commit: 22e8ceb3a871bcc8dff3c7fabd14e611ece9598a
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=22e8ceb3a871…
Author: Patricia Hill <patricia.hill(a)bugseng.com>
Date: Sat Dec 28 18:13:44 2013 +0000
More references added.
---
doc/ppl.bib | 34 --------------
doc/ppl_citations.bib | 115 +++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 115 insertions(+), 34 deletions(-)
diff --git a/doc/ppl.bib b/doc/ppl.bib
index bc5a897..cbb16bb 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -1967,40 +1967,6 @@ Summarizing:
Year = 1994,
}
-@InCollection{KapurZHZLN13,
- Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen",
- Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants",
- Booktitle = "Automated Reasoning and Mathematics:
- Essays in Memory of William W. McCune",
- Editor = "M. P. Bonacina and M. E. Stickel",
- Publisher = "Springer-Verlag, Berlin",
- Series = "Lecture Notes in Computer Science",
- Volume = 7788,
- Pages = "189--228",
- Year = 2013,
- ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)"
- 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 =< x =< h or
- l =< +/- x +/- y =< h) for imperative programs. Such properties
- have been successfully used to analyze commercial
- software consisting of hundreds of thousands of lines of
- code (using for example, the Astr\'ee tool based on
- abstract interpretation framework proposed by Cousot and
- his group). The main attraction of the proposed approach
- is its much lower complexity in contrast to the abstract
- interpretation approach (O(n^2) in contrast to O(n^4),
- where n is the number of variables) with the ability to
- still generate invariants of comparable strength. This
- 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) ≤ max
- (x + e,y + f,z + g,h)), thus enabling automatic
- generation of a subclass of disjunctive invariants for
- imperative programs as well."
-}
-
@Article{KhachiyanBBEG06,
Author = "L. Khachiyan and E. Boros and K. Borys
and K. Elbassioni and V. Gurvich",
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index e6e4f6f..e412fb8 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -1043,6 +1043,45 @@ Summarizing:
number of test cases."
}
+@InProceedings{BozgaIK12,
+ Author = "M. Bozga and R. Iosif and F. Kone\vcn\'y",
+ Title = "Deciding Conditional Termination",
+ Booktitle = "Tools and Algorithms for the Construction and Analysis
+ of Systems:
+ 18th International Conference, {TACAS} 2012",
+ Address = "Tallinn, Estonia",
+ Editor = "C. Flanagan and B. K{\"o}nig",
+ Publisher = "Springer-Verlag, Berlin",
+ Series = "Lecture Notes in Computer Science",
+ Volume = 7214,
+ ISBN = "978-3-642-28755-8 (Print) 978-3-642-28756-5 (Online)",
+ Pages = "252--266",
+ Year = 2012,
+ Abstract = "This paper addresses the problem of conditional
+ termination, which is that of defining the set of
+ initial configurations from which a given program
+ terminates. First we define the dual set, of initial
+ configurations, from which a non-terminating execution
+ exists, as the greatest fixpoint of the pre-image of the
+ transition relation. This definition enables the
+ representation of this set, whenever the closed form of
+ the relation of the loop is definable in a logic that
+ has quantifier elimination. This entails the
+ decidability of the termination problem for such
+ loops. Second, we present effective ways to compute the
+ weakest precondition for non-termination for difference
+ bounds and octagonal (non-deterministic) relations, by
+ avoiding complex quantifier eliminations. We also
+ investigate the existence of linear ranking functions
+ for such loops. Finally, we study the class of linear
+ affine relations and give a method of
+ under-approximating the termination precondition for a
+ non-trivial subclass of affine relations. We have
+ performed preliminary experiments on transition systems
+ modeling real-life systems, and have obtained
+ encouraging results."
+}
+
@Inproceedings{BramanM08,
Title = "Safety Verification of Fault Tolerant Goal-based Control Programs
with Estimation Uncertainty",
@@ -3090,6 +3129,40 @@ Summarizing:
interpretation."
}
+@InCollection{KapurZHZLN13,
+ Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen",
+ Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants",
+ Booktitle = "Automated Reasoning and Mathematics:
+ Essays in Memory of William W. McCune",
+ Editor = "M. P. Bonacina and M. E. Stickel",
+ Publisher = "Springer-Verlag, Berlin",
+ Series = "Lecture Notes in Computer Science",
+ Volume = 7788,
+ Pages = "189--228",
+ Year = 2013,
+ ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)",
+ 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 =< x =< h or
+ l =< +/- x +/- y =< h) for imperative programs. Such properties
+ have been successfully used to analyze commercial
+ software consisting of hundreds of thousands of lines of
+ code (using for example, the Astr\'ee tool based on
+ abstract interpretation framework proposed by Cousot and
+ his group). The main attraction of the proposed approach
+ is its much lower complexity in contrast to the abstract
+ interpretation approach (O(n^2) in contrast to O(n^4),
+ where n is the number of variables) with the ability to
+ still generate invariants of comparable strength. This
+ 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) ≤ max
+ (x + e,y + f,z + g,h)), thus enabling automatic
+ generation of a subclass of disjunctive invariants for
+ imperative programs as well."
+}
+
@Incollection {KhalilGP09,
Author = "G. Khalil and E. Goubault and S. Putot",
Title = "The Zonotope Abstract Domain {Taylor1+}",
@@ -3604,6 +3677,28 @@ Summarizing:
}
+@Article{MonniauxG12,
+ Author = "D. Monniaux and J. {Le Guen}",
+ Title = "Stratified Static Analysis Based on Variable Dependencies",
+ Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})",
+ Publisher = "Elsevier Science Publishers B. V.",
+ Address = "Amsterdam, The Netherlands",
+ Volume = 288,
+ Pages = "61--74",
+ Year = 2012,
+ ISSN = "1571-0661",
+ Abstract = "In static analysis by abstract interpretation, one often
+ uses 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{MihailaSS13b,
Author = "B. Mihaila and A. Sepp and A. Simon",
Title = "Widening as Abstract Domain",
@@ -4026,6 +4121,26 @@ Summarizing:
cost."
}
+@article{LuMMRFL12,
+ Author = "Q. Lu and M. Madsen and M. Milata and S. Ravn and U. Fahrenberg and K. G. Larsen",
+ Title = "Reachability analysis for timed automata using max-plus algebra",
+ ISSN = "1567-8326",
+ Journal = "Journal of Logic and Algebraic Programming",
+ Volume = 81,
+ Number = 3,
+ Year = 2012,
+ Abstract = "We show that max-plus polyhedra are usable as a data
+ structure in reachability analysis of timed
+ automata. Drawing inspiration from the extensive work
+ that has been done on difference bound matrices, as well
+ as previous work on max-plus polyhedra in other areas, we
+ develop the algorithms needed to perform forward and
+ backward reachability analysis using max-plus
+ polyhedra. To show that the approach works in practice
+ and theory alike, we have created a proof-of-concept
+ implementation on top of the model checker opaal."
+}
+
@Article{RizkBFS09,
Author = "A. Rizk and G. Batt and F. Fages and S. Soliman",
Title = "A General Computational Method for Robustness Analysis
Module: ppl/ppl
Branch: master
Commit: 2f1203b99f97684a6c7b52747fe785595b421940
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f1203b99f97…
Author: Patricia Hill <patricia.hill(a)bugseng.com>
Date: Sat Dec 28 13:00:59 2013 +0000
More references added.
---
doc/ppl.bib | 34 +++++++++++++++++++++++++++++
doc/ppl_citations.bib | 57 +++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 91 insertions(+), 0 deletions(-)
diff --git a/doc/ppl.bib b/doc/ppl.bib
index cbb16bb..bc5a897 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -1967,6 +1967,40 @@ Summarizing:
Year = 1994,
}
+@InCollection{KapurZHZLN13,
+ Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen",
+ Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants",
+ Booktitle = "Automated Reasoning and Mathematics:
+ Essays in Memory of William W. McCune",
+ Editor = "M. P. Bonacina and M. E. Stickel",
+ Publisher = "Springer-Verlag, Berlin",
+ Series = "Lecture Notes in Computer Science",
+ Volume = 7788,
+ Pages = "189--228",
+ Year = 2013,
+ ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)"
+ 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 =< x =< h or
+ l =< +/- x +/- y =< h) for imperative programs. Such properties
+ have been successfully used to analyze commercial
+ software consisting of hundreds of thousands of lines of
+ code (using for example, the Astr\'ee tool based on
+ abstract interpretation framework proposed by Cousot and
+ his group). The main attraction of the proposed approach
+ is its much lower complexity in contrast to the abstract
+ interpretation approach (O(n^2) in contrast to O(n^4),
+ where n is the number of variables) with the ability to
+ still generate invariants of comparable strength. This
+ 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) ≤ max
+ (x + e,y + f,z + g,h)), thus enabling automatic
+ generation of a subclass of disjunctive invariants for
+ imperative programs as well."
+}
+
@Article{KhachiyanBBEG06,
Author = "L. Khachiyan and E. Boros and K. Borys
and K. Elbassioni and V. Gurvich",
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index cdbf314..e6e4f6f 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -1087,6 +1087,33 @@ Summarizing:
hypersurfaces) are computed."
}
+@Article{BrauerKK13,
+ Author = "J. Brauer and A King. and S. Kowalewski",
+ Title = "Abstract interpretation of microcontroller code: Intervals meet congruences",
+ Journal = "Science of Computer Programming",
+ Volume = 78,
+ Number = "7",
+ Pages = "862--883",
+ Year = 2006,
+ Publisher = "Elsevier North-Holland, Inc.",
+ Address = "Amsterdam, The Netherlands",
+ ISSN = "0167-6423",
+ Abstract = "Bitwise instructions, loops and indirect data access
+ present challenges to the verification of
+ microcontroller programs. In particular, since registers
+ are often memory mapped, it is necessary to show that an
+ indirect store operation does not accidentally mutate a
+ register. To prove this and related properties, this
+ article advocates using the domain of bitwise linear
+ congruences in conjunction with intervals to derive
+ accurate range information. The paper argues that these
+ two domains complement one another when reasoning about
+ microcontroller code. The paper also explains how SAT
+ solving, which applied with dichotomic search, can be
+ used to recover branching conditions from binary code
+ which, in turn, further improves interval analysis."
+}
+
@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",
@@ -2954,6 +2981,36 @@ Summarizing:
techniques."
}
+@Article{Jakubczy12k,
+ Author = "K. Jakubczyk",
+ Title = "Sweeping in Abstract Interpretation",
+ Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})",
+ Publisher = "Elsevier Science Publishers B. V.",
+ Address = "Amsterdam, The Netherlands",
+ Volume = 288,
+ Pages = "25--36",
+ Year = 2012,
+ ISSN = "1571-0661",
+ Abstract = "In this paper we present how sweeping line techniques,
+ which are very popular in computational geometry, can be
+ adapted for static analysis of computer software by
+ abstract interpretation. We expose how concept of the
+ sweeping line can be used to represent elements of a
+ numerical abstract domain of boxes, which is a
+ disjunctive refinement of a well known domain of
+ intervals that allows finite number of disjunctions. We
+ provide a detailed description of the representation
+ along with standard domain operations
+ algorithms. Furthermore we introduce very precise
+ widening operator for the domain. Additionally we show
+ that the presented idea of the representation based on
+ sweeping line technique is a generalisation of the
+ representation that uses Linear Decision Diagrams (LDD),
+ which is one of possible optimisations of our idea. We
+ also show that the presented widening operator is often
+ more precise than the previous one."
+}
+
@Article{JhalaM09,
Author = "R. Jhala and R. Majumdar",
Title = "Software Model Checking",
Module: ppl/ppl
Branch: master
Commit: d86bf4a6f5e1353f04d4de18ab0197fda617ad5b
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d86bf4a6f5e1…
Author: Patricia Hill <patricia.hill(a)bugseng.com>
Date: Sat Dec 28 09:42:16 2013 +0000
More references added.
---
doc/ppl_citations.bib | 77 +++++++++++++++++++++++++++++++++++++++++++++++-
1 files changed, 75 insertions(+), 2 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 573ba03..3798fa2 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -1401,6 +1401,45 @@ Summarizing:
implementation over several benchmark systems."
}
+@Inproceedings{CostantiniFM13,
+ author = "G. Costantini and P. Ferrara and G. Maggiore",
+ title = "The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software",
+ Booktitle = "Formal Methods and Software Engineering:
+ Proceedings of 15th International Conference on Formal
+ Engineering Methods, {ICFEM} 2013",
+ Address = "Queenstown, New Zealand",
+ Series = "Lecture Notes in Computer Science",
+ Editor = "L. Groves and J. Sun",
+ Publisher = "Springer-Verlag, Berlin",
+ ISBN = "978-3-642-41201-1 (Print) 978-3-642-41202-8 (Online)",
+ Pages = "447--463",
+ Volume = 8144,
+ Year = 2013,
+ Abstract = "Computer Games Software deeply relies on physics
+ simulations, which are particularly demanding to analyze
+ because they manipulate a large amount of interleaving
+ floating point variables. Therefore, this application
+ domain is an interesting workbench to stress the
+ trade-off between accuracy and efficiency of abstract
+ domains for static analysis.
+
+ In this paper, we introduce Parametric Hypercubes, a
+ novel disjunctive non-relational abstract domain. Its
+ main features are: (i) it combines the low computational
+ cost of operations on (selected) multidimensional
+ intervals with the accuracy provided by lifting to a
+ power-set disjunctive domain, (ii) the compact
+ representation of its elements allows to limit the space
+ complexity of the analysis, and (iii) the parametric
+ nature of the domain provides a way to tune the
+ accuracy/efficiency of the analysis by just setting the
+ widths of the hypercubes sides.
+
+ The first experimental results on a representative
+ Computer Games case study outline both the efficiency
+ and the precision of the proposal."
+}
+
@Inproceedings{CovaFBV06,
Author = "M. Cova and V. Felmetsger and G. Banks and G. Vigna",
Title = "Static Detection of Vulnerabilities in x86 Executables",
@@ -2127,7 +2166,7 @@ Summarizing:
checkers."
}
-@Inproceedings{MihailaSS13a,
+@Inproceedings{GarocheKT13,
Author = "P.-L. Garoche and T. Kahsai and C. Tinelli",
Title = "Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers",
Booktitle = "NASA Formal Methods:
@@ -2164,6 +2203,40 @@ Summarizing:
our method."
}
+@Inproceedings{GhorbalIBMG12,
+ Author = "K Ghorbal and F Ivan{\vc}i{\'c} and G Balakrishnan and N Maeda",
+ Title = "Donut Domains:
+ Efficient Non-convex Domains for Abstract Interpretation",
+ Booktitle = "Verification, Model Checking, and Abstract Interpretation:
+ Proceedings of the 13th International Conference ({VMCAI} 2012)",
+ Address = "Philadelphia, PA, USA",
+ Editor = "V. Kuncak and A. Rybalchenko",
+ Publisher = "Springer-Verlag, Berlin",
+ Volume = 7148,
+ Year = 2012,
+ Pages = "235--250",
+ ISBN = "978-3-642-27939-3 (Print) 978-3-642-27940-9 (Online)",
+ Abstract = "Program analysis using abstract interpretation has been
+ successfully applied in practice to find runtime bugs or
+ prove software correct. Most abstract domains that are
+ used widely rely on convexity for their
+ scalability. However, the ability to express non-convex
+ properties is sometimes required in order to achieve a
+ precise analysis of some numerical properties. This work
+ combines already known abstract domains in a novel way
+ in order to design new abstract domains that tackle some
+ non-convex invariants. The abstract objects of interest
+ are encoded as a pair of two convex abstract objects:
+ the first abstract object defines an over-approximation
+ of the possible reached values, as is done
+ customarily. The second abstract object
+ under-approximates the set of impossible values within
+ the state-space of the first abstract object. Therefore,
+ the geometrical concretization of our objects is defined
+ by a convex set minus another convex set (or hole). We
+ thus call these domains donut domains."
+}
+
@PhdThesis{Gobert07th,
Author = "F. Gobert",
Title = "Towards putting abstract interpretation of {Prolog} into practice:
@@ -3599,7 +3672,7 @@ Summarizing:
@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",
+ Journal = "ACM SIGSOFT Software Engineering Notes",
Volume = 37,
Number = 6,
Year = 2012,
Module: ppl/ppl
Branch: master
Commit: 9580dfe6324b3bc6dddf9cfde3f4668e9858fea4
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9580dfe6324b…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 09:59:32 2013 +0100
Author field fixed.
---
doc/ppl_citations.bib | 2 +-
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index 27eab07..573ba03 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -4197,7 +4197,7 @@ Summarizing:
}
@Inproceedings{SharmaGHAN13,
- Author = "R. Sharma and S. Gupta and B. Hariharan and A. Aiken and AV. Nori",
+ Author = "R. Sharma and S. Gupta and B. Hariharan and A. Aiken and A. V. Nori",
Title = "Verification as Learning Geometric Concepts",
Booktitle = "Static Analysis:
Proceedings of the 20th International Symposium (SAS 2013)",
Module: ppl/ppl
Branch: master
Commit: 01fd0ad80bf20c095f6a3b03efdb093a4668c138
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=01fd0ad80bf2…
Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com>
Date: Sat Dec 28 09:57:46 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 5a3dbdd..27eab07 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -4845,7 +4845,8 @@ Summarizing:
@Incollection{ZuffereyWH12,
Author = "D. Zufferey and T. Wies and T. A. Henzinger",
Title = "Ideal Abstractions for Well-Structured Transition Systems",
- Booktitle = "Proceedings of 13th International Conference on Verification, Model Checking, and Abstract Interpretation, {VMCAI} 2012",
+ Booktitle = "Verification, Model Checking, and Abstract Interpretation:
+ Proceedings of 13th International Conference (VMCAI 2012)",
Series = "Lecture Notes in Computer Science",
Editor = "V. Kuncak and A. Rybalchenko",
Publisher = "Springer-Verlag, Berlin",
