Timeline
Feb 22, 2012:
- 5:12 PM Changeset [1722] by
- changes to english in third part of report
- 2:38 PM Changeset [1721] by
- some changes to the report
- 2:37 PM Changeset [1720] by
- New draft.
- 2:06 PM Changeset [1719] by
- Show that non-termination survives a terminating function call.
- 1:54 PM Changeset [1718] by
- added skull.sty for daemon (skull) symbol
- 11:28 AM Changeset [1717] by
- added diagrams.sty for drawing commutative diagrams
- 11:00 AM Changeset [1716] by
- proof outline, as requested by referees, being typed up in latex
- 10:10 AM Changeset [1715] by
- Some progress.
Feb 21, 2012:
- 4:22 PM Changeset [1714] by
- …
- 11:58 AM Changeset [1713] by
- Add a distinguished final state to the front-end languages to match up …
- 11:58 AM Changeset [1712] by
- Show that constructing an RTLabs structure trace really does use a …
Feb 20, 2012:
- 11:15 AM Changeset [1711] by
- finished block_cost' proof: 1.5 minutes to typecheck qed.
- 10:04 AM Changeset [1710] by
- changes from friday afternoon
Feb 17, 2012:
- 11:52 AM Changeset [1709] by
- Changes to the execution of the MOVC instruction
- 11:51 AM Changeset [1708] by
- Change to the execution of the MOVC instruction
Feb 16, 2012:
- 6:05 PM Changeset [1707] by
- Progress on finite segments of infinite RTLabs structured trace.
- 6:05 PM Changeset [1706] by
- Checkpoint RTLabs structured traces.
- 6:05 PM Changeset [1705] by
- Checkpoint RTLabs labelling soundness work.
- 4:54 PM Changeset [1704] by
- typo
- 11:41 AM WikiStart edited by
- change of title for wilmer (diff)
- 11:36 AM Changeset [1703] by
- minimal change
- 11:35 AM Changeset [1702] by
- updated the report and changed a bit the names
- 11:25 AM Changeset [1701] by
- added updated compiler tarball
- 11:23 AM Changeset [1700] by
- updated README
- 11:22 AM Changeset [1699] by
- 5.1 up
- 11:05 AM Changeset [1698] by
- minor modifications
Feb 15, 2012:
- 6:02 PM Changeset [1697] by
- important bug found
- 4:09 PM Changeset [1696] by
- finished adding russell types to the traverse_cost_* functions
- 2:10 PM Changeset [1695] by
- Progress on CostsProof?.ma file.
- 9:30 AM Changeset [1694] by
- indexed labels branch
Feb 14, 2012:
- 4:38 PM Changeset [1693] by
- Changes to ASMCosts and CostsProofs? files to get everything working again.
- 1:18 PM Changeset [1692] by
- resolved conflict in asm costs this morning
- 1:43 AM Changeset [1691] by
- Some progress in the proof: less daemons, less hypotheses in lemmas.
Feb 13, 2012:
- 3:58 PM Changeset [1690] by
- nested loops are not supported yet, the only test had one
- 3:54 PM Changeset [1689] by
- kept out the wrapper (which I did not touch, so not sure it works)
- 9:08 AM Changeset [1688] by
- up d5.1-5.3
Feb 10, 2012:
- 2:12 PM Changeset [1687] by
- corrected title
Feb 9, 2012:
- 6:16 PM Changeset [1686] by
- corrected abstract
- 6:08 PM Changeset [1685] by
- adjusted comparison with aiT
- 5:42 PM Changeset [1684] by
- changes from the past week
- 5:41 PM Changeset [1683] by
- abstract and running example
- 1:22 PM Changeset [1682] by
- Complete proof for as_after_return for RTLabs.
- 1:22 PM Changeset [1681] by
- Checkpoint of stack preservation work in RTLabs.
- 1:22 PM Changeset [1680] by
- Comment out unused tailcalls in Cminor and RTLabs. (They would be a …
Feb 7, 2012:
- 6:01 PM Changeset [1679] by
- Frama-C plug-in (sources+documentation)
- 4:36 PM Changeset [1678] by
- finished editing the english in the report
- 12:23 PM Changeset [1677] by
- changes to paolo's english in the report, about a 1/4 of the way through
Feb 6, 2012:
- 6:50 PM Changeset [1676] by
- corrected some faults still TODO: running example, language corrections
- 3:33 PM Changeset [1675] by
- Some work on sound labelled for RTLabs.
- 12:32 PM Changeset [1674] by
- corrected some faults still TODO: running example, language corrections
Feb 4, 2012:
- 11:58 AM Changeset [1673] by
- report on indexed labels TODO: corrections, examples, etc
Feb 1, 2012:
- 4:16 PM Changeset [1672] by
- Matita now generates a couple of inversion lemmas that were manually …
- 4:16 PM Changeset [1671] by
- A little more on RTLabs infinite traces.
- 4:16 PM Changeset [1670] by
- Snapshot of non-terminating RTLabs structured traces work.
- 3:36 PM Changeset [1669] by
- Commit for claudio
Jan 30, 2012:
- 11:41 AM Changeset [1668] by
- - split build_maps into build_maps and build_maps_ok - work with CSC …
Jan 29, 2012:
- 10:25 PM Changeset [1667] by
- Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
Jan 28, 2012:
- 1:42 PM Changeset [1666] by
- PreStatus? datatype change: the code_memory field is not a left …
Jan 27, 2012:
- 5:05 PM Changeset [1665] by
- progress on closing holes in block_cost' proof
- 12:11 AM Changeset [1664] by
- corrected a bug in loop peeling where continue and breaks were not …
Jan 26, 2012:
- 5:40 PM Changeset [1663] by
- old cases working again, work on new ones
- 10:06 AM Changeset [1662] by
- rev
- 10:04 AM Changeset [1661] by
- rev
- 8:58 AM Changeset [1660] by
- Deliverable: Frama-C plug-in (D5.1-5.3)
- 8:43 AM Changeset [1659] by
Jan 25, 2012:
- 6:18 PM Changeset [1658] by
- asm costs changes from today
- 5:40 PM Changeset [1657] by
- preliminary version of D5
Jan 23, 2012:
- 7:01 PM Changeset [1656] by
- Minor fixups to RTLabs/Traces due to syntax changes.
- 6:31 PM Changeset [1655] by
- Update Cminor and RTLabs semantics to use new monad definitions.
- 5:37 PM Changeset [1654] by
- Corrections to structured trace definitions (see the mailing list). …
- 5:37 PM Changeset [1653] by
- Start on building finite sections of non-terminating structured traces.
- 5:37 PM Changeset [1652] by
- Forgot to apply 1583 to non-terminating case.
- 5:37 PM Changeset [1651] by
- Start looking at non-terminating structured traces by defining …
Note: See TracTimeline
for information about the timeline view.
