more

publications.bib

@@ -206,7 +206,7 @@ throughout the proof.}
 @InProceedings{Gardner2010Reasoning,
   Title                    = {{Reasoning About Client-side Web Programs: Invited Talk}},
   Author                   = {Philippa Gardner},
-  Booktitle                = {Proceedings of the 2010 {EDBT/ICDT} Workshops, Lausanne, Switzerland, March 22-26, 2010},
+  Booktitle                = {Proceedings of the {EDBT/ICDT} Workshops},
   Year                     = {2010},
   doi                      = {10.1145/1754239.1754261},
   
@@ -359,7 +359,7 @@ We introduce a program logic for reasoning about a broad subset of JavaScript, i
 @InProceedings{Maffeis2004Behavioural,
   Title                    = {{Behavioural Equivalences for Dynamic Web Data}},
   Author                   = {Sergio Maffeis and Philippa Gardner},
-  Booktitle                = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {TCS}},
+  Booktitle                = {Proceedings of 3\textsuperscript{rd} International Conference on Theoretical Computer Science {(TCS)}},
   Year                     = {2004},
   Pages                    = {535--548},
   
@@ -583,6 +583,7 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
     school                  = {Imperial College London},
     author                  = {Gian Ntzik},
     year                    = {2016}, 
+    phdthesis               = {Y},
     
     Project                 = { concurrency },
     
@@ -594,7 +595,8 @@ Building on separation logic with concurrent abstract predicates (CAP), we intro
     school                  = {Imperial College London},
     author                  = {Pedro {da Rocha Pinto}},
     year                    = {2016}, 
-
+    phdthesis               = {Y},
+    
     Project                 = { concurrency },
     
     Abstract                = {In this thesis, we address the problem of verifying the functional correctness of concurrent programs, with emphasis on fine-grained concurrent data structures. Reasoning about such programs is challenging since data can be concurrently accessed by multiple threads: the reasoning must account for the interference between threads, which is often subtle. To reason about interference, concurrent operations should either be at distinct times or on distinct data. We present TaDA, a sound program logic for verifying clients and implementations that use abstract specifications that incorporate both abstract atomicity—the abstraction that operations take effect at a single, discrete instant in time—and abstract disjointness—the abstraction that operations act on distinct data resources. Our key contribution is the introduction of atomic triples, which offer an expressive approach for specifying program modules. We also present Total-TaDA, a sound extension of TaDA with which we can verify total correctness of concurrent programs, i.e. that such programs both produce the correct result and terminate. With Total-TaDA, we can specify constraints on a thread’s concurrent environment that are necessary to guarantee termination. This allows us to verify total correctness for nonblocking algorithms and express lock- and wait-freedom. More generally, the abstract specifications can express that one operation cannot impede the progress of another, a new non-blocking property that we call non-impedance. Finally, we describe how to extend TaDA for proving abstract atomicity for data structures that make use of helping—where one thread is performing an abstract operation on behalf of another—and speculation—where an abstract operation is determined by future behaviour.}