{"id":"W4411271981","doi":"10.1109/icse-companion66252.2025.00061","title":"Structured State Space Exploration of Dash+ Models","year":2025,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Dash; Computer science; Space (punctuation); State (computer science); Space exploration; Aerospace engineering; Engineering; Programming language; Operating system","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.0002282169,0.00005186161,0.0000753227,0.00009426212,0.00002772594,0.00003368607,0.0003824756,0.00002483,0.000004235592],"category_scores_gemma":[0.00003511293,0.00004558488,0.00001892696,0.0003888646,0.0000204814,0.001408411,0.00009835103,0.00004097196,0.000003316251],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001937481,"about_ca_system_score_gemma":0.00004509138,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000199438,"about_ca_topic_score_gemma":0.000005867797,"domain_scores_codex":[0.9994292,0.00005579958,0.0001604638,0.0001509259,0.0001219482,0.00008172277],"domain_scores_gemma":[0.9993672,0.00002424277,0.00006389506,0.0004341196,0.00009400725,0.00001653349],"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.000003218528,0.000006641963,0.00001061367,0.00001044922,0.000003801538,8.426173e-8,0.0004871671,0.009705575,0.003367339,0.9542741,0.0001794662,0.0319515],"study_design_scores_gemma":[0.00006903608,0.00001221334,0.0002370056,0.000005635016,0.000001117336,1.530953e-7,0.00002512481,0.5456305,0.1254427,0.3283194,0.00022055,0.0000365817],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.003629651,0.00001946166,0.9814672,0.0003526558,0.0002565634,0.0001045634,7.419517e-7,0.00008395206,0.01408517],"genre_scores_gemma":[0.3056706,0.000007959602,0.6933594,0.00005853739,0.000003133017,0.000005085652,6.873379e-7,0.000001445353,0.000893203],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6259547,"threshold_uncertainty_score":0.1858898,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0522554194748681,"score_gpt":0.3197338185893923,"score_spread":0.2674783991145241,"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."}}