{"id":"W4308078800","doi":"10.1109/icsess54813.2022.9930214","title":"A Model-Checking Framework for the Verification of Move Smart Contracts","year":2022,"lang":"en","type":"article","venue":"","topic":"Blockchain Technology Applications and Security","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Model checking; Vulnerability (computing); Formal verification; Function (biology); Exploit; Popularity; Distributed ledger; Core (optical fiber); Computer security; Distributed computing; Smart contract; Software engineering; Programming language; Blockchain","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0003430566,0.00004129134,0.00006319008,0.00003072093,0.0002946722,0.00001378136,0.0007447146,0.00003935562,0.000009157218],"category_scores_gemma":[0.00004130851,0.00003197737,0.00003745014,0.0002303019,0.0000362454,0.00004054795,0.0001846664,0.0001458005,7.827157e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000168546,"about_ca_system_score_gemma":0.00003189204,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001256735,"about_ca_topic_score_gemma":0.000002351891,"domain_scores_codex":[0.9995129,0.00001316558,0.0001215576,0.0001567029,0.00009913062,0.00009660148],"domain_scores_gemma":[0.9990342,0.0002438869,0.00008164881,0.0005820846,0.00004676474,0.00001136201],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000002013935,0.00003683289,0.00002399675,0.000001465364,0.000006327329,3.644787e-8,0.0002834377,0.002391601,0.0003266481,0.980079,0.0001875186,0.01666112],"study_design_scores_gemma":[0.00005502063,0.00001226522,0.000192203,6.555912e-7,0.000002657367,9.792569e-7,0.00006329917,0.6692492,0.001655583,0.3251797,0.003558283,0.00003008201],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.006169582,0.0001157888,0.9864413,0.006521504,0.00005391224,0.0003110264,0.000006529466,0.00009390987,0.0002864728],"genre_scores_gemma":[0.8260426,0.000005113254,0.1730825,0.0004234437,0.00000524486,0.0003941478,0.000001147339,0.000002447497,0.00004335768],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.819873,"threshold_uncertainty_score":0.226641,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02870296921507702,"score_gpt":0.2675425272831928,"score_spread":0.2388395580681158,"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."}}