Timeline
Jun 4, 2012:
- 5:38 PM Changeset [2017] by
- Large swathes of proof of main lemma added.
- 4:13 PM Changeset [2016] by
- Slight change in simplification strategy to better match the semantics
- 4:06 PM Changeset [2015] by
- Changes following a conversation with Jaap: as it stands computation …
Jun 2, 2012:
- 10:39 PM Changeset [2014] by
- Fixed problem in James' email message.
- 12:11 AM Changeset [2013] by
- Put in HiPEAC 2013
Jun 1, 2012:
- 11:49 PM Changeset [2012] by
- Added proposed papers to D6.2
May 31, 2012:
- 4:41 PM Changeset [2011] by
- Minor cleanup.
- 3:10 PM Changeset [2010] by
- Make globalenvs use proper maps.
May 30, 2012:
- 9:34 PM Changeset [2009] by
- Proof of simulation completed for singe-step executions.
- 7:22 PM Changeset [2008] by
- - substantial closing of holes in proof
- 6:55 PM Changeset [2007] by
- Potential workshop invitees
- 6:43 PM Changeset [2006] by
- - added alias for bitvector zero - changed extralib bounded …
May 29, 2012:
- 2:51 PM Changeset [2005] by
- - minor changes to make things compile with a clean checkout
May 28, 2012:
- 2:35 PM Changeset [2004] by
- Minor edits from discussion.
- 1:10 PM Changeset [2003] by
- Some discussion of correctness statements.
May 26, 2012:
- 4:15 PM Changeset [2002] by
- Supplement to D6.2
May 25, 2012:
- 1:47 PM Changeset [2001] by
- Get the compiler to output more.
- 11:01 AM Changeset [2000] by
- Fix g.e. glitch in label simulation.
- 10:45 AM Changeset [1999] by
- Make back-end use the main global envs.
- 10:18 AM Changeset [1998] by
- Version number bumped.
- 10:05 AM Changeset [1997] by
- Changed titles of reports to match correct deliverable title
- 9:18 AM Changeset [1996] by
- Work on correctness from yesterday.
May 24, 2012:
- 7:18 PM Changeset [1995] by
- Overall compiler definition; bits and pieces to make everything happy(ish).
- 6:08 PM Changeset [1994] by
- Remove redundant allocation definition in Globalenvs.
- 5:10 PM Changeset [1993] by
- Make front-end memory model only depend on the general definitions by …
- 4:26 PM Changeset [1992] by
- Ayache?
- 4:24 PM Changeset [1991] by
- Put the front end transformations together and make an example use it.
- 4:24 PM Changeset [1990] by
- the LUSTRE paper has not yet appeared what about the Ayache/Frama?-C …
- 4:16 PM Changeset [1989] by
- Notes of 2012-05-24 of the UEdin/UniBo meeting to discuss publication …
- 11:39 AM Changeset [1988] by
- Abstraction of the memory contents in the memory models is no longer …
- 10:22 AM Changeset [1987] by
- Move BEValues to common to reflect their use in the memory model for …
- 9:35 AM Changeset [1986] by
- Get rid of unused abstraction of Globalenvs.
May 22, 2012:
- 6:12 PM Changeset [1985] by
- A single `false' case for unconditional jumps completed.
- 5:37 PM Changeset [1984] by
- Most proof obligations closed in main_lemma apart from those of the …
- 11:15 AM Changeset [1983] by
- Changes to simplify the simpler cases of the main_lemma.
- 8:14 AM Changeset [1982] by
- add 2.1 Survey
- 8:13 AM Changeset [1981] by
- update 5.1
- 8:12 AM Changeset [1980] by
- update 5.1
- 12:57 AM Changeset [1979] by
- Very very very tricky lemma closed. A dreadful mix of JM equality …
- 12:37 AM Changeset [1978] by
- Two more cases completed.
- 12:05 AM Changeset [1977] by
- Unblocked: let ... as hides two different terms, one that uses Leibniz …
May 21, 2012:
- 7:04 PM Changeset [1976] by
- * monads: just changed some defs, which had to be propagated in some …
- 5:48 PM Changeset [1975] by
- Work from today on closing main_thm.
- 5:03 PM Changeset [1974] by
- Progress on the cast simplification proof.
- 4:57 PM Changeset [1973] by
- - removed superfluous match - displaced 'cases daemon'
- 10:33 AM Changeset [1972] by
- Simple lemma with strangely complex proof complete.
May 20, 2012:
- 10:34 PM Changeset [1971] by
- 1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
May 18, 2012:
- 9:18 PM Changeset [1970] by
- Work-in-progress: correction proof for the cast removal on expressions.
- 6:14 PM Changeset [1969] by
- Some more progress, but now we must prove something on a Russell …
- 12:08 PM Changeset [1968] by
- Update D4.3's title, memory model details, and some typographical …
- 11:48 AM Changeset [1967] by
- Mov case completed.
May 17, 2012:
- 5:45 PM Changeset [1966] by
- Progress made on main_thm proof: trying to find a pattern to use …
- 12:42 PM Changeset [1965] by
- - further completed proof, changed jump_expansion' to reflect new type …
- 12:06 PM Changeset [1964] by
- introduced as_label_of_cost and adapted accordingly. Equality of cost …
- 2:23 AM Changeset [1963] by
- More progress in restoring the original proof.
- 12:25 AM Changeset [1962] by
- More examples are now indexed.
May 16, 2012:
- 9:12 PM Changeset [1961] by
- No more interaction required.
- 5:24 PM Changeset [1960] by
- Update RTLabs structured traces to make minor changes in definitions.
- 5:12 PM Changeset [1959] by
- Commented out diverging application of demodulation and closed goals …
- 4:47 PM Changeset [1958] by
- Marked divergence in StatusProofs?.ma
- 3:53 PM Changeset [1957] by
- Stitching proofs back together after slight change in statement of …
- 3:10 PM Changeset [1956] by
- - finished proof of lemma (where auto does strange things again)
- 3:03 PM Changeset [1955] by
- Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
- 2:44 PM Changeset [1954] by
- Initial state is in the labelling simulation (modulo global envs results).
- 10:29 AM Changeset [1953] by
- Commit to avoid conflicts.
- 1:29 AM Changeset [1952] by
- AssemblyProof? splitted.
- 1:28 AM Changeset [1951] by
- Bug with overloaded names in the context.
May 15, 2012:
- 6:20 PM Changeset [1950] by
- - advances in policy
- 5:51 PM Changeset [1949] by
- * lemma trace rel to eq flatten trace * some more properties of …
- 11:13 AM Changeset [1948] by
- Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
- 12:30 AM Changeset [1947] by
- Failure of automation/demod investigated a little bit.
- 12:01 AM Changeset [1946] by
- \snd half_add => add everywhere
May 14, 2012:
- 10:40 PM Changeset [1945] by
- All proof statements repaired.
- 7:56 PM Changeset [1944] by
- common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
- 6:45 PM Changeset [1943] by
- - changed 'labels okay' part of create_label_cost_map
- 6:02 PM Changeset [1942] by
- Work on showing the equivalence of two methods of looking up from the maps.
- 4:33 PM Changeset [1941] by
- Changes to the AssemblyProof? with a few more (large) axioms closed.
- 4:05 PM Changeset [1940] by
- - committed new version of final invariant
- 10:37 AM Changeset [1939] by
- Changes to get things to compile and to avoid the dependency …
- 10:05 AM Changeset [1938] by
- Definitions moved to the right places, now everything compiles again.
May 11, 2012:
- 3:06 PM Changeset [1937] by
- - filled in some of the gaps in the proof of Policy - reverted …
- 2:38 PM Changeset [1936] by
- Some holes filled in AssemblyProof?.ma.
- 1:39 PM WikiStart edited by
- (diff)
May 10, 2012:
- 5:13 PM Changeset [1935] by
- Generalized some lemma in ASM/CostsProof.ma to work on abstract …
- 3:37 PM Changeset [1934] by
- - various & sundry moves of lemmas to better places - integrated …
- 12:00 PM Changeset [1933] by
- - slight revamp
- 10:35 AM Changeset [1932] by
- - added some more dependent types (we love 'em)
May 9, 2012:
- 7:23 PM Changeset [1931] by
- - added latest bvt alias - temporary "cases daemon" commit of new …
- 6:30 PM Changeset [1930] by
- Tidy up labelling simulation stuff a bit.
- 2:44 PM Changeset [1929] by
- Simplified proof by removing most of the invariants on the statements …
- 1:36 PM Changeset [1928] by
- Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should …
- 1:05 PM Changeset [1927] by
- Reduced complexity of good_program predicate, ported to new notion of …
May 8, 2012:
- 6:09 PM Changeset [1926] by
- * added as_label to abstract status, with as_costed defined with it. …
- 6:08 PM Changeset [1925] by
- - re-added jump_lenggh
- 6:04 PM Changeset [1924] by
- Added comment
- 3:43 PM Changeset [1923] by
- Small change, closing daemon that went under the RADAR
- 3:41 PM Changeset [1922] by
- Main labelling simulation proof complete.
- 3:29 PM Changeset [1921] by
- Horror proof mostly finished (compiles all way until end of CostsProof?.ma).
- 11:16 AM Changeset [1920] by
- Most of the labelling simulation. Still need to sort out switch …
May 7, 2012:
- 11:12 AM Changeset [1919] by
- Fixes to get everything compiling again
Note: See TracTimeline
for information about the timeline view.
