{"id":"W1997553387","doi":"10.1007/s00165-012-0252-5","title":"Proving termination of nonlinear command sequences","year":2012,"lang":"en","type":"article","venue":"Formal Aspects of Computing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Theory of computation; Nonlinear system; Simple (philosophy); Computer science; Algorithm; Divergence (linguistics); Class (philosophy); Loop (graph theory); Variable (mathematics); Mathematics; Theoretical computer science; Artificial intelligence; Mathematical analysis; Combinatorics","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.003008884,0.0008083038,0.0007034034,0.0007460396,0.00105321,0.001297184,0.001529122,0.0007583209,0.003651333],"category_scores_gemma":[0.01610241,0.0003395333,0.0008752471,0.0003807853,0.004880088,0.002219885,0.002487639,0.001778051,0.0008016499],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001554532,"about_ca_system_score_gemma":0.001934592,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003310635,"about_ca_topic_score_gemma":0.001974845,"domain_scores_codex":[0.9955536,0.001122832,0.0002193582,0.0004969435,0.002094917,0.0005124597],"domain_scores_gemma":[0.9862163,0.009127734,0.0007756332,0.001388721,0.002170648,0.0003209872],"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.001251393,0.0004349089,0.01027731,0.000619721,0.0001160733,0.001718109,0.002132097,0.1904949,0.1357505,0.4930985,0.004117025,0.1599894],"study_design_scores_gemma":[0.0001018815,0.0001826299,0.0005888321,0.00005325086,0.00002934007,0.0001997413,0.0001337083,0.7202342,0.09681395,0.1774649,0.00415858,0.00003906378],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.09045764,0.00003857705,0.9015779,0.0001769026,0.00003122557,0.0001141606,0.00008087272,0.002426678,0.005096084],"genre_scores_gemma":[0.8089403,0.00005477861,0.1864463,0.0001563041,0.00003005438,0.0001346309,0.0002060599,0.0003835926,0.003648007],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.003651333,"threshold_uncertainty_score":0.01591271,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02360080994626788,"score_gpt":0.297527706928594,"score_spread":0.2739268969823261,"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."}}