upenn-acg/verified-tsan

Issues

• [supporting lemma]: extended version of exec_fail_iexec

  #7 opened 8 years ago by stilltracy
  0

• admits in first_fail & first_fail'

  #12 opened 9 years ago by stilltracy
  1

• uninstantiated existential in instrument_sim_safe

  #11 opened 9 years ago by stilltracy
  1

• uninstantiated existential in hb_check_fail_spec_n'

  #10 opened 9 years ago by stilltracy
  1

• uninstantiated existential in instrument_sim_race2::load

  #9 opened 9 years ago by stilltracy
  1

• [supporting lemma]: initialized should imply can_write

  #8 opened 9 years ago by stilltracy
  1

• [supporting lemma]: conditional transitivity&symmetry of mem_vals

  #5 opened 9 years ago by stilltracy
  1

• [supporting lemma]: extended version of state_sim_steps

  #6 opened 9 years ago by stilltracy
  1

• using induction on a hypothesis causes loss of information

  #3 opened 9 years ago by stilltracy
  1

• initial memory of the original program vs. instrumented program

  #4 opened 9 years ago by stilltracy
  1

• [TODO]: prove a corollary of instrument_sim_safe2 that holds for iexec_star

  #1 opened 9 years ago by stilltracy
  2

• [TODO]: proof structure of the "soundness" direction in the correctness theorem

  #2 opened 9 years ago by stilltracy
  0