Timeline
Jun 21, 2012:
- 5:21 PM Changeset [2106] by
- Fix up a couple of proofs broken by recent changes.
- 5:21 PM Changeset [2105] by
- Show some results about globalenvs and program transformations.
- 5:21 PM Changeset [2104] by
- Fill in misc axiom.
- 5:21 PM Changeset [2103] by
- Make transform_*program take a more general transformation to make …
Jun 20, 2012:
- 4:51 PM Changeset [2102] by
- - some small changes
Jun 19, 2012:
- 4:43 PM Changeset [2101] by
- - renamed medium to absolute jump - revised proofs of policy, some …
Jun 18, 2012:
- 5:16 PM Changeset [2100] by
- temporary solution to a bug where operations on spilled registers …
- 2:07 PM WikiStart edited by
- (diff)
- 2:02 PM WikiStart edited by
- (diff)
- 2:00 PM WikiStart edited by
- (diff)
Jun 15, 2012:
- 5:56 PM Changeset [2099] by
- - added reference to Intel dev manual
- 5:29 PM Changeset [2098] by
- - updates & changes
- 3:25 PM Changeset [2097] by
- Consistency change (institution)
- 3:25 PM Changeset [2096] by
- Changes to the English for Jaap, and some tidying up and making …
- 1:58 PM Changeset [2095] by
- Added reference to CompCert? and CompCertTSO.
- 1:56 PM Changeset [2094] by
- - oops
- 1:55 PM Changeset [2093] by
- - added reference to CompCertTSO
- 1:38 PM Changeset [2092] by
- Jaap noticed it's Randall Hyde not Holmes.
- 1:35 PM Changeset [2091] by
- - systematically changed 'jump' to 'branch'
- 12:57 PM Changeset [2090] by
- Fixed mistaken reference to RISC instead of CISC architectures.
- 11:54 AM Changeset [2089] by
- Harmonised institution name to that used by Jaap
- 11:52 AM Changeset [2088] by
- Added list of keywords as is required. Other minor changes.
- 11:40 AM Changeset [2087] by
- Tidied up the paper, added a few more things, tidied and expanded …
- 11:39 AM Changeset [2086] by
- - spell-check
- 11:36 AM Changeset [2085] by
- - rewrote introduction - changed 'medium' to 'absolute' - added a bit …
- 1:17 AM Changeset [2084] by
- - changed bibliography style - added CerCo? thanks - some words of …
Jun 14, 2012:
- 5:32 PM Changeset [2083] by
- More work on paper from today.
- 4:26 PM Changeset [2082] by
- - reworked and extended presentation of invariants
- 12:04 PM Changeset [2081] by
- Type of assembly fixed to be compatible with the old one and to take …
- 11:57 AM Changeset [2080] by
- - added references to SDCC and gcc (thanks, Dominic) - updated sigma …
- 11:45 AM Changeset [2079] by
- sigma_policy_specification restyled
- 11:44 AM Changeset [2078] by
- sigma_policy_specification has been 1) strengthened 2) made nicer to …
- 10:45 AM Changeset [2077] by
- - committed actual file instead of link
- 10:30 AM Changeset [2076] by
- First steps towards a simulation proof for switch removal.
- 10:25 AM Changeset [2075] by
- Solved conflict in AssemblyProof?
- 10:23 AM Changeset [2074] by
- Prophylactic renaming of a relation
- 4:10 AM Changeset [2073] by
- All false daemons removed.
- 4:03 AM Changeset [2072] by
- We need to import Jaap's invariants now.
- 3:25 AM Changeset [2071] by
- More daemons closed, but one is suspect now.
- 2:18 AM Changeset [2070] by
- More daemons closed.
Jun 13, 2012:
- 7:58 PM Changeset [2069] by
- …
- 7:54 PM Changeset [2068] by
- …
- 7:50 PM Changeset [2067] by
- …
- 6:46 PM Changeset [2066] by
- Finished for the day.
- 5:54 PM Changeset [2065] by
- - committed another draft
- 5:29 PM Changeset [2064] by
- - more progress
- 5:05 PM Changeset [2063] by
- Minor fixes
- 5:00 PM Changeset [2062] by
- Everything repaired (broken because of new proof obligation for fetch).
- 4:59 PM Changeset [2061] by
- Added Randall Holmes' Usenet post on branch displacement optimisation …
- 4:26 PM Changeset [2060] by
- More work on paper.
- 3:44 PM Changeset [2059] by
- - updated Policy to work better
- 3:17 PM Changeset [2058] by
- First draft of changes to main sections (i.e. those describing the …
- 1:30 PM Changeset [2057] by
- Repaired (was broken by fetch_pseudo_instruction now taking a proof …
- 1:01 PM Changeset [2056] by
- Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
- 12:11 PM Changeset [2055] by
- Warning: this commit adds an hypothesis that breaks all of assembly stuff.
- 11:58 AM Changeset [2054] by
- - progress
- 11:02 AM Changeset [2053] by
- Introduction changed, with many paragraphs deleted.
- 10:04 AM Changeset [2052] by
- Initial commit of proposed CPP 2012 paper on the proof of correctness …
Jun 12, 2012:
- 5:49 PM Changeset [2051] by
- Finished the Jmp case in the main theorem.
- 4:01 PM Changeset [2050] by
- Limit some normalization that doesn't seem to like.
- 3:49 PM Changeset [2049] by
- - progress
- 2:46 PM Changeset [2048] by
- - factorised jump decisions
- 2:18 PM Changeset [2047] by
- Big bugs in policy calculations found. Waiting for Jaap's commit.
- 1:36 PM Changeset [2046] by
- - removed old paper directory
- 1:35 PM Changeset [2045] by
- - renamed paper directory
- 10:52 AM Changeset [2044] by
- PCs for RTLabs structured traces.
Jun 8, 2012:
- 11:41 PM Changeset [2043] by
- Broken code commented out.
- 11:33 PM Changeset [2042] by
- Repaired (Type => DeqSet?)
- 11:21 PM Changeset [2041] by
- Repaired: unified syntax for monads.
- 7:38 PM Changeset [2040] by
- Repaired using new /demod/ that allows to specify the rules to be used.
- 6:20 PM Changeset [2039] by
- New, better interface for subaddressing_mode_elim
- 6:17 PM Changeset [2038] by
- split => vsplit
- 5:56 PM Changeset [2037] by
- flatten is now part of stdlib
- 5:52 PM Changeset [2036] by
- New daemon inserted because /demod/ got worst :-(
- 5:51 PM Changeset [2035] by
- Fixed
- 5:16 PM Changeset [2034] by
- - split Policy into three separate files for ease (and indeed …
- 4:57 PM Changeset [2033] by
- Daemon reverted.
- 4:32 PM Changeset [2032] by
- !! BEWARE: major commit !! 1) [affects everybody] split for …
- 3:52 PM Changeset [2031] by
- Mention FMICS 2012 paper
- 1:44 PM Changeset [2030] by
- Cast simplification was too conservative, now reasonably aggressive.
Jun 7, 2012:
- 6:30 PM Changeset [2029] by
- Mild revision of invitee list; commitment to HiPEAC
- 5:58 PM Changeset [2028] by
- - bugfix to Assembly (forgotten sigma) - added …
- 5:53 PM Changeset [2027] by
- Got the main lemma to apply in the proof of main theorem again and …
- 4:37 PM Changeset [2026] by
- Added a new file to house the main theorem as the type checking time …
- 3:51 PM Changeset [2025] by
- Silly typo and old comment.
- 3:20 PM Changeset [2024] by
- Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
- 2:08 PM Changeset [2023] by
- Closed main lemma modulo closing trivial subgoals about commutations …
- 10:47 AM Changeset [2022] by
- - corrected jump calculation algorithm
- 1:44 AM Changeset [2021] by
- Proof skeleton in place. Several daemons to be closed adding invariants.
Jun 6, 2012:
- 6:27 PM Changeset [2020] by
- CJNE case complete, DJNZ case almost complete
- 6:24 PM Changeset [2019] by
- Split out special induction principle for Clight from soundness file. …
Jun 5, 2012:
- 5:49 PM Changeset [2018] by
- CJNE case a complete mess.
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 …
Note: See TracTimeline
for information about the timeline view.
