{"id":"W4229576726","doi":"10.1145/1273442.1250769","title":"Path invariants","year":2007,"lang":"en","type":"article","venue":"ACM SIGPLAN Notices","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":25,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Predicate abstraction; Computer science; Predicate (mathematical logic); Path (computing); Abstract interpretation; Program analysis; Theoretical computer science; Abstraction; Counterexample; Spurious relationship; Path expression; Programming language; Control flow; Invariant (physics); Control flow graph; Algorithm; Model checking; Mathematics; Discrete mathematics","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.002803969,0.001271902,0.0007840893,0.003249449,0.001321539,0.002337967,0.002733072,0.001348123,0.008930077],"category_scores_gemma":[0.01497539,0.0009156644,0.003014223,0.001655109,0.002554366,0.006534007,0.003148219,0.002803004,0.002290304],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001541701,"about_ca_system_score_gemma":0.002571089,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0025947,"about_ca_topic_score_gemma":0.002482216,"domain_scores_codex":[0.994474,0.000694861,0.0004505642,0.001181362,0.002621394,0.0005777342],"domain_scores_gemma":[0.9894488,0.005622629,0.001043153,0.002129681,0.001614077,0.0001417568],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0003313589,0.0001805638,0.005438176,0.0009119064,0.0001407586,0.001008316,0.000918591,0.05496548,0.01772651,0.690479,0.01156424,0.2163351],"study_design_scores_gemma":[0.00008491321,0.0001970687,0.001773562,0.0002487481,0.0002703215,0.0007713187,0.0002394319,0.2367337,0.05995672,0.6312364,0.0683504,0.0001374455],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.007987701,0.0001349223,0.9819459,0.0001901536,0.00006682763,0.0002424461,0.0008771046,0.0035353,0.005019528],"genre_scores_gemma":[0.1975226,0.0005107875,0.7898023,0.0003187349,0.0001276303,0.0007550376,0.003447308,0.001363381,0.006152249],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.008930077,"threshold_uncertainty_score":0.02987415,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04224519862286649,"score_gpt":0.3124832385447945,"score_spread":0.2702380399219281,"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."}}