Timeline


and

Feb 16, 2012:

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

Feb 15, 2012:

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

Feb 14, 2012:

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

Feb 13, 2012:

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

Feb 10, 2012:

2:12 PM Changeset [1687] by tranquil
corrected title

Feb 9, 2012:

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

Feb 7, 2012:

6:01 PM Changeset [1679] by ayache
Frama-C plug-in (sources+documentation)
4:36 PM Changeset [1678] by mulligan
finished editing the english in the report
12:23 PM Changeset [1677] by mulligan
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 tranquil
corrected some faults still TODO: running example, language corrections
3:33 PM Changeset [1675] by campbell
Some work on sound labelled for RTLabs.
12:32 PM Changeset [1674] by tranquil
corrected some faults still TODO: running example, language corrections

Feb 4, 2012:

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

Feb 1, 2012:

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

Jan 30, 2012:

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

Jan 29, 2012:

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

Jan 28, 2012:

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

Jan 27, 2012:

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

Jan 26, 2012:

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

Jan 25, 2012:

6:18 PM Changeset [1658] by mulligan
asm costs changes from today
5:40 PM Changeset [1657] by amadio
preliminary version of D5

Jan 23, 2012:

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

Jan 19, 2012:

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

Jan 18, 2012:

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

Jan 17, 2012:

1:13 PM Changeset [1647] by tranquil
* corrected some notation problems * adapted Cligth with slight …
Note: See TracTimeline for information about the timeline view.