Skip to content

PoorlyDefinedBehaviour/formal-methods

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

189 Commits
a_more_complex_thread
a_more_complex_thread
 
 
add_integers
add_integers
 
 
add_integers_p_lang
add_integers_p_lang
 
 
arbitrary_sorting_machine
arbitrary_sorting_machine
 
 
barrier
barrier
 
 
binary_search
binary_search
 
 
boolean_flags_are_enough_for_everyone
boolean_flags_are_enough_for_everyone
 
 
boss_fight
boss_fight
 
 
bounded_channel
bounded_channel
 
 
bounded_fifo_buffer
bounded_fifo_buffer
 
 
condition_variable
condition_variable
 
 
condition_variables
condition_variables
 
 
confused_counter
confused_counter
 
 
countdown_event
countdown_event
 
 
countdown_event_revisited
countdown_event_revisited
 
 
counter_incrementer
counter_incrementer
 
 
database
database
 
 
deadlock
deadlock
 
 
dekkers_algorithm
dekkers_algorithm
 
 
dining_philosophers
dining_philosophers
 
 
door
door
 
 
dragon_fire
dragon_fire
 
 
fifo_buffer
fifo_buffer
 
 
happens_before
happens_before
 
 
insufficient_lock
insufficient_lock
 
 
kata
kata
 
 
knapsack
knapsack
 
 
lazy_initialization_release_acquire_ordering
lazy_initialization_release_acquire_ordering
 
 
lcs
lcs
 
 
leftpad
leftpad
 
 
library_system
library_system
 
 
linked_list
linked_list
 
 
manual_reset_event
manual_reset_event
 
 
map_reduce
map_reduce
 
 
max
max
 
 
messages
messages
 
 
multple_starting_states
multple_starting_states
 
 
non_atomic_instructions
non_atomic_instructions
 
 
non_deterministic_behavior
non_deterministic_behavior
 
 
operators_and_functions
operators_and_functions
 
 
p_client_server
p_client_server
 
 
p_hello_world
p_hello_world
 
 
p_lang_deadlock_empire_non_atomic_instructions
p_lang_deadlock_empire_non_atomic_instructions
 
 
p_lang_distributed_lock_with_fencing
p_lang_distributed_lock_with_fencing
 
 
p_lang_durable_execution
p_lang_durable_execution
 
 
p_lang_mutex
p_lang_mutex
 
 
p_lang_the_deadlock_empire_boolean_flags
p_lang_the_deadlock_empire_boolean_flags
 
 
p_lang_the_deadlock_empire_confused_counter
p_lang_the_deadlock_empire_confused_counter
 
 
p_lang_the_deadlock_empire_insufficient_lock
p_lang_the_deadlock_empire_insufficient_lock
 
 
p_lang_the_deadlock_empire_simple_counter
p_lang_the_deadlock_empire_simple_counter
 
 
p_lang_worker_machines_with_call_transitions
p_lang_worker_machines_with_call_transitions
 
 
p_worker_machines
p_worker_machines
 
 
procedures
procedures
 
 
process_sets
process_sets
 
 
producer_consumer
producer_consumer
 
 
producer_consumer_variant
producer_consumer_variant
 
 
quint_bank
quint_bank
 
 
quint_bank_16_10_2025
quint_bank_16_10_2025
 
 
quint_booleans_16_10_25
quint_booleans_16_10_25
 
 
quint_checking_properties
quint_checking_properties
 
 
quint_coint_16_10_25
quint_coint_16_10_25
 
 
quint_hello_world_16_10_25
quint_hello_world_16_10_25
 
 
quint_integers_16_10_25
quint_integers_16_10_25
 
 
quint_sets
quint_sets
 
 
relaxed_ordering_total_modification_order
relaxed_ordering_total_modification_order
 
 
release_acquire_ordering
release_acquire_ordering
 
 
semaphores
semaphores
 
 
simple_coin
simple_coin
 
 
simple_counter
simple_counter
 
 
single_decree_paxos
single_decree_paxos
 
 
single_decree_paxos_p_lang
single_decree_paxos_p_lang
 
 
sorting_machine
sorting_machine
 
 
specifying_systems/hour_clock
specifying_systems/hour_clock
 
 
squares
squares
 
 
steveslab_using_quint_to_harden_post
steveslab_using_quint_to_harden_post
 
 
the_barrier
the_barrier
 
 
the_deadlock_empire/fizzbee
the_deadlock_empire/fizzbee
 
 
thread_spawn_and_join_happens_before
thread_spawn_and_join_happens_before
 
 
time_periods
time_periods
 
 
tla_a_caching_memory
tla_a_caching_memory
 
 
tla_a_linearizable_memory
tla_a_linearizable_memory
 
 
tla_alternating_one_bit_clock
tla_alternating_one_bit_clock
 
 
tla_alternation
tla_alternation
 
 
tla_am_pm_hour_clock
tla_am_pm_hour_clock
 
 
tla_and_pluscal_modeling_concurrency_jan_7_2025
tla_and_pluscal_modeling_concurrency_jan_7_2025
 
 
tla_and_pluscal_modeling_message_queues_jan_7_2025
tla_and_pluscal_modeling_message_queues_jan_7_2025
 
 
tla_another_spec
tla_another_spec
 
 
tla_async_interface
tla_async_interface
 
 
tla_await
tla_await
 
 
tla_bnf_grammars
tla_bnf_grammars
 
 
tla_business_logic
tla_business_logic
 
 
tla_cache_invalidation
tla_cache_invalidation
 
 
tla_carbon_credit
tla_carbon_credit
 
 
tla_cascading_failures
tla_cascading_failures
 
 
tla_citadin_counter
tla_citadin_counter
 
 
tla_database_and_blob
tla_database_and_blob
 
 
tla_db_migration
tla_db_migration
 
 
tla_die_hard
tla_die_hard
 
 
tla_die_harder
tla_die_harder
 
 
tla_fairness_10_12_2024
tla_fairness_10_12_2024
 
 

Repository files navigation

About

Studying the use of formal methods to specify distributed systems

Resources

Readme
Activity

Stars

5 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages