Timeline
Mar 2, 2012:
- 4:28 PM Changeset [1804] by
- The submitted version.
- 4:27 PM Changeset [1803] by
- yet another small correction in the LTL to LIN part
- 3:55 PM Changeset [1802] by
- other small corrections
- 3:16 PM Changeset [1801] by
- small correction
Mar 1, 2012:
- 5:29 PM Changeset [1800] by
- Applied suggestions by Roberto.
- 4:49 PM Changeset [1799] by
- Applied Roberto's suggestions.
- 4:23 PM Changeset [1798] by
- Applied comments by Brian, Randy and Roberto.
Feb 29, 2012:
- 2:03 PM Changeset [1797] by
- implemented brian's changes
- 11:49 AM Changeset [1796] by
- Cast removal is also an endo-transformation.
Feb 28, 2012:
- 6:11 PM Changeset [1795] by
- Final version, waiting for comments.
- 6:07 PM Changeset [1794] by
- Added cpp paper as an addendum to the report
- 5:57 PM Changeset [1793] by
- …
- 5:56 PM Changeset [1792] by
- …
- 5:01 PM Changeset [1791] by
- cleaning up
- 4:35 PM Changeset [1790] by
- edited the report so that all the spelling is consistent (british …
- 4:25 PM Changeset [1789] by
- …
- 11:32 AM Changeset [1788] by
- small modifications
- 10:57 AM Changeset [1787] by
- New proposal.
Feb 27, 2012:
- 6:40 PM Changeset [1786] by
- …
- 5:55 PM Changeset [1785] by
- finished ERTL to LTL sketch
- 5:55 PM Changeset [1784] by
- Start on proof of existence of nonterminating RTLabs structured traces.
- 5:55 PM Changeset [1783] by
- Remove junk from non-terminating structured traces.
- 5:55 PM Changeset [1782] by
- Correct bad inversion.
- 5:55 PM Changeset [1781] by
- Reinstated the lstlisting style
- 5:45 PM Changeset [1780] by
- finished rtl to ertl
- 5:11 PM Changeset [1779] by
- …
- 5:09 PM Changeset [1778] by
- …
- 5:01 PM Changeset [1777] by
- …
- 4:53 PM Changeset [1776] by
- …
- 4:11 PM Changeset [1775] by
- …
- 4:08 PM Changeset [1774] by
- …
- 3:53 PM Changeset [1773] by
- …
- 3:46 PM Changeset [1772] by
- …
- 3:44 PM Changeset [1771] by
- some typos fixed, commit mostly to avoid conflicts
- 2:57 PM Changeset [1770] by
- …
- 2:52 PM Changeset [1769] by
- ..
- 2:46 PM Changeset [1768] by
- …
- 2:45 PM Changeset [1767] by
- …
- 2:19 PM Changeset [1766] by
- avoid conflicts
- 2:16 PM Changeset [1765] by
- Rule out final states in non-terminating executions chunks (RTLabs …
- 2:16 PM Changeset [1764] by
- Terminating function preserve the property that the execution does not …
- 1:52 PM Changeset [1763] by
- to avoid conflicts
- 1:51 PM Changeset [1762] by
- Changes and fixes.
- 11:31 AM Changeset [1761] by
- …
- 11:01 AM Changeset [1760] by
- avoiding conflicts
- 10:02 AM Changeset [1759] by
- Tentative agenda.
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
Note: See TracTimeline
for information about the timeline view.
