{"id":"W1987237000","doi":"10.1109/qest.2010.28","title":"Model Checking Randomized Algorithms with Java PathFinder","year":2010,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":11,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"","keywords":"Probabilistic logic; Computer science; Java; Pathfinder; Code (set theory); State (computer science); State space; Algorithm; Bridge (graph theory); Programming language; Statistical model; Artificial intelligence; Mathematics; Statistics","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.00135165,0.0001077318,0.0001982412,0.00006151662,0.00007979218,0.0001201672,0.0006045884,0.00006664206,0.00002290886],"category_scores_gemma":[0.0001219351,0.000070415,0.00005000494,0.000190246,0.00008940699,0.0005853781,0.0001006958,0.0002191562,0.00003108457],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00000974693,"about_ca_system_score_gemma":0.00005998209,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001751285,"about_ca_topic_score_gemma":0.000006129882,"domain_scores_codex":[0.9990192,0.00006829199,0.0001895959,0.000275898,0.000252376,0.0001946397],"domain_scores_gemma":[0.9990501,0.00008583063,0.00008439602,0.0006160683,0.0000982473,0.00006539244],"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.0004558213,0.00004118097,0.00003188071,0.000005455396,0.00001735282,0.000001603297,0.0007922841,0.001241128,0.004649432,0.9358233,0.0000745665,0.056866],"study_design_scores_gemma":[0.01262326,0.00001116333,0.00005460362,0.000003176976,0.000004451731,0.00001097847,0.000006689912,0.9712204,0.007473464,0.008358546,0.0001075581,0.0001256898],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.007054142,0.000004392065,0.9708751,0.0002040868,0.0002847544,0.0002309606,2.079325e-7,0.0002224206,0.02112387],"genre_scores_gemma":[0.1684704,0.00000181328,0.8306431,0.0002195941,0.00003271199,0.0000361938,4.639315e-7,0.000007120722,0.0005885485],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9699793,"threshold_uncertainty_score":0.287144,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02755318015593063,"score_gpt":0.2812277448683242,"score_spread":0.2536745647123936,"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."}}