Timeline



May 24, 2012:

7:18 PM Changeset [1995] by campbell
Overall compiler definition; bits and pieces to make everything happy(ish).
6:08 PM Changeset [1994] by campbell
Remove redundant allocation definition in Globalenvs.
5:10 PM Changeset [1993] by campbell
Make front-end memory model only depend on the general definitions by …
4:26 PM Changeset [1992] by mckinna
Ayache?
4:24 PM Changeset [1991] by campbell
Put the front end transformations together and make an example use it.
4:24 PM Changeset [1990] by mckinna
the LUSTRE paper has not yet appeared what about the Ayache/Frama?-C …
4:16 PM Changeset [1989] by mckinna
Notes of 2012-05-24 of the UEdin/UniBo meeting to discuss publication …
11:39 AM Changeset [1988] by campbell
Abstraction of the memory contents in the memory models is no longer …
10:22 AM Changeset [1987] by campbell
Move BEValues to common to reflect their use in the memory model for …
9:35 AM Changeset [1986] by campbell
Get rid of unused abstraction of Globalenvs.

May 22, 2012:

6:12 PM Changeset [1985] by mulligan
A single `false' case for unconditional jumps completed.
5:37 PM Changeset [1984] by mulligan
Most proof obligations closed in main_lemma apart from those of the …
11:15 AM Changeset [1983] by mulligan
Changes to simplify the simpler cases of the main_lemma.
8:14 AM Changeset [1982] by amadio
add 2.1 Survey
8:13 AM Changeset [1981] by amadio
update 5.1
8:12 AM Changeset [1980] by amadio
update 5.1
12:57 AM Changeset [1979] by sacerdot
Very very very tricky lemma closed. A dreadful mix of JM equality …
12:37 AM Changeset [1978] by sacerdot
Two more cases completed.
12:05 AM Changeset [1977] by sacerdot
Unblocked: let ... as hides two different terms, one that uses Leibniz …

May 21, 2012:

7:04 PM Changeset [1976] by tranquil
* monads: just changed some defs, which had to be propagated in some …
5:48 PM Changeset [1975] by mulligan
Work from today on closing main_thm.
5:03 PM Changeset [1974] by garnier
Progress on the cast simplification proof.
4:57 PM Changeset [1973] by boender
- removed superfluous match - displaced 'cases daemon'
10:33 AM Changeset [1972] by mulligan
Simple lemma with strangely complex proof complete.

May 20, 2012:

10:34 PM Changeset [1971] by sacerdot
1. Interpret.ma: we need to prove \sigma (execute_preinstruction …

May 18, 2012:

9:18 PM Changeset [1970] by garnier
Work-in-progress: correction proof for the cast removal on expressions.
6:14 PM Changeset [1969] by sacerdot
Some more progress, but now we must prove something on a Russell …
12:08 PM Changeset [1968] by campbell
Update D4.3's title, memory model details, and some typographical …
11:48 AM Changeset [1967] by sacerdot
Mov case completed.

May 17, 2012:

5:45 PM Changeset [1966] by mulligan
Progress made on main_thm proof: trying to find a pattern to use …
12:42 PM Changeset [1965] by boender
- further completed proof, changed jump_expansion' to reflect new type …
12:06 PM Changeset [1964] by tranquil
introduced as_label_of_cost and adapted accordingly. Equality of cost …
2:23 AM Changeset [1963] by sacerdot
More progress in restoring the original proof.
12:25 AM Changeset [1962] by sacerdot
More examples are now indexed.

May 16, 2012:

9:12 PM Changeset [1961] by sacerdot
No more interaction required.
5:24 PM Changeset [1960] by campbell
Update RTLabs structured traces to make minor changes in definitions.
5:12 PM Changeset [1959] by mulligan
Commented out diverging application of demodulation and closed goals …
4:47 PM Changeset [1958] by mulligan
Marked divergence in StatusProofs?.ma
3:53 PM Changeset [1957] by mulligan
Stitching proofs back together after slight change in statement of …
3:10 PM Changeset [1956] by boender
- finished proof of lemma (where auto does strange things again)
3:03 PM Changeset [1955] by mulligan
Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
2:44 PM Changeset [1954] by campbell
Initial state is in the labelling simulation (modulo global envs results).
10:29 AM Changeset [1953] by mulligan
Commit to avoid conflicts.
1:29 AM Changeset [1952] by sacerdot
AssemblyProof? splitted.
1:28 AM Changeset [1951] by sacerdot
Bug with overloaded names in the context.

May 15, 2012:

6:20 PM Changeset [1950] by boender
- advances in policy
5:51 PM Changeset [1949] by tranquil
* lemma trace rel to eq flatten trace * some more properties of …
11:13 AM Changeset [1948] by mulligan
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
12:30 AM Changeset [1947] by sacerdot
Failure of automation/demod investigated a little bit.
12:01 AM Changeset [1946] by sacerdot
\snd half_add => add everywhere

May 14, 2012:

10:40 PM Changeset [1945] by sacerdot
All proof statements repaired.
7:56 PM Changeset [1944] by sacerdot
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
6:45 PM Changeset [1943] by boender
- changed 'labels okay' part of create_label_cost_map
6:02 PM Changeset [1942] by mulligan
Work on showing the equivalence of two methods of looking up from the maps.
4:33 PM Changeset [1941] by mulligan
Changes to the AssemblyProof? with a few more (large) axioms closed.
4:05 PM Changeset [1940] by boender
- committed new version of final invariant
10:37 AM Changeset [1939] by mulligan
Changes to get things to compile and to avoid the dependency …
10:05 AM Changeset [1938] by sacerdot
Definitions moved to the right places, now everything compiles again.

May 11, 2012:

3:06 PM Changeset [1937] by boender
- filled in some of the gaps in the proof of Policy - reverted …
2:38 PM Changeset [1936] by mulligan
Some holes filled in AssemblyProof?.ma.
1:39 PM WikiStart edited by mulligan
(diff)

May 10, 2012:

5:13 PM Changeset [1935] by mulligan
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
3:37 PM Changeset [1934] by boender
- various & sundry moves of lemmas to better places - integrated …
12:00 PM Changeset [1933] by boender
- slight revamp
10:35 AM Changeset [1932] by boender
- added some more dependent types (we love 'em)

May 9, 2012:

7:23 PM Changeset [1931] by boender
- added latest bvt alias - temporary "cases daemon" commit of new …
6:30 PM Changeset [1930] by campbell
Tidy up labelling simulation stuff a bit.
2:44 PM Changeset [1929] by mulligan
Simplified proof by removing most of the invariants on the statements …
1:36 PM Changeset [1928] by mulligan
Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
1:05 PM Changeset [1927] by mulligan
Reduced complexity of good_program predicate, ported to new notion of …

May 8, 2012:

6:09 PM Changeset [1926] by tranquil
* added as_label to abstract status, with as_costed defined with it. …
6:08 PM Changeset [1925] by boender
- re-added jump_lenggh
6:04 PM Changeset [1924] by mulligan
Added comment
3:43 PM Changeset [1923] by mulligan
Small change, closing daemon that went under the RADAR
3:41 PM Changeset [1922] by campbell
Main labelling simulation proof complete.
3:29 PM Changeset [1921] by mulligan
Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
11:16 AM Changeset [1920] by campbell
Most of the labelling simulation. Still need to sort out switch …

May 7, 2012:

11:12 AM Changeset [1919] by mulligan
Fixes to get everything compiling again

May 4, 2012:

3:40 PM Changeset [1918] by tranquil
using listb.ma now
2:21 PM Changeset [1917] by tranquil
predicate for unrepeating traces, fused final_abstract_status with …
1:59 PM Changeset [1916] by mulligan
Closed remaining daemons in block_cost'. Rest of file now typechecks …

May 3, 2012:

7:13 PM Changeset [1915] by garnier
Correction of a typo in switchRemoval.
5:53 PM Changeset [1914] by campbell
Fix bug in Clight semantics that misses goto-labels inside a cost …
4:20 PM Changeset [1913] by mulligan
Got the rest of the file to typecheck as before.
4:11 PM Changeset [1912] by mulligan
Patches to get block_cost' and dependencies working again after change …

Apr 27, 2012:

6:45 PM Changeset [1911] by mulligan
Changed statement of block_cost' to start on new termination argument
5:48 PM Changeset [1910] by mulligan
Finished proof modulo termination argument
10:59 AM Changeset [1909] by mulligan
Ported new statements to remainder of Interpret.ma file.

Apr 26, 2012:

5:38 PM Changeset [1908] by fguidi
notation fixup following last commit of matita we shifted the levels …
5:37 PM Changeset [1907] by mulligan
Fixes to get file to compile
5:20 PM Changeset [1906] by mulligan
Statements simplified in block_cost and dependencies
5:15 PM Changeset [1905] by boender
- plugging gap in assembly proof
5:03 PM Changeset [1904] by mulligan
Problem with proof fixed by noting that problem is actually irrelevant
4:49 PM Changeset [1903] by mulligan
Small changes prior to experiment
4:20 PM Changeset [1902] by mulligan
Reverted needless changes to StructuredTraces?
3:35 PM Changeset [1901] by mulligan
Slight changes to StructuredTraces?: should not change too much
Note: See TracTimeline for information about the timeline view.