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 in-lined 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