{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006002662,0.001889978,0.001367276,0.002257863,0.001009759,0.003064978,0.003567723,0.001967147,0.00334096],"category_scores_gemma":[0.02759711,0.001552007,0.004435119,0.001180681,0.006059153,0.006098304,0.005425289,0.006036411,0.0008191827],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002407156,"about_ca_system_score_gemma":0.003329489,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01070486,"about_ca_topic_score_gemma":0.008783537,"domain_scores_codex":[0.9910738,0.002973663,0.0005756523,0.001459638,0.002971653,0.0009456669],"domain_scores_gemma":[0.9844707,0.009498812,0.001254521,0.003072662,0.001360307,0.0003430102],"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.0005528093,0.0004137938,0.004844114,0.0005813499,0.0002803383,0.001219593,0.001039234,0.420784,0.02296928,0.4538433,0.006226123,0.08724606],"study_design_scores_gemma":[0.000138833,0.0001185829,0.0002475188,0.00009759732,0.00007737744,0.0001956847,0.00005035795,0.7539724,0.02145763,0.2178432,0.0057248,0.0000760117],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0139612,0.00006010097,0.9800299,0.0003351716,0.00005628878,0.00007850465,0.00006783639,0.004371301,0.001039625],"genre_scores_gemma":[0.3146415,0.000215471,0.6802527,0.0005662782,0.00008322825,0.0003389744,0.0003412231,0.001494776,0.002065849],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01070486,"threshold_uncertainty_score":0.03174549,"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."}}