ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
fsf-15
why3/examples
History
Matteo Manighetti cde6ba24c9 Merge remote-tracking branch 'why3-inria/master' into why3-devel
2024-02-20 11:14:13 +01:00
..
add_list
Upgrade Z3 proofs
2023-08-28 14:29:51 +02:00
add_list_vc_sp
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
algo63
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
algo64
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
algo65
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
all_distinct
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
amortization
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
arm
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
array_most_frequent
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
array_of_list
new example: array_of_list
2024-02-02 19:17:29 +01:00
assigning_meanings_to_programs
fix sessions
2024-02-20 11:10:11 +01:00
avl
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
bag
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
balance
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
bellman_ford
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
bignum
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
binary_multiplication
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
binary_search
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
binary_search_vc_sp
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
binary_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
binary_sqrt
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
binomial
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
binomial_heap
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
bitcount
fix sessions
2024-02-20 11:10:11 +01:00
bitvector_examples
fix sessions
2024-02-20 11:10:11 +01:00
bitvectors
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
bitwalker
fix sessions
2024-02-20 11:10:11 +01:00
braun_trees
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
bresenham
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
bts
fix sessions
2024-02-20 11:10:11 +01:00
bubble_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
c_cursor
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
check-builtin
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
checking_a_large_routine
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
coincidence_count
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
coincidence_count_list
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
conjugate
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
counting_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
cubic_root
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
cursor_examples
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
decrease1
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
defunctionalization
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
dfa_example
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
dfs
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
dijkstra
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
disamb
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
division
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
doc_examples
…
double_wp
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
dyck
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
edit_distance
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
equality_up_to_spaces
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
esterel
fix sessions
2024-02-20 11:10:11 +01:00
euler001
Move CVC4 proofs to CVC5
2023-08-28 14:31:08 +02:00
euler002
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
euler011
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
euler_sieve
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
ewd673
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
f_puzzle
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
fact
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
fact_vc_sp
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
fenwick
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
fib_memo
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
fibonacci
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
fill
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
find
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
finger_trees
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
finite_tarski
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
flag
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
flag2
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
flexible_arrays
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
foveoos11_challenge1
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
foveoos11_challenge2
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
foveoos11_challenge3
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
foveoos11-cm
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
gcd
Merge remote-tracking branch 'why3-inria/master' into why3-devel
2024-02-20 11:14:13 +01:00
gcd_bezout
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
gcd_bezout_vc_sp
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
gcd_vc_sp
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
generate_all_trees
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
gnome_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
hackers-delight
fix sessions
2024-02-20 11:10:11 +01:00
hashtbl_impl
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
hillel_challenge
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
huffman_with_two_queues
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
i_cant_believe_it_can_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
induction
Upgrade Z3 proofs
2023-08-28 14:29:51 +02:00
infinity_of_primes
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
insertion_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
insertion_sort_list
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
insertion_sort_naive
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
inverse_in_place
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
isqrt
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
isqrt_von_neumann
Facilitate proof of arithmetic on bitvectors by Alt-Ergo
2024-02-20 11:10:10 +01:00
just_join
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
kleene_algebra
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
kmp
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
knuth_prime_numbers
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
koda_ruskey
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
largest_prime_factor
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
lcp
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
leftist_heap
Move CVC4 proofs to CVC5
2023-08-28 14:31:08 +02:00
linear_probing
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
linked_list_rev
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
list_removal
Upgrade Z3 proofs
2023-08-28 14:29:51 +02:00
locate_max
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
logic
fix sessions
2024-02-20 11:10:11 +01:00
max_matrix
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
maximum_subarray
examples: variant of Kadane's algorithm
2024-02-11 19:11:47 +01:00
mccarthy
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
mccarthy_vc_sp
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
mergesort_array
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
mergesort_list
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
mergesort_queue
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
mex
improve mex example
2024-01-29 12:11:27 +01:00
micro-c
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
min_max
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
mjrty
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
mlcfg
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
muller
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
multiprecision
fix sessions
2024-02-20 11:10:11 +01:00
mutual_recursion
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
my_cosine
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
nistonacci
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
numeric
Forward propagation of rounding errors
2024-01-18 10:31:14 +00:00
optimal_replay
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
pairing_heap
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
pairing_heap_bin
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
pancake_sorting
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
patience
Upgrade Z3 proofs
2023-08-28 14:29:51 +02:00
pigeonhole
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
power
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
power_vc_sp
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
prover
Fix occurrences of "occurences".
2023-11-23 19:04:11 +01:00
python
Remove some trailing whitespaces.
2023-11-23 18:46:29 +01:00
queens
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
queens_bv
fix sessions
2024-02-20 11:10:11 +01:00
queue_two_lists
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
quicksort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
random_access_list
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
register_allocation
updated sessions
2023-08-24 16:29:59 +02:00
relabel
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
remove_duplicate
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
remove_duplicate_hash
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
residual
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
resizable_array
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
rightmostbittrick
fix sessions
2024-02-20 11:10:11 +01:00
ring_buffer
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
ring_decision
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
ropes
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
same_fringe
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
schorr_waite
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
schorr_waite_via_recursion
updated sessions
2023-08-24 16:29:59 +02:00
schorr_waite_with_ghost_monitor
updated sessions
2023-08-24 16:29:59 +02:00
search
cleaning up
2023-12-14 20:01:43 +01:00
selection_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
sf
Move CVC4 proofs to CVC5
2023-08-28 14:31:08 +02:00
sieve
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
skew_heaps
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
snapshotable_trees
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
sorted_list
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
space_saving
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
split_string
fix sessions
2024-02-20 11:10:11 +01:00
stackify
refresh identifiers in variant clauses
2023-09-28 22:09:56 +02:00
stdlib
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
string_base64_encoding
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
string_hex_encoding
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
string_search
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
subsequence
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
sudoku
Use Option from standard library
2024-01-22 16:43:44 +01:00
sumrange
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
swap
fix sessions
2024-02-20 11:10:11 +01:00
tests
Update Alt-Ergo 2.3.x proofs
2023-08-28 14:17:52 +02:00
tests-provers
fix sessions
2024-02-20 11:10:11 +01:00
there_and_back_again
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
three_idem_ring
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
topological_sorting
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
tortoise_and_hare
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
tower_of_hanoi
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
toy_compiler
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
tree_height
Move CVC4 proofs to CVC5
2023-08-28 14:31:08 +02:00
tree_of_array
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
tree_of_list
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
unraveling_a_card_trick
Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.
2023-09-07 18:05:01 +00:00
use_api
Merge remote-tracking branch 'why3-inria/master' into why3-devel
2024-02-20 11:14:13 +01:00
vacid_0_binary_heaps
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
vacid_0_build_maze
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
vacid_0_red_black_trees
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
vacid_0_sparse_array
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2015_dancing_links
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2015_parallel_gcd
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
verifythis_2015_relaxed_prefix
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2016_matrix_multiplication
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2016_tree_traversal
updated sessions
2023-08-24 16:29:59 +02:00
verifythis_2017_maximum_sum_submatrix
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2017_odd_even_sort_rearranging
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2017_odd_even_transposition_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2017_pair_insertion_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2017_tree_buffer
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_array_based_queuing_lock_1
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_array_based_queuing_lock_2
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_le_rouge_et_le_noir_1
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2018_le_rouge_et_le_noir_2
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_mind_the_gap_1
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_mind_the_gap_2
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2018_register_allocation
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2019_cartesian_trees
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_2019_ghc_sort
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_2021_dll_to_bst
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2021_lexicographic_permutations_1
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2021_lexicographic_permutations_2
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2021_shearsort
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
verifythis_2021_shearsort_modified
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
verifythis_fm2012_LRS
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
verifythis_fm2012_treedel
updated sessions
2023-08-24 16:29:59 +02:00
verifythis_PrefixSumRec
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
vstte10_aqueue
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
vstte10_inverting
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
vstte10_max_sum
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
vstte10_queens
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
vstte10_search_list
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
vstte12_bfs
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
vstte12_combinators
Use Option from standard library
2024-01-22 16:43:44 +01:00
vstte12_ring_buffer
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
vstte12_tree_reconstruction
Resolve "Remove axioms in Z3 and CVC4 drivers"
2023-09-01 15:47:33 +00:00
vstte12_two_way_sort
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
warshall_algorithm
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
white_and_black_balls
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
word_common_factor
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
WP_revisited
Fix session timings on moloch
2023-10-23 09:18:45 +02:00
wrap_lines
Resolve "Add injectivity for type invariant"
2024-01-31 13:02:13 +00:00
zeros
Fix sessions for nightly bench.
2023-10-22 15:49:03 +02:00
add_list_vc_sp.mlw
…
add_list.mlw
…
algo63.mlw
…
algo64.mlw
…
algo65.mlw
…
all_distinct.mlw
…
amortization.mlw
…
arm.mlw
…
array_most_frequent.mlw
…
array_of_list.mlw
new example: array_of_list
2024-02-02 19:17:29 +01:00
assigning_meanings_to_programs.mlw
gallery: more auto-dereference
2024-01-23 19:09:26 +01:00
bag.mlw
remove unsound module null.Null
2024-01-27 10:58:19 +01:00
balance.mlw
gallery: improve balance example even more
2023-04-07 10:59:08 +02:00
bellman_ford.mlw
…
bench.sh
…
bignum.mlw
…
binary_multiplication.mlw
…
binary_search_vc_sp.mlw
…
binary_search.mlw
…
binary_sort.mlw
…
binary_sqrt.mlw
…
binomial_heap.mlw
…
binomial.mlw
new example: binomial coefficient
2023-02-17 19:31:10 +01:00
bitcount.mlw
Several renamings and fix a few pre and post-conditions
2021-09-29 08:57:02 +02:00
bitvector_examples.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
bitwalker.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
braun_trees.mlw
gallery: two return types added
2022-12-01 20:02:29 +01:00
bresenham.mlw
…
bubble_sort.mlw
…
checking_a_large_routine.mlw
examples: variant of Turing's factorial
2022-08-26 11:27:04 +02:00
coincidence_count_list.mlw
…
coincidence_count.mlw
…
conjugate.mlw
…
counting_sort.mlw
…
cubic_root.mlw
…
cursor_examples.mlw
Use interfaces in cursor_examples.mlw
2023-05-23 13:27:45 +02:00
decrease1.mlw
…
defunctionalization.mlw
…
dfa_example.mlw
…
dfs.mlw
…
dijkstra.mlw
…
disamb.mlw
…
division.mlw
…
dyck.mlw
…
edit_distance.mlw
…
equality_up_to_spaces.mlw
…
esterel.mlw
…
euler001.mlw
Update comment.
2022-10-25 05:24:17 +02:00
euler002.mlw
…
euler011.mlw
…
euler_sieve.mlw
fix sessions
2021-06-25 14:15:38 +02:00
ewd673.mlw
…
f_puzzle.mlw
…
fact_vc_sp.mlw
…
fact.mlw
…
fenwick.mlw
…
fib_memo.mlw
…
fibonacci.mlw
fix sessions
2022-07-30 11:40:25 +02:00
fill.mlw
…
find.mlw
…
finger_trees.mlw
…
finite_tarski.mlw
…
flag2.mlw
…
flag.mlw
…
flexible_arrays.mlw
flexible arrays: more operations
2023-04-18 14:35:23 +02:00
foveoos11_challenge1.mlw
…
foveoos11_challenge2.mlw
…
foveoos11_challenge3.mlw
…
gcd_bezout_vc_sp.mlw
…
gcd_bezout.mlw
…
gcd_vc_sp.mlw
…
gcd.mlw
…
generate_all_trees.mlw
…
gnome_sort.mlw
…
hackers-delight.mlw
…
hashtbl_impl.mlw
…
hello-world.mlw
…
hillel_challenge.mlw
…
huffman_with_two_queues.mlw
…
i_cant_believe_it_can_sort.mlw
cleaning up
2022-07-04 11:28:47 +02:00
incremental.mlw
…
induction.mlw
…
infinity_of_primes.mlw
new example: infinity_of_primes
2021-06-11 14:37:03 +02:00
insertion_sort_list.mlw
…
insertion_sort_naive.mlw
…
insertion_sort.mlw
…
inverse_in_place.mlw
…
isqrt_von_neumann.mlw
…
isqrt.mlw
…
just_join.mlw
Fix typos.
2023-11-23 18:38:17 +01:00
kleene_algebra.mlw
kleene_algebra example: no more unnecessary axioms
2021-06-27 18:56:11 +02:00
kmp.mlw
…
knuth_prime_numbers.mlw
…
koda_ruskey.mlw
…
largest_prime_factor.mlw
…
lcp.mlw
…
leftist_heap.mlw
…
linear_probing.mlw
…
linked_list_rev.mlw
gallery: list reversal terminates, even on cyclic lists
2022-11-06 00:02:54 +01:00
list_removal.mlw
…
locate_max.mlw
Document the extraction to C.
2022-05-11 17:46:27 +02:00
max_matrix.mlw
…
maximum_subarray.mlw
examples: variant of Kadane's algorithm
2024-02-11 19:11:47 +01:00
mccarthy_vc_sp.mlw
…
mccarthy.mlw
…
mergesort_array.mlw
…
mergesort_list.mlw
…
mergesort_queue.mlw
…
mex.mlw
improve mex example
2024-01-29 12:11:27 +01:00
min_max.mlw
…
mjrty.mlw
new example: space saving algorithm
2023-05-09 15:54:05 +02:00
muller.mlw
…
mutual_recursion.mlw
…
my_cosine.mlw
…
nistonacci.mlw
…
optimal_replay.mlw
…
pairing_heap_bin.mlw
…
pairing_heap.mlw
…
pancake_sorting.mlw
…
patience.mlw
…
pigeonhole.mlw
…
power_vc_sp.mlw
…
power.mlw
example power: cleaning up, new version
2023-07-25 10:48:55 +02:00
queens_bv.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
queens.mlw
…
queue_two_lists.mlw
…
quicksort.mlw
…
random_access_list.mlw
…
reduced_regtests.list
…
register_allocation.mlw
…
regtests.out
Fix sessions and update oracles for result variables in VC SP
2021-10-04 15:53:08 +02:00
regtests.sh
add option --ignore-shapes to why3 replay
2023-07-18 15:31:43 +00:00
relabel.mlw
…
remove_duplicate_hash.mlw
…
remove_duplicate.mlw
…
residual.mlw
…
resizable_array.mlw
…
rightmostbittrick.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
ring_buffer.mlw
…
ropes.mlw
…
same_fringe.mlw
…
schorr_waite_via_recursion.mlw
…
schorr_waite_with_ghost_monitor.mlw
…
schorr_waite.mlw
…
search.mlw
cleaning up
2023-12-14 20:01:43 +01:00
selection_sort.mlw
…
sf.mlw
…
sieve.mlw
…
skew_heaps.mlw
…
snapshotable_trees.mlw
…
sorted_list.mlw
…
space_saving.mlw
Fix typos.
2023-11-23 18:38:17 +01:00
split_string.mlw
split_string example updated
2024-01-25 21:49:21 +01:00
string_base64_encoding.mlw
…
string_hex_encoding.mlw
…
string_search.mlw
…
subsequence.mlw
…
sudoku.mlw
Fix occurrences of "occurences".
2023-11-23 19:04:11 +01:00
sumrange.mlw
…
swap.mlw
…
there_and_back_again.mlw
…
three_idem_ring.mlw
…
TODO
…
topological_sorting.mlw
…
tortoise_and_hare.mlw
fix sessions
2021-06-25 15:01:56 +02:00
tower_of_hanoi.mlw
…
toy_compiler.mlw
Remove some trailing whitespaces.
2023-11-23 18:46:29 +01:00
tree_height.mlw
…
tree_of_array.mlw
…
tree_of_list.mlw
…
unraveling_a_card_trick.mlw
…
vacid_0_build_maze.mlw
…
vacid_0_red_black_trees.mlw
…
vacid_0_sparse_array.mlw
…
verifythis_2015_dancing_links.mlw
…
verifythis_2015_parallel_gcd.mlw
…
verifythis_2015_relaxed_prefix.mlw
…
verifythis_2016_tree_traversal.mlw
…
verifythis_2017_maximum_sum_submatrix.mlw
…
verifythis_2017_odd_even_sort_rearranging.mlw
…
verifythis_2017_odd_even_transposition_sort.mlw
…
verifythis_2017_pair_insertion_sort.mlw
…
verifythis_2017_tree_buffer.mlw
…
verifythis_2018_array_based_queuing_lock_1.mlw
…
verifythis_2018_array_based_queuing_lock_2.mlw
…
verifythis_2018_le_rouge_et_le_noir_1.mlw
…
verifythis_2018_le_rouge_et_le_noir_2.mlw
…
verifythis_2018_mind_the_gap_1.mlw
…
verifythis_2018_mind_the_gap_2.mlw
…
verifythis_2018_register_allocation.mlw
simplifies fib tail rec proof and add counterexample to regalloc as a comment
2021-09-16 16:33:30 +02:00
verifythis_2019_cartesian_trees.mlw
…
verifythis_2019_ghc_sort.mlw
…
verifythis_2021_dll_to_bst.mlw
typo
2023-02-17 13:32:33 +01:00
verifythis_2021_lexicographic_permutations_1.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_lexicographic_permutations_2.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_shearsort_modified.mlw
fix euler_sieve, array and split_vc interaction
2021-04-30 10:48:03 +02:00
verifythis_2021_shearsort.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_fm2012_LRS.mlw
Remove some trailing whitespaces.
2023-11-23 18:46:29 +01:00
verifythis_fm2012_treedel.mlw
…
verifythis_PrefixSumRec.mlw
…
vstte10_aqueue.mlw
…
vstte10_inverting.mlw
…
vstte10_max_sum.mlw
…
vstte10_queens.mlw
…
vstte10_search_list.mlw
…
vstte12_bfs.mlw
…
vstte12_combinators.mlw
support for algebraic types simplify some proofs.
2023-01-31 08:25:07 +01:00
vstte12_ring_buffer.mlw
…
vstte12_tree_reconstruction.mlw
…
vstte12_two_way_sort.mlw
…
warshall_algorithm.mlw
…
white_and_black_balls.mlw
…
word_common_factor.mlw
…
wrap_lines.mlw
…
zeros.mlw
…