aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'release/v1.2.2'Yann Herklotz2021-10-013-3/+7
|\
| * Fix citation file and READMEv1.2.2Yann Herklotz2021-10-012-3/+2
| * Update Changelog with 1.2.2 releaseYann Herklotz2021-10-011-0/+5
* | Merge branch 'develop'Yann Herklotz2021-10-0121-280/+2735
|\ \ | |/ |/|
| * Fix equivalence checkingYann Herklotz2021-10-012-5/+2
| * Add printers for expressions and RTLParYann Herklotz2021-10-012-0/+114
| * Fix compilation of new intermediate languagesYann Herklotz2021-10-016-12/+21
| * Improve equivalence checking using SATYann Herklotz2021-10-011-15/+22
| * Fix scheduler for operation chainingYann Herklotz2021-10-011-8/+22
| * Add back scheduling to the driverYann Herklotz2021-09-302-2/+2
| * Merge remote-tracking branch 'origin/develop' into developYann Herklotz2021-09-2913-56/+1259
| |\
| | * Make all OCaml files compileYann Herklotz2021-09-292-4/+4
| | * Revert "Remove more OCaml files to compile successfully without admits."Yann Herklotz2021-09-275-0/+1085
| | * Add dependencies for Alectryon documentationYann Herklotz2021-09-275-9/+15
| | * Compile HTLPargen againYann Herklotz2021-09-242-6/+5
| | * Fix scopingYann Herklotz2021-09-241-12/+10
| | * Add back top-level functionsYann Herklotz2021-09-241-40/+157
| * | Export without titleYann Herklotz2021-09-271-0/+2
| |/
| * RTLpargen passes compilation againYann Herklotz2021-09-222-10/+18
| * Merge remote-tracking branch 'origin/develop' into developYann Herklotz2021-09-2290-1650/+4575
| |\
| | * Fix the comparison of predicated expressionsYann Herklotz2021-09-221-138/+174
| | * Change Inductive to recordYann Herklotz2021-09-223-18/+17
| | * Start adding hashing to RTLPargenYann Herklotz2021-09-202-7/+51
| | * Merge branch 'master' into developYann Herklotz2021-09-202-12/+22
| | |\
| | * \ Merge branch 'master' into developYann Herklotz2021-09-1887-1521/+4378
| | |\ \
| * | | | Add full proof of SAT conversionYann Herklotz2021-07-241-2/+22
| * | | | Finish SAT proofYann Herklotz2021-07-241-3/+4
| |/ / /
| * | | 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
* | | | Merge remote-tracking branch 'origin/master'Yann Herklotz2021-09-291-3/+3
|\ \ \ \
| * | | | Update README on the status of VericertYann Herklotz2021-09-271-2/+2
| * | | | Add empty titleYann Herklotz2021-09-272-0/+2
| | |_|/ | |/| |
* | | | Update docsYann Herklotz2021-09-291-0/+0
* | | | Export without titleYann Herklotz2021-09-271-0/+2
|/ / /
* | | Update the docsYann Herklotz2021-09-201-0/+0
generated by cgit (git 2.34.1) at 2024-06-26 15:07:44 +0000