{"id":"W2091682271","doi":"10.1145/2767133","title":"SMT-Based Synthesis of Distributed Self-Stabilizing Systems","year":2015,"lang":"en","type":"article","venue":"ACM Transactions on Autonomous and Adaptive Systems","topic":"Distributed systems and fault tolerance","field":"Computer Science","cited_by":14,"is_retracted":false,"has_abstract":true,"ca_institutions":"McMaster University","funders":"","keywords":"Computer science; Mutual exclusion; Self-stabilization; Asynchronous communication; Correctness; Distributed computing; Token ring; Dijkstra's algorithm; Security token; Suzuki-Kasami algorithm; Distributed algorithm; Protocol (science); Matching (statistics); Set (abstract data type); State (computer science); Topology (electrical circuits); Theoretical computer science; Graph; Algorithm; Computer network; Shortest path problem; Mathematics","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0006295068,0.0004672142,0.0004079035,0.0004799631,0.0004407886,0.0005528147,0.000653929,0.0004608141,0.002660875],"category_scores_gemma":[0.00169689,0.0002760447,0.0006444771,0.000303785,0.000723926,0.0004666701,0.0009322944,0.000592162,0.0005075553],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006482827,"about_ca_system_score_gemma":0.0007717906,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0006374628,"about_ca_topic_score_gemma":0.001085852,"domain_scores_codex":[0.999447,0.0001305123,0.00005134291,0.00009455356,0.0002286132,0.00004793131],"domain_scores_gemma":[0.9992548,0.0003247716,0.0000755841,0.0001403207,0.0001767068,0.00002788704],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0001166023,0.00007023825,0.0005620553,0.0003724381,0.00004670442,0.0003682444,0.0003206162,0.6809636,0.07371645,0.1434901,0.001713565,0.09825949],"study_design_scores_gemma":[0.00004237512,0.0000648198,0.00007106458,0.00002855749,0.00002003282,0.00005659741,0.00003449958,0.9320256,0.02575422,0.03352113,0.008371582,0.000009426265],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01473889,0.00008018268,0.9778211,0.00008160352,0.00004663764,0.00008233827,0.00007914558,0.0009972993,0.00607285],"genre_scores_gemma":[0.4736461,0.0001523482,0.5221102,0.00006448152,0.00002534255,0.0003343789,0.0002371632,0.0002288315,0.003201146],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.002660875,"threshold_uncertainty_score":0.008901477,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03194881532200321,"score_gpt":0.2374703559030241,"score_spread":0.2055215405810208,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}