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
26.0
why3/examples
History
MARCHE Claude 89a894b47a do not map IEEE floats theory to Alt-Ergo's own theory 
Upgrade to AE 2.6.2
2025-06-18 10:45:29 +09:00
..
add_list
…
add_list_vc_sp
…
algo63
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
algo64
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
algo65
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
all_distinct
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
amortization
…
anagrammi
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
arm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
array_most_frequent
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
array_of_list
…
assigning_meanings_to_programs
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
avl
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bag
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
balance
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bellman_ford
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bignum
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
binary_multiplication
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
binary_search
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
binary_search_vc_sp
…
binary_sort
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
binary_sqrt
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
binomial
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
binomial_heap
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bitcount
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
bitvector_examples
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bitvectors
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bitwalker
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
braun_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bresenham
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bts
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bubble_sort
…
c_cursor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
check-builtin
…
checking_a_large_routine
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
coincidence_count
…
coincidence_count_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
coma
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
conjugate
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
counting_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
cubic_root
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
cursor_examples
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
decrease1
…
defunctionalization
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
dfa_example
…
dfs
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
dijkstra
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
disamb
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
division
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
doc_examples
…
double_wp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
dyck
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
edit_distance
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
equality_up_to_spaces
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
esterel
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler001
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler002
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler011
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler_sieve
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ewd673
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
f_puzzle
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fact
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fact_vc_sp
…
fenwick
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fib_memo
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fibonacci
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fill
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
find
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
finger_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
finite_tarski
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
flag
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
flag2
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
flexible_arrays
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
foveoos11_challenge1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
foveoos11_challenge2
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
foveoos11_challenge3
…
foveoos11-cm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
gcd
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
gcd_bezout
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
gcd_bezout_vc_sp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
gcd_vc_sp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
generate_all_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
gnome_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
hackers-delight
…
hashtbl_impl
…
hillel_challenge
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
huffman_with_two_queues
…
i_cant_believe_it_can_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
induction
…
infinity_of_primes
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
insertion_sort
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
insertion_sort_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
insertion_sort_naive
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
inverse_in_place
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
isqrt
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
isqrt_von_neumann
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
just_join
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
kleene_algebra
…
kmp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
knuth_prime_numbers
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
koda_ruskey
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
largest_prime_factor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
lcp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
leftist_heap
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
linear_probing
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
linked_list_rev
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
list_removal
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
locate_max
…
logic
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
longest_increasing_subsequence
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
max_matrix
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
maximum_subarray
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mccarthy
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mccarthy_vc_sp
…
mergesort_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mergesort_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mergesort_queue
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mex
minimum excludant example
2025-02-01 21:22:20 +01:00
micro-c
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
min_max
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mjrty
…
mlcfg
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
muller
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
multiprecision
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
mutual_recursion
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
my_cosine
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
nistonacci
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
numeric
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
optimal_replay
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
pairing_heap
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
pairing_heap_bin
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
pancake_sorting
…
patience
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
pigeonhole
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
power
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
power_vc_sp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
proper_cuts
…
prover
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
python
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
queens
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
queens_bv
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
queue_two_lists
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
quicksort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
random_access_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
register_allocation
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
relabel
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
remove_duplicate
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
remove_duplicate_hash
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
residual
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
resizable_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
rightmostbittrick
…
ring_buffer
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ring_decision
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ropes
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
same_fringe
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
schorr_waite
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
schorr_waite_via_recursion
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
schorr_waite_with_ghost_monitor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
search
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
selection_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sf
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sieve
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
skew_heaps
…
snapshotable_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sorted_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
space_saving
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
split_string
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
stackify
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
stdlib
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
string_base64_encoding
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
string_hex_encoding
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
string_search
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
subsequence
…
sudoku
…
sumrange
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
swap
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tests
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tests-provers
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
there_and_back_again
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
three_idem_ring
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
topological_sorting
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tortoise_and_hare
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tower_of_hanoi
…
toy_compiler
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
tree_height
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tree_of_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tree_of_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
unraveling_a_card_trick
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
use_api
restored API example for counterexamples
2025-03-03 13:12:26 +01:00
vacid_0_binary_heaps
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_build_maze
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_red_black_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_sparse_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2015_dancing_links
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2015_parallel_gcd
…
verifythis_2015_relaxed_prefix
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2016_matrix_multiplication
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2016_tree_traversal
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_maximum_sum_submatrix
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_odd_even_sort_rearranging
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_odd_even_transposition_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_pair_insertion_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_tree_buffer
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_array_based_queuing_lock_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_array_based_queuing_lock_2
…
verifythis_2018_le_rouge_et_le_noir_1
…
verifythis_2018_le_rouge_et_le_noir_2
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_mind_the_gap_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_mind_the_gap_2
…
verifythis_2018_register_allocation
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2019_cartesian_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2019_ghc_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_dll_to_bst
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_lexicographic_permutations_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_lexicographic_permutations_2
…
verifythis_2021_shearsort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_shearsort_modified
…
verifythis_2024_challenge0
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2024_challenge1
…
verifythis_fm2012_LRS
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_fm2012_treedel
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_PrefixSumRec
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_aqueue
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_inverting
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_max_sum
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
vstte10_queens
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_search_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_bfs
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_combinators
…
vstte12_ring_buffer
…
vstte12_tree_reconstruction
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_two_way_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
warshall_algorithm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
white_and_black_balls
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
word_common_factor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
WP_revisited
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
wrap_lines
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
zeros
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
add_list_vc_sp.mlw
…
add_list.mlw
…
algo63.mlw
…
algo64.mlw
…
algo65.mlw
…
all_distinct.mlw
…
amortization.mlw
…
anagrammi.mlw
…
arm.mlw
…
array_most_frequent.mlw
…
array_of_list.mlw
…
assigning_meanings_to_programs.mlw
…
bag.mlw
…
balance.mlw
…
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
…
bitcount.mlw
…
bitvector_examples.mlw
…
bitwalker.mlw
…
braun_trees.mlw
…
bresenham.mlw
…
bubble_sort.mlw
…
checking_a_large_routine.mlw
…
coincidence_count_list.mlw
…
coincidence_count.mlw
…
conjugate.mlw
…
counting_sort.mlw
…
cubic_root.mlw
…
cursor_examples.mlw
…
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
…
euler002.mlw
…
euler011.mlw
…
euler_sieve.mlw
…
ewd673.mlw
…
f_puzzle.mlw
…
fact_vc_sp.mlw
…
fact.mlw
…
fenwick.mlw
…
fib_memo.mlw
…
fibonacci.mlw
…
fill.mlw
…
find.mlw
…
finger_trees.mlw
…
finite_tarski.mlw
…
flag2.mlw
…
flag.mlw
…
flexible_arrays.mlw
…
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
…
incremental.mlw
…
induction.mlw
…
infinity_of_primes.mlw
…
insertion_sort_list.mlw
…
insertion_sort_naive.mlw
…
insertion_sort.mlw
…
inverse_in_place.mlw
…
isqrt_von_neumann.mlw
…
isqrt.mlw
…
just_join.mlw
…
kleene_algebra.mlw
…
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
…
list_removal.mlw
…
locate_max.mlw
…
longest_increasing_subsequence.mlw
…
max_matrix.mlw
…
maximum_subarray.mlw
…
mccarthy_vc_sp.mlw
…
mccarthy.mlw
…
mergesort_array.mlw
…
mergesort_list.mlw
…
mergesort_queue.mlw
…
mex.mlw
minimum excludant example
2025-02-01 21:22:20 +01:00
min_max.mlw
…
mjrty.mlw
…
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
…
proper_cuts.mlw
…
queens_bv.mlw
…
queens.mlw
…
queue_two_lists.mlw
…
quicksort.mlw
…
random_access_list.mlw
…
reduced_regtests.list
…
register_allocation.mlw
…
regtests.out
…
regtests.sh
…
relabel.mlw
…
remove_duplicate_hash.mlw
…
remove_duplicate.mlw
…
residual.mlw
…
resizable_array.mlw
…
rightmostbittrick.mlw
…
ring_buffer.mlw
…
ropes.mlw
…
same_fringe.mlw
…
schorr_waite_via_recursion.mlw
…
schorr_waite_with_ghost_monitor.mlw
…
schorr_waite.mlw
…
search.mlw
…
selection_sort.mlw
…
sf.mlw
…
sieve.mlw
…
skew_heaps.mlw
…
snapshotable_trees.mlw
…
sorted_list.mlw
…
space_saving.mlw
…
split_string.mlw
…
string_base64_encoding.mlw
…
string_hex_encoding.mlw
…
string_search.mlw
…
subsequence.mlw
…
sudoku.mlw
…
sumrange.mlw
…
swap.mlw
…
there_and_back_again.mlw
…
three_idem_ring.mlw
…
TODO
…
topological_sorting.mlw
…
tortoise_and_hare.mlw
…
tower_of_hanoi.mlw
…
toy_compiler.mlw
…
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
…
verifythis_2019_cartesian_trees.mlw
…
verifythis_2019_ghc_sort.mlw
…
verifythis_2021_dll_to_bst.mlw
…
verifythis_2021_lexicographic_permutations_1.mlw
…
verifythis_2021_lexicographic_permutations_2.mlw
…
verifythis_2021_shearsort_modified.mlw
…
verifythis_2021_shearsort.mlw
…
verifythis_2024_challenge0.mlw
…
verifythis_2024_challenge1.mlw
…
verifythis_fm2012_LRS.mlw
…
verifythis_fm2012_treedel.mlw
…
verifythis_PrefixSumRec.mlw
…
vstte10_aqueue.mlw
…
vstte10_inverting.mlw
…
vstte10_max_sum.mlw
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
vstte10_queens.mlw
…
vstte10_search_list.mlw
…
vstte12_bfs.mlw
…
vstte12_combinators.mlw
…
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
…