../

Meeting

  • Deadline is on June 14 AOE
  • The discrepancy in the results was due to the fpu_ready signal. It was considered as a Runtime-Verified one as Rodinia was not ran on. After running rodinia it was falsified and never made it into to assumptions in the first place
  • We are not saying that our simple template is the be-all-end-all approach. With more complex templates, assumptions can lead to a closer matching of Runtime and Formal.
  • Our main contribution is moving cat-3 to cat-1 as assumptions and the assumption chain concept
  • HARM requires a signal to go high to capture it. Meaning for the template G(A -> X(B)), a signal that never goes high can never occur as A.

New experiments

  • Measure time without any assumptions
  • With Cat-3 assumptions
  • With Cat-1 assumptions
  • With Cat-3 and Cat-1 assumptions

Cactus plot

  • Can visualize the number of rules proven over time using a cactus plot

Figure changes

  • Add a circle around the part that is used as assumption in Fig. 7

  • In Fig. 5 show that assumptions are coming from another template

  • Better wording for “unverified”?

  • Does G(!A) do anything to G(A -> X(B))?