Commits · validate-0.88.3 · sovereign / why3-avr

23 Aug, 2019 7 commits
- modified 96-bit karatsuba in similar sense · 274df245
  Marc Schoolderman authored Aug 23, 2019
  
  274df245
- convert karatsuba80 into a 'localized' version · 5538acc9
  Marc Schoolderman authored Aug 22, 2019
  
  5538acc9
- cleanup of karatsuba64 · 887f74f0
  Marc Schoolderman authored Aug 22, 2019
  
  887f74f0
- merged avr_code22 into karatsuba48/64 · 6f42fc27
  Marc Schoolderman authored Aug 22, 2019
  
  6f42fc27
- cleanup proof; moved two instructions back to original position · 0ffc2ae5
  Marc Schoolderman authored Aug 22, 2019
  
  0ffc2ae5
- ported to why3 0.88.3 · 70d2f1bd
  Marc Schoolderman authored Aug 22, 2019
  
  70d2f1bd
- experiment: express effects of all blocks in local terms (why3 0.87.3) · c83341b2
  Marc Schoolderman authored Aug 22, 2019
  
  c83341b2
22 Aug, 2019 2 commits
- typo: assume -> assert. luckily, it was easily proven. · 5279ed0a
  Marc Schoolderman authored Aug 22, 2019
  
  5279ed0a
- removed pvs files · 42741d7b
  Marc Schoolderman authored Aug 22, 2019
  
  42741d7b
20 Aug, 2019 2 commits
- updated README; removed vestigial dependency on Z3 · 1bcdae7f
  Marc Schoolderman authored Aug 20, 2019
  
  1bcdae7f
- major cleanup of directory structure · db0572e2
  Marc Schoolderman authored Aug 19, 2019
  
  db0572e2
19 Aug, 2019 1 commit
- ported the proofs to why3 version 0.88.3; · ca07259c
  Marc Schoolderman authored Aug 19, 2019
```
removed any dependency on alt-ergo < 2.0.0
```
  ca07259c
20 Apr, 2018 2 commits
- ran bisection on proofs · 02ec34b5
  Marc Schoolderman authored Apr 20, 2018
  
  02ec34b5
- slight optimization · 0ed6b403
  Marc Schoolderman authored Apr 20, 2018
  
  0ed6b403
09 May, 2017 1 commit
- optimised 96-bit version · f370892c
  Marc Schoolderman authored May 09, 2017
  
  f370892c
08 May, 2017 2 commits
- optimised (removed checks) · 9d308b2c
  Marc Schoolderman authored May 08, 2017
  
  9d308b2c
- added 64- 80- and 96-bit karatsuba versions · 3ab5cbd5
  Marc Schoolderman authored Apr 13, 2017
  
  3ab5cbd5
13 Apr, 2017 2 commits
- added markings to reduce the number of invariants/asserts needed · 5d08ecc9
  Marc Schoolderman authored Apr 13, 2017
  
  5d08ecc9
- version bump of tools used · 402accd8
  Marc Schoolderman authored Apr 13, 2017
  
  402accd8
14 Mar, 2017 1 commit
- added shadow-registers to remove several assertions and improve verification times · e7a225ea
  Marc Schoolderman authored Mar 14, 2017
  
  e7a225ea
07 Dec, 2016 2 commits
- added README · a8bc648b
  Marc Schoolderman authored Dec 07, 2016
  
  a8bc648b
- cleaned up files · d94b7b24
  Marc Schoolderman authored Dec 07, 2016
  
  d94b7b24
06 Dec, 2016 2 commits
- remove old abandoned attempts · 16b1f0f4
  Marc Schoolderman authored Dec 06, 2016
  
  16b1f0f4
- enhanced model with memory/register exclusion · de64bfd8
  Marc Schoolderman authored Dec 06, 2016
  
  de64bfd8
05 Dec, 2016 1 commit
- int_flag -> cpu_flag · 6e65fb15
  Marc Schoolderman authored Dec 05, 2016
  
  6e65fb15
02 Dec, 2016 2 commits
- replace M with Map · 5f955d6b
  Marc Schoolderman authored Dec 02, 2016
  
  5f955d6b
- alternative justification of add · 83147d46
  Marc Schoolderman authored Dec 02, 2016
  
  83147d46
29 Nov, 2016 1 commit
- rename register_file -> address_space · f104ac14
  Marc Schoolderman authored Nov 29, 2016
  
  f104ac14
24 Nov, 2016 1 commit
- 40x40 in push button style · bbb5e818
  Marc Schoolderman authored Nov 24, 2016 and Marc Schoolderman committed Nov 24, 2016
  
  bbb5e818
22 Nov, 2016 1 commit
- further cleanup · ce4fb8a8
  Marc Schoolderman authored Nov 22, 2016 and Marc Schoolderman committed Nov 22, 2016
  
  ce4fb8a8
10 Nov, 2016 1 commit
- further reduction · 3328d354
  Marc Schoolderman authored Nov 10, 2016 and Marc Schoolderman committed Nov 10, 2016
  
  3328d354
09 Nov, 2016 1 commit
- removed checks · ad31b617
  Marc Schoolderman authored Nov 09, 2016 and Marc Schoolderman committed Nov 09, 2016
  
  ad31b617
08 Nov, 2016 2 commits
- minimization (invalidates some checks) · 80df2b13
  Marc Schoolderman authored Nov 08, 2016 and Marc Schoolderman committed Nov 08, 2016
  
  80df2b13
- first verification · afc2f3cc
  Marc Schoolderman authored Nov 08, 2016 and Marc Schoolderman committed Nov 08, 2016
  
  afc2f3cc
21 Oct, 2016 3 commits
- optimized mul32 · 293386ca
  Marc Schoolderman authored Oct 21, 2016 and Marc Schoolderman committed Oct 21, 2016
  
  293386ca
- edited mul24 · 07dfa4cb
  Marc Schoolderman authored Oct 21, 2016 and Marc Schoolderman committed Oct 21, 2016
  
  07dfa4cb
- initial commit · 61b2f2ba
  Marc Schoolderman authored Oct 21, 2016 and Marc Schoolderman committed Oct 21, 2016
  
  61b2f2ba
25 Nov, 2016 1 commit
- added NCSA license file · c4a1e8df
  Marc Schoolderman authored Nov 25, 2016
  
  c4a1e8df