Commits · 773f2a803f5e7ba2d3b305432dc44f7da4ac1d1f · AVA / FloVer · GitLab

02 Sep, 2016 2 commits
- Prove validation theorems for params and constants, start working on bound for addition · 773f2a80
  Heiko Becker authored Sep 02, 2016
  
  773f2a80
- Make split stronger, resp. behave like the coq split · 441bd264
  Heiko Becker authored Sep 02, 2016
  
  441bd264
29 Aug, 2016 2 commits
- Fix bug in IV Arith and prove nearly full IV checker · f0a320f9
  Heiko Becker authored Aug 29, 2016
  
  f0a320f9
- Progress on validation of IVs in HOL Light · 5a981682
  Heiko Becker authored Aug 29, 2016
  
  5a981682
26 Aug, 2016 5 commits
- Type in doc fixing and add lemma existential_rewriting to HOL dev, without proof · 10c11261
  Heiko Becker authored Aug 26, 2016
  
  10c11261
- Make eval_0_det proper proof in HOL-Light style and simplify coq dev · c42a6ab3
  Heiko Becker authored Aug 26, 2016
  
  c42a6ab3
- Move machineEpsilon to Infra.RealSimps · 692353f0
  Heiko Becker authored Aug 26, 2016
  
  692353f0
- Prove subtraction error bound · 8883bb13
  Heiko Becker authored Aug 26, 2016
  
  8883bb13
- Prove addition error bound in HOL · e7378eba
  Heiko Becker authored Aug 26, 2016
  
  e7378eba
25 Aug, 2016 4 commits
- Remove unused search term · 7ab5c59a
  Heiko Becker authored Aug 25, 2016
  
  7ab5c59a
- More work on bound proofs · 0c434c2b
  Heiko Becker authored Aug 25, 2016
  
  0c434c2b
- Finish IntervalArithmetic and start proving Errorbounds · 000ccc7c
  Heiko Becker authored Aug 25, 2016
  
  000ccc7c
- Prove interval multiplication in HOL correct · 354c9cfb
  Heiko Becker authored Aug 25, 2016
  
  354c9cfb
24 Aug, 2016 4 commits
- Prove necessary lemma to get multiplication in structure similar to Coq, start working on proof · f464b139
  Heiko Becker authored Aug 24, 2016
  
  f464b139
- Change pretty printer of rationals to accurate one for manual testing · 87d70593
  Heiko Becker authored Aug 24, 2016
  
  87d70593
- Test multiplication, fix flaw · d17de1b5
  Heiko Becker authored Aug 24, 2016
  
  d17de1b5
- Add validator functions, currently unproven · 6ee8f753
  Heiko Becker authored Aug 24, 2016
  
  6ee8f753
23 Aug, 2016 8 commits
- SimpleDoppler test working by hand · 349fbc0f
  Heiko Becker authored Aug 23, 2016
  
  349fbc0f
- Prove error for multiplication, still needs testing wether computed bound is... · 706c08f3
  Heiko Becker authored Aug 23, 2016
```
Prove error for multiplication, still needs testing wether computed bound is low enough for actual validation
```
  706c08f3
- Fix holes in correctness lemma. Only multiplication left · 6dac01f9
  Heiko Becker authored Aug 23, 2016
  
  6dac01f9
- Prove holes in validation of errors, which required validity of interval checker · e8dca322
  Heiko Becker authored Aug 23, 2016
  
  e8dca322
- Proof interval validation sound · 5166f958
  Heiko Becker authored Aug 23, 2016
  
  5166f958
- Prove subtraction correct for error bound validation · e720b1ec
  Heiko Becker authored Aug 23, 2016
  
  e720b1ec
- Minor lemma fixes · 9251741e
  Heiko Becker authored Aug 23, 2016
  
  9251741e
- Add some new tests · 31573e54
  Heiko Becker authored Aug 23, 2016
  
  31573e54
22 Aug, 2016 3 commits
- Addition correct apart from correctness hole for IV checker · a54517e0
  Heiko Becker authored Aug 22, 2016
  
  a54517e0
- Constants and Parameters are shown again · c18cbf6c
  Heiko Becker authored Aug 22, 2016
  
  c18cbf6c
- Prove existential rewriting lemma for evaluations · 687917a3
  Heiko Becker authored Aug 22, 2016
  
  687917a3
21 Aug, 2016 3 commits
- Proof draft for interval bounds correctness · c2fce16b
  Heiko Becker authored Aug 21, 2016
  
  c2fce16b
- Add unverified interval validation, division unsupported · b2217643
  Heiko Becker authored Aug 21, 2016
  
  b2217643
- Prove interval arithmetic on rationals · 2cf1ff57
  Heiko Becker authored Aug 21, 2016
  
  2cf1ff57
20 Aug, 2016 2 commits
- Make a little cleanup · 72273a09
  Heiko Becker authored Aug 20, 2016
  
  72273a09
- Fine tuning of infrastructure · d7b02693
  Heiko Becker authored Aug 20, 2016
  
  d7b02693
19 Aug, 2016 6 commits
- Add current state of interval arithmetic for HOL Light · b7e2923c
  Heiko Becker authored Aug 19, 2016
  
  b7e2923c
- Add draft state of checker · 868479ee
  Heiko Becker authored Aug 19, 2016
  
  868479ee
- Fix error bounds for simpleDoppler example, correct parameter bound... · c8a22163
  Heiko Becker authored Aug 19, 2016
```
Fix error bounds for simpleDoppler example, correct parameter bound computations and implemented addition bounds
```
  c8a22163
- Fix bug in error computation, use machineEpsilon/2 now instead of machineEps... · 159cf56b
  Heiko Becker authored Aug 19, 2016
  
  159cf56b
- Forgot to add RationalConstruction.v · b5bf6af1
  Heiko Becker authored Aug 19, 2016
  
  b5bf6af1
- Certificate checker can soundly validate constants now · cd137018
  Heiko Becker authored Aug 19, 2016
  
  cd137018
18 Aug, 2016 1 commit
- Add draft of error computing function · 8f121ce2
  Heiko Becker authored Aug 18, 2016
  
  8f121ce2