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

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

  • administrative stuffs