Index: papers/FDL2012/myBib.bib
===================================================================
--- papers/FDL2012/myBib.bib	(revision 92)
+++ papers/FDL2012/myBib.bib	(revision 101)
@@ -10,8 +10,7 @@
 
 @ARTICLE{clarke94model,
-  author = {E.M.~Clarke and O.~Grumberg and D.E.~Long},
-  title = {{Model Checking and Abstraction}},
+  author = {E. M.~Clarke and O.~Grumberg and D.E.~Long},
+  title = {Model Checking and Abstraction},
   journal = {ACM Transactions on Programming Languages and Systems},
-  year = {1994},
   volume = {16},
   pages = {1512--1542},
@@ -21,6 +20,9 @@
   issn = {0164-0925},
   keywords = {model cheking, abstraction, CTL, preservation},
-  publisher = {ACM Press}
-}
+  publisher = {ACM Press},
+  year = {1994}
+}
+
+
 @PHDTHESIS{braunstein_phd07,
   author = {C.~Braunstein},
@@ -28,7 +30,7 @@
 	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)}},
+  school = {UniversitÃ© Pierre et Marie Curie},
   year = {2007},
-  address = {LIP6/SOC},
+  address = {LIP6-SOC},
   owner = {cecile},
   timestamp = {2007.04.16}
@@ -46,11 +48,11 @@
 @conference{ ClarkeEmerson81temporal_logic,
    author = "E. M. Clarke and  E. A. Emerson",
-   title = "Design and systhesis of synchronization  skeletons using branching time temporal logic",
-   booktitle = "In Logic of Programs Workshop",
+   title = "Design and systhesis of synchronization skeletons using branching time temporal logic",
+   booktitle = "Logic of Programs Workshop",
    volume = 131,
    address = "Yorktown Heights, New York",
-   year = 1981,
    month = May,
-   publisher = "LNCS 131, Springer "
+   publisher = "LNCS 131, Springer",
+   year = 1981
 }
 
@@ -62,6 +64,5 @@
    number = 2,
    pages = {244-263},
-   year = 1986,
-   month = Apr
+   year = 1986
 }
 
@@ -69,8 +70,8 @@
    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 = "CAV'00",
    address = "Chicago, IL",
-   year = 2000,
-   publisher = "LNCS"
+   publisher = "LNCS",
+   year = 2000
 }
 
@@ -78,10 +79,10 @@
    author = "J. P. Queille and J. Sifakis",
    title = "Specification and verification of concurrent systems in CESAR",
-   booktitle = "In Proceedings of the 5th International Symposium on Programming",
+   booktitle = "Proceedings of the 5th International Symposium on Programming",
    volume = 137,
    address = "Turin, Italy",
-   year = 1982,
    month = April,
-   publisher = "LNCS 137, Springer "
+   publisher = "LNCS 137, Springer",
+   year = 1982
 }
 
@@ -90,9 +91,9 @@
 @conference{ BCCFZ04SMC_with_SAT,
     author = "A. Biere and A. Cimatti and E. Clarke and M.Fujita and Y. Zhu",
-    title = "{ Symbolic Model  Checking using SAT procedures instead of BDDs}",
+    title = "{Symbolic Model  Checking using SAT procedures instead of BDDs}",
      booktitle = {Proceedings: Design Automation Conference (DAC '99)},
     pages = {317-320},
-    year = 1999,
     month = February,
+    year = 1999
 }
 
@@ -101,7 +102,6 @@
     author = "The VIS Group",
     title = "{VIS: A system for Verification and Synthesis}",
-    journal = {Springer Lecture Notes in Computer Science},
+    journal = {Springer LNCS},
     volume = 1102,
-    number = 1102,
     pages = {428-432},
     year = 1996
@@ -114,7 +114,7 @@
      booktitle = {16th Conference on Computer Aided Verification (CAV '04)},
     pages = {519-522},
-    year = 2004,
     month = Jul,
-    publisher = "LNCS 3114"
+    publisher = "LNCS 3114",
+    year = 2004
 }
 
@@ -154,10 +154,10 @@
    author = "C. Roux and  E. Encrenaz ",
    title = "{CTL} may be ambigous when model-checking {Moore Machines} ",
-   booktitle = " IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
+   booktitle = "IFIP WG 10.5 12th International Advance Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)",
    volume = 2860,
    address = "Italy",
-   year = 2003,
    month = Nov,
-   publisher = "LNCS"
+   publisher = "LNCS",
+   year = 2003
 }
 
@@ -166,9 +166,9 @@
    author = "F. Xie and J.C. Browne ",
    title = "{Verified Systems by Composition from Verified Components} ",
-   booktitle = " In ESEC/FSE 2003: Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering Conference",
+   booktitle = "ESEC/FSE 2003: 11th ACM SIGSOFT Symposium on Foundations of Software Eng. Conf.",
    pages = {227-286},
-   address = "Helsinki, Finland",
-   year = 2003,
-   publisher = "ACM Press"
+   address = "Finland",
+   publisher = "ACM Press",
+   year = 2003
 }
 
@@ -177,9 +177,9 @@
    author = "J. Li and X. Sun and F. Xie and X. Song",
    title = "{Component-Based Abstraction Refinement} ",
-   booktitle = "In Proc. of 10th International Conference on Software Reuse (ICSR)",
+   booktitle = "10th Int. Conf. on Software Reuse (ICSR)",
    pages = {39-51},
-   address = "Beijing, China",
-   year = 2008,
-   publisher = "Springer-Verlag"
+   address = "China",
+   publisher = "Springer-Verlag",
+   year = 2008
 }
 
