Yale internship
March to August 2010
With Zhong Shao.
Place
Computer Science department of Yale University (New Haven, USA)
Final report
Available as a PDF.
Done
TODO

Proof on mixed C and assembly :
Timeline
Week 19
 Tuesday : logical axioms used to simplify equivalence classes of assertions and trace equality
 Wednesday : code reorganisation for transition semantics, proof of ENV rule
Week 18
Week 17
 Monday : discussions about what to do next for historical logic and for a Coq implementation with Yanni
 Tuesday : reading about prophecy variables and the QED system
 Wednesday : coming back to the Coq code with a report on it
 Tuesday, Friday : cleaning of the Coq code, discussions with Yanni for an implementation design choice
Week 16
 Monday : beginning of a precise proof added to the report
 Tuesday, Wednesday : precise proof of "enqueue"
 Thursday : beginning of a precise proof for "dequeue", properties to ensure the guarantee
 Friday : end of the queue proof
Week 15
 Monday : proof of MCAS abandoned (historical logic not important), work on optimistic queue instead : report
 Tuesday : formalization of queue safety property
 Wednesday : key properties + sketch of the proof
 Thursday : discussions on the proof + potential dereferencing bug found
 Friday : in the train ; partially read articles : Mozes  Shavit queues, queues with GC verification, the Repeat Offender Problem
Week 14
 proof of the simple optimistic incrementation example
 thinking about logical variables formalization
 beginning of proof of MCAS
Week 13
 Monday : Coq : soundness formalization updated to the new report version
 Tuesday : Coq : code refractored into multiple files
 Wednesday : sick
 Thursday : work on Fu's stack proof
 Friday : work on Fu's stack proof + looking for other algorithms
Week 12
 Monday : Coq
 Tuesday : Coq
 Wednesday : Coq : soundness proof for 2 sequential rules
 Thursday : Coq : formalization of last cases for sequential rules, beginning of RG rules
 Friday : Coq : soundness theorems formalization
Week 11
 Monday : application of RGSep in Victor's PhD read
 Tuesday : Ming Fu's logic formalization started
 Wednesday : Coq
 Thursday : Coq
 Friday : Coq
Week 10
Week 9
 unsuccessful tests on a toy language with inlined C code : Coq source
 NEPLS seminar
Week 8
 Incrementation operation added to CompCert
 Look at the external function calls formalisation
Week 7
Week 6
 look CompCert source code
 learn basis about the PowerPC assembly
 Coq, CompCert, cross compiler chain, PowerPC emulator installed
Week 5
Week 4
Week 3
 trying to catch the OS class during Spring Break
Week 2
Week 1