{"id":"W4250193792","doi":"10.1109/gas.2013.6632584","title":"Towards model checking of computer games with Java PathFinder","year":2013,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"York University","funders":"","keywords":"Computer science; Java; Pathfinder; Programming language; Model checking; Code (set theory); State (computer science); Space (punctuation); Source code; State space; Operating system; World Wide Web; Mathematics; Set (abstract data type)","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.000213755,0.00008955317,0.0001212101,0.00005919267,0.00002795275,0.00006755564,0.0005419381,0.00004051421,0.00003046428],"category_scores_gemma":[0.000008879585,0.00006235842,0.0000275597,0.0001838473,0.00004678647,0.0007194534,0.0001562785,0.00006663852,0.00002996039],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001663704,"about_ca_system_score_gemma":0.00004965628,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006553469,"about_ca_topic_score_gemma":0.000001010824,"domain_scores_codex":[0.9991835,0.00003209015,0.0001799713,0.0002126491,0.0002323121,0.0001594535],"domain_scores_gemma":[0.9992042,0.00001673864,0.00008686804,0.0004856167,0.0001608285,0.0000457693],"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.00000411302,0.00009702577,0.0008525665,0.00004508197,0.00002587559,6.94655e-7,0.002199876,0.01927091,0.002585319,0.5076097,0.001203084,0.4661058],"study_design_scores_gemma":[0.0001137524,0.00005993635,0.007523338,0.00001276729,0.000001656103,0.00000374354,0.00001390281,0.9757495,0.01264501,0.003727556,0.0000510259,0.00009782915],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02904038,0.000007560898,0.9606411,0.0001734795,0.00007536205,0.0001341079,2.167989e-7,0.00009624266,0.009831498],"genre_scores_gemma":[0.3515052,0.000001309203,0.6481495,0.0001801094,0.00001288334,0.00001023841,2.372372e-7,0.000004050364,0.0001364298],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9564786,"threshold_uncertainty_score":0.2542903,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03259177534948429,"score_gpt":0.2648165694368518,"score_spread":0.2322247940873675,"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."}}