Timeline
Feb 24, 2012:
- 7:01 PM Changeset [1758] by
- Minor improvements to front-end; add an overall statement.
- 6:13 PM Changeset [1757] by
- …
- 5:59 PM Changeset [1756] by
- Improved outline.
- 5:49 PM Changeset [1755] by
- …
- 5:46 PM Changeset [1754] by
- …
- 5:36 PM Changeset [1753] by
- …
- 5:18 PM Changeset [1752] by
- …
- 5:09 PM Changeset [1751] by
- Commit to avoid conflicts with Claudio
- 5:02 PM Changeset [1750] by
- start of ERTL to LTL
- 4:55 PM Changeset [1749] by
- Rephrased introduction.
- 4:53 PM Changeset [1748] by
- commit to avoid conflicts
- 4:25 PM Changeset [1747] by
- - New and updated version of effort table
- 4:09 PM Changeset [1746] by
- Revisions to front-end text.
- 4:07 PM Changeset [1745] by
- Conclusions.
- 4:03 PM Changeset [1744] by
- - New version of effort table
- 3:45 PM Changeset [1743] by
- diagrams finished, adding text
- 3:40 PM Changeset [1742] by
- - committed new version of effort table
- 3:24 PM Changeset [1741] by
- …
- 2:32 PM Changeset [1740] by
- …
- 2:30 PM Changeset [1739] by
- Footnote for optimizations.
- 2:05 PM Changeset [1738] by
- - small change (layout)
- 2:04 PM Changeset [1737] by
- - small change
- 1:19 PM Changeset [1736] by
- Show that the bound on the number of instructions until a cost label …
- 1:00 PM Changeset [1735] by
- a bit more added
- 11:44 AM Changeset [1734] by
- followed brian's lead in explaining the backend translation steps with …
- 10:10 AM Changeset [1733] by
- More on front-end.
Feb 23, 2012:
- 7:07 PM Changeset [1732] by
- More on front-end.
- 5:25 PM Changeset [1731] by
- A bit of front-end proof outline.
- 5:17 PM Changeset [1730] by
- Minor changes while studying the proof.
- 2:29 PM Changeset [1729] by
- Comment left from SVN merge removed.
- 1:48 PM Changeset [1728] by
- avoiding conflicts
- 1:47 PM Changeset [1727] by
- - added last RTL - ERTL diagrams
- 1:14 PM Changeset [1726] by
- Finished description of LTL to LIN
- 12:51 PM Changeset [1725] by
- commit to avoid conflicts
- 12:51 PM Changeset [1724] by
- - added diagrams to RTL to ERTL section
- 10:41 AM Changeset [1723] by
- added more to header of file, commit to avoid conflicts with jaap
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
Note: See TracTimeline
for information about the timeline view.
