Index: /papers/FDL2012/abstraction_refinement.tex
===================================================================
--- /papers/FDL2012/abstraction_refinement.tex	(revision 56)
+++ /papers/FDL2012/abstraction_refinement.tex	(revision 57)
@@ -47,4 +47,5 @@
 \item  $\sigma$ is not a path of the concrete system $M$: $\exists k$ such
 that $(s_{k}, s_{k+1}) \not\in R$.
+\end{itemize}
 \end{definition}
 
Index: /papers/FDL2012/framework.tex
===================================================================
--- /papers/FDL2012/framework.tex	(revision 56)
+++ /papers/FDL2012/framework.tex	(revision 57)
@@ -114,5 +114,5 @@
 
 As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property.
-The AKS composition has been defined in \cite{these_braunstein}; it extends
+The AKS composition has been defined in \cite{braunstein_phd07}; it extends
 the classical synchrounous composition of Moore machine to deal with
 four-valued variables.
Index: /papers/FDL2012/myBib.bib
===================================================================
--- /papers/FDL2012/myBib.bib	(revision 56)
+++ /papers/FDL2012/myBib.bib	(revision 57)
@@ -43,5 +43,5 @@
    author = "E. M. Clarke and  O. Grumberg and S. Jha and Y. Lu and H. Veith",
    title = "{Counterexample-guided Abstraction Refinement}",
-   booktitle = "Computer Aided Verification (CAV '00)",
+   booktitle = "Computer Aided Verification (CAV'00)",
    address = "Chicago, IL",
    year = 2000,
@@ -86,5 +86,5 @@
     author = "H. S. Jin and M. Awedh and F. Somenzi",
     title = "{CirCUs: A Satisfiablilty Solver Geared Towards Bounded Model Checking}",
-     booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
+     booktitle = {16th Conference on Computer Aided Verification (CAV'04)},
     pages = {519-522},
     year = 2004,
@@ -111,6 +111,6 @@
 @article{ bara08abs_composant,
     author = "A. Bara",
-    title = "{Abstraction de Composant pour la Vérification par Model-Checking}",
-    journal = {Mémoire de DiplÎme Universitaire OMP - LIP6-SOC},
+    title = "{Abstraction de Composant pour la Vérification par Model-Checking}",
+    journal = {Mémoire de DiplÎme Universitaire OMP - LIP6-SOC},
     year =  2008
 }
@@ -143,5 +143,5 @@
    author = "H. Peng and Y. Mokhtari and S. Tahar ",
    title = "{Environment Synthesis for Compositional Model Checking} ",
-   booktitle = "In ICCD’02 : Proceedings of the 20th International Conference on Computer Design",
+   booktitle = "In ICCD'02 : Proceedings of the 20th International Conference on Computer Design",
    pages = {70-75},
    address = "Freiburg, Germany",
@@ -154,5 +154,5 @@
    author = "M. Schickel  and V. Nimbler and M. Braun and H. Eveking ",
    title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ",
-   booktitle = "In FDL’06: Proceedings of  Forum on specification and Design Languages",
+   booktitle = "In FDL'06: Proceedings of  Forum on specification and Design Languages",
    year = 2006
 }
@@ -160,5 +160,5 @@
 
 @conference{ CiardoLS00mdd_async,
-   author = "G.Ciardo and G. LÃŒttgen and R. Siminiceanu",
+   author = "G.Ciardo and G. LÌttgen and R. Siminiceanu",
    title = "{ Efficient symbolic state-space construction for asynchronous systems} ",
    booktitle = "In Proc. of ICATPN '2000",
@@ -184,5 +184,5 @@
    author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani",
    title = "{ You Assume, We Guarantee : Methodology and Case Studies} ",
-   booktitle = "CAV ’98 : Proceedings of the 10th International Conference on Computer Aided Verification",
+   booktitle = "CAV'98 : Proceedings of the 10th International Conference on Computer Aided Verification",
    volume = 1427,
    pages = {440-451},
@@ -205,7 +205,7 @@
 
 @conference{ GrafSaidi97abstract_construct,
-   author = "  S. Graf and H. Saïdi",
+   author = "  S. Graf and H. Saïdi",
    title = "{ Construction of Abstract State Graphs with PVS} ",
-   booktitle = " In CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification",
+   booktitle = " In CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification",
    volume = 1254,
    year = 1997,
@@ -290,4 +290,15 @@
 }
 
+@PHDTHESIS{braunstein_phd07,
+  author = {C.~Braunstein},
+  title = {"Conception Incrémentale, Vérification de Composants Matériels et
+	Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur
+	Puce"},
+  school = {{Universitée Pierre et Marie Curie (Paris 6)}},
+  year = {2007},
+  address = {LIP6/SOC},
+  owner = {cecile},
+  timestamp = {2007.04.16}
+}
 
 @misc{ patanshnik88bibtex,