@@ -189,9 +189,9 @@
    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 = "ICCDâ02: 20th Int. Conference on Computer Design",
    pages = {70-75},
    address = "Freiburg, Germany",
-   year = 2002,
-   publisher = "IEEE Computer Society"
+   publisher = "IEEE Computer Society",
+   year = 2002
 }
 
@@ -200,5 +200,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 = "FDLâ06: Forum on specification and Design Languages",
    year = 2006
 }
@@ -207,21 +207,21 @@
 @conference{ CiardoLS00mdd_async,
    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",
+   title = "{Efficient symbolic state-space construction for asynchronous systems} ",
+   booktitle = "Proc. of ICATPN '2000",
    volume = 1825,
    pages = {103-122},
-   year = 2000,
-   publisher = "LNCS, Springer Verlag"
+   publisher = "LNCS, Springer Verlag",
+   year = 2000
 }
 
 @conference{ CTM05hdd,
    author = "J-M. Couvreur and Y. Thierry-Mieg",
-   title = "{ Hierarchical Decision Diagrams to Exploit Model Structure} ",
-   booktitle = "In FORTE : Proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked  and Distributed Systems",
+   title = "{Hierarchical Decision Diagrams to Exploit Model Structure} ",
+   booktitle = "FORTE: 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems",
    volume = 3731,
    pages = {443-457},
    address = "Taipei, Taiwan",
-   year = 2005,
-   publisher = "LNCS, Springer"
+   publisher = "LNCS, Springer",
+   year = 2005
 }
 
@@ -229,32 +229,32 @@
 @conference{ HQR98assume_guarantee,
    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 Int. Conference on Computer Aided Verification",
+   title = "{You Assume, We Guarantee: Methodology and Case Studies} ",
+   booktitle = "CAVâ98",
    volume = 1427,
    pages = {440-451},
-   address = "Vancouver, Canada",
-   year = 1998,
-   publisher = " LNCS, Springer-Verlag"
+   address = "Canada",
+   publisher = "Springer-Verlag",
+   year = 1998
 }
 
 
 @conference{ GrumbergLong91assume_guarantee,
-   author = " O. Grumberg and D. E. Long",
-   title = "{  Model Checking and Modular Verification} ",
-   booktitle = " In International Conference on Concurency Theory",
+   author = "O. Grumberg and D. E. Long",
+   title = "{Model Checking and Modular Verification}",
+   booktitle = "Int. Conference on Concurency Theory",
    volume = 527,
    pages = {250-263},
-   year = 1991,
-   publisher = " LNCS, Springer-Verlag"
+   publisher = "Springer-Verlag",
+   year = 1991
 }
 
 
 @conference{ GrafSaidi97abstract_construct,
-   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",
+   author = "S. Graf and H. SaÃ¯di",
+   title = "{Construction of Abstract State Graphs with PVS}",
+   booktitle = "Computer Aided Verification (CAVâ97)",
    volume = 1254,
-   year = 1997,
-   publisher = " LNCS, Springer"
+   publisher = "LNCS, Springer",
+   year = 1997
 }
 
@@ -262,11 +262,11 @@
 
 @conference{ PardoHachtel97autoAbsMC,
-   author = "  S. Pardo and G. Hachtel",
-   title = "{ Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
-   booktitle = " In CAV â97",
+   author = "S. Pardo and G. Hachtel",
+   title = "{Automatic Abstraction Technique for Propositional mu-Calculus Model Checking} ",
+   booktitle = "CAVâ97",
    volume = 1254,
    pages = {12-23},
-   year = 1997,
-   publisher = " LNCS, Springer-Verlag"
+   publisher = "Springer-Verlag",
+   year = 1997
 }
 
@@ -274,8 +274,8 @@
 @conference{ PardoHachtel98incremCTLMC,
    author = "  S. Pardo and G. Hachtel",
-   title = "{ Incremental CTL Model Checking Using BDD Subsetting} ",
-   booktitle = " In DAC â98: 35th Design Automation Conference ",
+   title = "{Incremental CTL Model Checking Using BDD Subsetting} ",
+   booktitle = "DAC â98: 35th Design Automation Conference ",
    pages = {457-462},
-   year = 1998,
+   year = 1998
 }
 
