{"id":"W14931976","doi":"","title":"Partial-order verification in SPIN can be more efficient","year":2002,"lang":"en","type":"article","venue":"Zahnarztliche Welt","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Partial order reduction; Model checking; Computer science; Reduction (mathematics); Concurrency; Set (abstract data type); Programming language; Formal verification; Linear temporal logic; Temporal logic; High-level verification; Algorithm; Theoretical computer science; Mathematics; Software","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.0006334005,0.0001814415,0.0001772021,0.0001955757,0.0001066635,0.0001030973,0.0008884546,0.0001217982,0.00008550598],"category_scores_gemma":[0.0002667625,0.0001842826,0.00004919784,0.001186867,0.00008040979,0.0002367348,0.0001374805,0.0002236892,0.0001908185],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001535391,"about_ca_system_score_gemma":0.00003204829,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001493379,"about_ca_topic_score_gemma":0.00002111719,"domain_scores_codex":[0.9980993,0.000172354,0.0003929296,0.0005318265,0.0003901664,0.0004133823],"domain_scores_gemma":[0.9985185,0.00004826301,0.0001406828,0.00109324,0.00008909224,0.0001102109],"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.00007027237,0.002476913,0.007899798,0.0001939064,0.00006500463,0.00008985132,0.05808834,0.05817552,0.03654915,0.5542499,0.01506562,0.2670757],"study_design_scores_gemma":[0.0004194238,0.00006180466,0.01538501,0.00002141813,0.000004615452,0.00001234005,0.0001309116,0.947418,0.01676911,0.0001311131,0.01934584,0.0003003834],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.464825,0.0003820551,0.5080467,0.01748979,0.001159755,0.0008509126,0.000007497654,0.000675869,0.006562342],"genre_scores_gemma":[0.8210975,0.00002853667,0.1772373,0.001063537,0.00007145097,0.00009807137,0.000006366616,0.00001951282,0.000377706],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8892425,"threshold_uncertainty_score":0.7514826,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04558110259136665,"score_gpt":0.3031753412705201,"score_spread":0.2575942386791535,"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."}}