index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
...
|
*
Make minor updates
Son Ho
2024-03-17
3
-7
/
+14
|
*
Fix a small issue ollowing updates in Charon
Son Ho
2024-03-17
1
-3
/
+8
|
*
Update following changes in Charon
Son Ho
2024-03-17
11
-72
/
+34
|
/
*
Merge pull request #88 from AeneasVerif/son/clashes
Son HO
2024-03-11
37
-703
/
+825
|
\
|
*
Update the flake.lock
Son Ho
2024-03-11
1
-12
/
+12
|
*
Regenerate the test files
Son Ho
2024-03-11
14
-244
/
+227
|
*
Simplify the generated names
Son Ho
2024-03-11
1
-14
/
+25
|
*
Update the generated files
Son Ho
2024-03-11
15
-380
/
+389
|
*
Update tests/Makefile
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the generation of names
Son Ho
2024-03-11
7
-39
/
+57
|
*
Update a builtin name
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the builtin name patterns
Son Ho
2024-03-10
1
-23
/
+66
|
*
Update the name generation and add CLI to print external pat names
Son Ho
2024-03-10
7
-48
/
+106
|
/
*
Merge pull request #85 from AeneasVerif/son/fix_loops3
Son HO
2024-03-09
28
-350
/
+1185
|
\
|
*
Update the flake.lock
Son Ho
2024-03-09
1
-24
/
+24
|
*
Regenerate the test files
Son Ho
2024-03-09
10
-0
/
+420
|
*
Fix an issue with the divergent encoding
Son Ho
2024-03-09
1
-3
/
+27
|
*
Fix some issues
Son Ho
2024-03-08
2
-9
/
+10
|
*
Add some comments
Son Ho
2024-03-08
2
-9
/
+12
|
*
Fix an issue in PureMicroPasses.filter_loop_inputs
Son Ho
2024-03-08
1
-13
/
+43
|
*
Simplify the contexts before symbolically evaluating loops
Son Ho
2024-03-08
4
-2
/
+137
|
*
Fix a last issue
Son Ho
2024-03-08
2
-51
/
+110
|
*
Fix an issue with the loops
Son Ho
2024-03-08
1
-1
/
+7
|
*
Make progress on fixing the loops
Son Ho
2024-03-08
8
-31
/
+70
|
*
Fix a small issue with the loops
Son Ho
2024-03-08
2
-7
/
+19
|
*
Fix some issues with the loops
Son Ho
2024-03-08
3
-140
/
+206
|
*
Do not fail in end_abstraction_aux if the abs disappeared
Son Ho
2024-03-08
2
-64
/
+80
|
*
Add logging information
Son Ho
2024-03-08
3
-0
/
+24
|
*
Update Print.ml
Son Ho
2024-03-08
1
-8
/
+8
|
/
*
Merge pull request #83 from AeneasVerif/son/backs
Son HO
2024-03-08
76
-18929
/
+705
|
\
|
*
Update the workers
Son Ho
2024-03-08
1
-1
/
+0
|
*
Update the flake.nix
Son Ho
2024-03-08
1
-14
/
+5
|
*
Remove the split test files for F*
Son Ho
2024-03-08
55
-16239
/
+0
|
*
Update the Makefile and remove the split files for F*
Son Ho
2024-03-08
5
-952
/
+4
|
*
Make progress on propagating the changes
Son Ho
2024-03-08
14
-949
/
+259
|
*
Remove the option to split fwd/back functions and update SymbolicToPure
Son Ho
2024-03-08
5
-776
/
+439
|
/
*
Merge pull request #82 from AeneasVerif/son/switch
Son HO
2024-03-08
20
-173
/
+352
|
\
|
*
Update the code generated for tuple projectors
Son Ho
2024-03-08
4
-19
/
+48
|
*
Fix tuple indexing for Lean backend
Zyad Hassan
2024-03-08
3
-6
/
+35
|
*
Update the generation of constant bodies for Lean
Son Ho
2024-03-08
6
-28
/
+26
|
*
Update the tuples syntax
Son Ho
2024-03-08
1
-1
/
+3
|
*
Update the tuples notations
Son Ho
2024-03-08
3
-51
/
+81
|
*
Remove some comments
Son Ho
2024-03-08
1
-31
/
+0
|
*
Update the handling of notations like #u32 or #isize
Son Ho
2024-03-08
4
-70
/
+104
|
*
Regenerate the test files
Son Ho
2024-03-08
5
-46
/
+46
|
*
Update the code generation
Son Ho
2024-03-08
2
-7
/
+6
|
*
Update the notation for heterogeneous negation
Son Ho
2024-03-08
1
-3
/
+12
|
*
Introduce a notation for constant scalars in match patterns
Son Ho
2024-03-07
1
-0
/
+29
|
*
Add a notation for tuple field accesses in Lean
Son Ho
2024-03-07
1
-0
/
+51
|
/
*
Merge pull request #73 from AeneasVerif/son/demo
Son HO
2024-02-11
17
-220
/
+3696
|
\
[prev]
[next]