@@ -283,77 +283,77 @@
 @conference{ Burch_al91smc_part_transition,
    author = " J. R. Burch and E. M. Clarke and D. E. Long",
-   title = "{ Symbolic Model Checking with Partitioned Transition Relations} ",
+   title = "{Symbolic Model Checking with Partitioned Transition Relations} ",
    booktitle = "Proceedings of the 1991 International Conference on VLSI",
    pages = {49-58},
    month = August,
-   year = 1991,
+   year = 1991
 }
 
 
 @conference{ Burch_al93smc_circuit_verif,
-   author = " J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli",
-   title = "{ Symbolic Model Checking for Sequential Circuit Verification} ",
-   booktitle = " IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
+   author = "J. R. Burch and E. M. Clarke and D. E. Long and K. L. Mcmillan and D.L. Dilli",
+   title = "{Symbolic Model Checking for Sequential Circuit Verification} ",
+   booktitle = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
    volume = {13(4)},
    pages = {401-424},
-   year = 1993,
+   year = 1993
 }
 
 
 @conference{ Kroening_al07vcegar,
-   author = " Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke",
-   title = "{ VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
-   booktitle = " In TACAS '07 ",
-   year = 2007,
+   author = " H. Jain and D. Kroening and N. Sharygina and E. Clarke",
+   title = "{VCEGAR: Verilog CounterExample Guided Abstraction Refinement} ",
+   booktitle = "TACAS'07 ",
+   year = 2007
 }
 
 
 @ARTICLE { Sharygina_al12PreciseApprox,
-    AUTHOR = { Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich },
-    TITLE = { {An Abstraction Refinement Approach Combining Precise and Approximated Techniques} },
-    JOURNAL = { International Journal on Software Tools for Technology Transfer (STTT) },
+    AUTHOR = {N. Sharygina and S. Tonetta and A. Tsitovich},
+    TITLE = {An Abstraction Refinement Approach Combining Precise and Approximated Techniques},
+    JOURNAL = {International Journal on Software Tools for Technology Transfer},
     VOLUME = {14},
     PAGES ={1-14},
-    YEAR = { 2012},
+    YEAR = {2012}
 }
 
 
 @conference{ microsoft04SLAM,
-   author = " Thomas Ball and Byron Cook and Vladimir Levin and Sriram K. Rajamani",
-   title = "{ SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
-   booktitle = "In 4th Int. Conference on Integrated Formal Methods (IFM 2004)",
+   author = "T. Ball and B. Cook and V. Levin and S. K. Rajamani",
+   title = "{SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft} ",
+   booktitle = "4th Int. Conf. on Integrated Formal Methods",
    volume = 2999,
    pages = {1-20},
-   year = 2004,
-   publisher = " LNCS, Springer"
+   publisher = "Springer",
+   year = 2004
 }
 
 
 @conference{ berkeley07BLAST,
-   author = "  Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
-   title = "{ The Software Model Checker Blast: Applications to software engineering.} ",
-   booktitle = " International Journal on Software Tools for Technology Transfer",
+   author = "D. Beyer and T. A. Henzinger and R. Jhala and R. Majumdar",
+   title = "{The Software Model Checker Blast: Applications to software engineering} ",
+   booktitle = "Int. Journal on Software Tools for Technology Transfer",
    volume = {9 (5-6)},
    pages = {505-525},
-   year = 2007,
+   year = 2007
 }
 
 
 @inproceedings{pwk2009-date,
-  AUTHOR    = { Mitra Purandare and Thomas Wahl and Daniel Kroening },
-  TITLE     = { Strengthening Properties using Abstraction Refinement },
-  BOOKTITLE = { Proceedings of DATE 2009 },
-  YEAR      = { 2009 },
-  PUBLISHER = { ACM },
-  PAGES     = { 1692-1697 },
+  AUTHOR    = {M. Purandare and T. Wahl and D. Kroening},
+  TITLE     = {Strengthening Properties using Abstraction Refinement},
+  BOOKTITLE = {Proceedings of DATE 2009},
+  PUBLISHER = {ACM},
+  PAGES     = {1692-1697},
+  YEAR      = {2009}
 }
 
 
 @conference{ Kunz_al11ipc_abs,
-   author = " Minh D. Nguyen and Markus Wedler and Dominik Stoffel and Wolfgang Kunz ",
-   title = "{ Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}",
-   booktitle = "48th Proc. Design Automation Conference (DAC '11)",
+   author = "M. D. Nguyen and M. Wedler and D. Stoffel and W. Kunz ",
+   title = "{Formal Hardware/Software Co-Verification by Interval Property Checking with Abstraction}",
+   booktitle = "Design Automation Conference (DAC'11)",
    address = "San Diego, USA",
-   year = 2011,
+   year = 2011
 }
 
@@ -363,6 +363,5 @@
  publisher = "Addison-Wesley",
  title     = "The {\TeX}book",
- year      =  1984,
- isbn      = ""
+ year      =  1984
 }
 
