Context Navigation

Timeline

18:05 Changeset [1707] by campbell: Progress on finite segments of infinite RTLabs structured trace.
18:05 Changeset [1706] by campbell: Checkpoint RTLabs structured traces.
18:05 Changeset [1705] by campbell: Checkpoint RTLabs labelling soundness work.
17:15 D5.1-5.3.pdf attached to WikiStart by mulligan: Report for D5.1-5.3
16:54 Changeset [1704] by amadio: typo
11:55 src20111020.tgz attached to WikiStart by mulligan: Matita snapshot for typechecking recent deliverables
11:54 D3-3.pdf attached to WikiStart by mulligan: Deliverable for D3.3
11:54 D3-2.pdf attached to WikiStart by mulligan: Deliverable for D3.2
11:48 D5.1-5.3.tar.gz attached to WikiStart by mulligan: Deliverable for D5.1-5.3
11:41 WikiStart edited by mulligan: change of title for wilmer (diff)
11:36 Changeset [1703] by tranquil: minimal change
11:35 Changeset [1702] by tranquil: updated the report and changed a bit the names
11:25 Changeset [1701] by tranquil: added updated compiler tarball
11:23 Changeset [1700] by tranquil: updated README
11:22 Changeset [1699] by amadio: 5.1 up
11:05 Changeset [1698] by tranquil: minor modifications

18:02 Changeset [1697] by mulligan: important bug found
16:09 Changeset [1696] by mulligan: finished adding russell types to the traverse_cost_* functions
14:10 Changeset [1695] by mulligan: Progress on CostsProof?.ma file.
09:30 Changeset [1694] by tranquil: indexed labels branch

16:38 Changeset [1693] by mulligan: Changes to ASMCosts and CostsProofs? files to get everything working again.
13:18 Changeset [1692] by mulligan: resolved conflict in asm costs this morning
01:43 Changeset [1691] by sacerdot: Some progress in the proof: less daemons, less hypotheses in lemmas.

15:58 Changeset [1690] by tranquil: nested loops are not supported yet, the only test had one
15:54 Changeset [1689] by tranquil: kept out the wrapper (which I did not touch, so not sure it works)
09:08 Changeset [1688] by amadio: up d5.1-5.3

18:16 Changeset [1686] by tranquil: corrected abstract
18:08 Changeset [1685] by tranquil: adjusted comparison with aiT
17:42 Changeset [1684] by mulligan: changes from the past week
17:41 Changeset [1683] by tranquil: abstract and running example
13:22 Changeset [1682] by campbell: Complete proof for as_after_return for RTLabs.
13:22 Changeset [1681] by campbell: Checkpoint of stack preservation work in RTLabs.
13:22 Changeset [1680] by campbell: Comment out unused tailcalls in Cminor and RTLabs. (They would be a little …

18:01 Changeset [1679] by ayache: Frama-C plug-in (sources+documentation)
16:36 Changeset [1678] by mulligan: finished editing the english in the report
12:23 Changeset [1677] by mulligan: changes to paolo's english in the report, about a 1/4 of the way through

18:50 Changeset [1676] by tranquil: corrected some faults still TODO: running example, language corrections
15:33 Changeset [1675] by campbell: Some work on sound labelled for RTLabs.
12:32 Changeset [1674] by tranquil: corrected some faults still TODO: running example, language corrections

11:58 Changeset [1673] by tranquil: report on indexed labels TODO: corrections, examples, etc

16:16 Changeset [1672] by campbell: Matita now generates a couple of inversion lemmas that were manually …
16:16 Changeset [1671] by campbell: A little more on RTLabs infinite traces.
16:16 Changeset [1670] by campbell: Snapshot of non-terminating RTLabs structured traces work.
15:36 Changeset [1669] by mulligan: Commit for claudio

11:41 Changeset [1668] by boender: - split build_maps into build_maps and build_maps_ok - work with CSC on …

22:25 Changeset [1667] by sacerdot: Main lemma for the main_thm of AssemblyProof? re-declared as an axiom in …

13:42 Changeset [1666] by sacerdot: PreStatus? datatype change: the code_memory field is not a left parameter. …

17:05 Changeset [1665] by mulligan: progress on closing holes in block_cost' proof
00:11 Changeset [1664] by tranquil: corrected a bug in loop peeling where continue and breaks were not handled …

17:40 Changeset [1663] by mulligan: old cases working again, work on new ones
10:06 Changeset [1662] by amadio: rev
10:04 Changeset [1661] by amadio: rev
08:58 Changeset [1660] by ayache: Deliverable: Frama-C plug-in (D5.1-5.3)
08:43 Changeset [1659] by amadio

19:01 Changeset [1656] by campbell: Minor fixups to RTLabs/Traces due to syntax changes.
18:31 Changeset [1655] by campbell: Update Cminor and RTLabs semantics to use new monad definitions.
17:37 Changeset [1654] by campbell: Corrections to structured trace definitions (see the mailing list). Also …
17:37 Changeset [1653] by campbell: Start on building finite sections of non-terminating structured traces.
17:37 Changeset [1652] by campbell: Forgot to apply 1583 to non-terminating case.
17:37 Changeset [1651] by campbell: Start looking at non-terminating structured traces by defining soundness …

16:56 Changeset [1650] by mulligan: changes over the last couple of days: stuck due to matita producing terms …

18:17 Changeset [1649] by boender: - changes to Assembly for integration with Policy and easier use of _safe …
11:01 Changeset [1648] by mulligan: new version of utilities/monad.ma with typecheck command comented out

13:13 Changeset [1647] by tranquil: * corrected some notation problems * adapted Cligth with slight …

Note: See TracTimeline for information about the timeline view.