| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-12 | Prove test_raw_add theorem for init_state | Ramana Kumar | |
| It can be proved almost entirely by symbolic execution (in <15s) _if_ the right definitions are in the compset. It took a lot of interactive stumbling about to discover that LUPDATE was missing from the standard list compset. | |||
| 2018-06-12 | Make progress on HOL4 test_raw_add | Ramana Kumar | |
| The proof now gets through simulation of the first instruction of the test. | |||
| 2018-06-12 | Work on HOL symbolic evaluation of installing code | Ramana Kumar | |
| 2018-06-12 | Experimentation with PrePost for test_raw_add | Ramana Kumar | |
| 2018-06-12 | Speculation on executing a CHERI test in HOL4 | Ramana Kumar | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |