Update drafts.

bibs/header.bib

@@ -772,6 +772,7 @@ STRING{fse08        = fse # ", Atlanta, Georgia" }
 @STRING{tacas06     = tacas # ", Vienna, Austria" }
 @STRING{tacas08     = tacas # ", Budapest, Hungary" }
 @STRING{tacas12     = tacas # ", Tallinn, Estonia" }
+@STRING{tacas13     = tacas # ", Rome, Italy" }
 @STRING{tacas15     = tacas # ", London, England" }
 @STRING{tacas16     = tacas # ", Eindhoven, The Netherlands" }
 % ---

bibs/myrefs.bib

@@ -1,4 +1,12 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+@unpublished{AH18,
+  title    = {Constraint-Based Synthesis of Coupling Proofs},
+  author   = {Albarghouthi, Aws and
+              Hsu, Justin},
+  year     = {2018},
+  jh       = yes,
+}
+
 @unpublished{SBGHK17,
   title  = {Reasoning about Divergences for Relaxations of Differential Privacy},
   author = {Sato, Tetsuya and
@@ -3675,10 +3683,11 @@ year           = {2011}
   publisher    = elsevier
 }
 
-@misc{RandZdancewic15,
-  author       = {Rand, Robert and Zdancewic, Steve},
-  title        = {A Formally Verified Probabilistic {Hoare} Logic with Non-Termination},
-  year         = 2015
+@InProceedings{RandZ15,
+  author = 	 {Robert Rand and Steve Zdancewic},
+  title = 	 {{VPHL}: A Verified Partial-Correctness Logic for Probabilistic Programs},
+  booktitle = mfps15,
+  year = 	 {2015},
 }
 
 inproceedings{Kozen79,
@@ -4963,7 +4972,6 @@ inproceedings{LarsenS89,
  url = {https://doi.acm.org/10.1145/1706299.1706337},
  doi = {10.1145/1706299.1706337},
  acmid = {1706337},
- address = {New York, NY, USA},
  keywords = {proof-theoretic program synthesis, verification},
 }
 
@@ -4977,7 +4985,6 @@ inproceedings{LarsenS89,
  pages = {221--233},
  numpages = {13},
  acmid = {2535860},
- address = {New York, NY, USA},
  keywords = {games, horn clauses, program synthesis, proof rules, reactive synthesis, static analysis},
 }