aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Start adding hashing to RTLPargenYann Herklotz2021-09-202-7/+51
* Merge branch 'master' into developYann Herklotz2021-09-202-12/+22
|\
| * Update the docsYann Herklotz2021-09-201-0/+0
| * Improve the changelogYann Herklotz2021-09-181-10/+24
* | Merge branch 'master' into developYann Herklotz2021-09-1887-1521/+4378
|\|
| * Merge remote-tracking branch 'origin/master'Yann Herklotz2021-09-176-81/+131
| |\
| | * Update docsYann Herklotz2021-09-162-2/+2
| | * Add number of pages correctlyYann Herklotz2021-09-151-1/+1
| | * Fix a typo in README.orgYann Herklotz2021-09-151-1/+1
| | * Add DOI to articleYann Herklotz2021-09-152-1/+2
| | * Add CITATION.cffYann Herklotz2021-09-151-0/+46
| | * Fix linguist-vendored for repository statisticsYann Herklotz2021-09-151-1/+1
| | * Add more information about paper to READMEYann Herklotz2021-09-151-48/+64
| | * Move license to the SoftwarePipelining directoryYann Herklotz2021-09-152-32/+19
| * | Fix compilation with new CompCert versionYann Herklotz2021-09-174-34/+16
| |/
| * Fix proofs for SATYann Herklotz2021-08-121-6/+27
| * Add more artifact documentationYann Herklotz2021-08-122-4/+112
| * Fix pretty printing issue in VerilogYann Herklotz2021-08-121-1/+1
| * Use main instead of top for synthesising Vericert designsoopsla21Yann Herklotz2021-07-241-1/+1
| * Update instructions and fix testv1.2.1Yann Herklotz2021-07-124-6/+5
| * Remove comments in docker fileYann Herklotz2021-07-121-3/+3
| * Update the artifact descriptionYann Herklotz2021-07-127-4/+204
| * Remove more OCaml files to compile successfully without admits.Yann Herklotz2021-07-115-1085/+0
| * Remove unnecessary files and proofsYann Herklotz2021-07-117-16/+19
| * Update the run-legup.sh fileYann Herklotz2021-07-111-0/+4
| * Add legup scriptYann Herklotz2021-07-114-4/+74
| * Fix the small test bench for VericertYann Herklotz2021-07-117-137/+67
| * Fix some more of the benchmarksYann Herklotz2021-07-118-49/+35
| * Add divider benchmarksYann Herklotz2021-07-1144-0/+3581
| * Fix makefiles and add a parent makefileYann Herklotz2021-07-104-3/+18
| * Fix Makefiles slightlyYann Herklotz2021-07-108-7/+12
| * Add more documentation and clean up benchmarksYann Herklotz2021-07-1012-158/+139
| * Add docker file and some commentsYann Herklotz2021-07-092-0/+6
* | New release information to the changelogYann Herklotz2021-07-071-0/+3
* | Add changelog which mentions the RAM supportYann Herklotz2021-07-071-0/+1
* | Add predicate semantics to abstractdev/ioYann Herklotz2021-05-261-69/+296
* | Add predicate semantics to RTLParYann Herklotz2021-05-261-7/+8
* | Add predicate semantics to RTLBlockYann Herklotz2021-05-261-7/+8
* | Fix if-conversion pass with positivesYann Herklotz2021-05-261-1/+1
* | Change naturals to positive in predicatesYann Herklotz2021-05-262-45/+79
* | Add very top-level proofYann Herklotz2021-05-231-0/+33
* | Fix admitted in last theoremYann Herklotz2021-05-211-3/+8
* | Finish top-level of proofYann Herklotz2021-05-212-22/+23
* | Minimise the proof a bitYann Herklotz2021-05-161-18/+12
* | Finish up step_cf_instr_correct againYann Herklotz2021-05-162-19/+43
* | Fix the top-level proofs with new state_matchYann Herklotz2021-05-152-27/+164
* | Finish abstract interpretationYann Herklotz2021-05-121-75/+199
* | Fix admitted in first proof of sem. preservationYann Herklotz2021-05-101-19/+68
* | Finish correctness of semantics wrt. RTBlockYann Herklotz2021-05-061-84/+327
* | Add admitted proof of translations in RTLPargenYann Herklotz2021-05-031-27/+177
|/