Timeline
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 …
Jan 19, 2012:
- 4:56 PM Changeset [1650] by
- changes over the last couple of days: stuck due to matita producing …
Jan 18, 2012:
- 6:17 PM Changeset [1649] by
- - changes to Assembly for integration with Policy and easier use of …
- 11:01 AM Changeset [1648] by
- new version of utilities/monad.ma with typecheck command comented out
Jan 17, 2012:
- 1:13 PM Changeset [1647] by
- * corrected some notation problems * adapted Cligth with slight …
Jan 16, 2012:
- 3:04 PM Changeset [1646] by
- finished the block_costs computation, and propagated the changes …
Jan 13, 2012:
- 6:11 PM Changeset [1645] by
- more progress on the ASMCosts work: block_costs is now complete …
- 3:08 PM Changeset [1644] by
- minor changes
- 12:23 PM Changeset [1643] by
- * some changes in everything * separated extensions in sequential and …
Jan 12, 2012:
- 6:16 PM Changeset [1642] by
- finished big proof in all but two cases
Jan 11, 2012:
- 8:03 PM Changeset [1641] by
- * semanticsUtils_paolo.ma contains code to generate both graph and …
- 5:41 PM Changeset [1640] by
- * finished fork of semantics.ma * unification of Errors under the …
Jan 10, 2012:
- 5:27 PM Changeset [1639] by
- changes from today
- 4:31 PM Changeset [1638] by
- Tidy up RTLabs structured traces code a little.
- 11:26 AM Changeset [1637] by
- RTLabs structured traces: Add a termination measure to satisfy …
Note: See TracTimeline
for information about the timeline view.