{"id":"W2339217994","doi":"10.82308/10549","title":"Verifying finite-state properties of large-scale programs","year":2010,"lang":"en","type":"article","venue":"eScholarship@McGill (McGill)","topic":"Advanced Software Engineering Methodologies","field":"Computer Science","cited_by":18,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Computer science; Programming language; State (computer science); Finite-state machine; AspectJ; Instrumentation (computer programming); Code (set theory); Property (philosophy); Overhead (engineering); Runtime verification; Interface (matter); Program analysis; Software; Set (abstract data type); Operating system; Formal verification; Aspect-oriented programming","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001636143,0.0004197639,0.0005028153,0.000225421,0.0004762033,0.00009350853,0.001686436,0.0002296962,0.00001012939],"category_scores_gemma":[0.00270309,0.0003873982,0.0001905581,0.0007818997,0.0001592567,0.001583346,0.0008893558,0.001194878,0.00006047234],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008969433,"about_ca_system_score_gemma":0.0000333913,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002694983,"about_ca_topic_score_gemma":0.00008039424,"domain_scores_codex":[0.9969206,0.0002464078,0.0006146107,0.0008067598,0.0005607522,0.0008508576],"domain_scores_gemma":[0.9974128,0.0004529144,0.0002717177,0.001324066,0.0003088879,0.0002296278],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00004336645,0.0003775332,0.0001537006,0.0002794534,0.00007349363,0.00006999957,0.00009793257,0.005958496,0.4728954,0.0571539,7.351351e-7,0.462896],"study_design_scores_gemma":[0.001099198,0.0002828448,0.0004051483,0.0002399202,0.00002501571,0.00007324289,0.00008048172,0.003613865,0.9088507,0.0553904,0.0288239,0.001115315],"study_design_candidate":"bench_or_experimental","study_design_consensus":"bench_or_experimental","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9600589,0.0001502444,0.03475349,0.00003275564,0.001640561,0.0004994049,0.00006465733,0.001627652,0.001172394],"genre_scores_gemma":[0.6538351,0.0000200339,0.3457581,0.00006410714,0.00001565247,0.00006158735,0.000003011017,0.00004758022,0.0001948299],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.4617807,"threshold_uncertainty_score":0.9998578,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03812769426984222,"score_gpt":0.2553908144314829,"score_spread":0.2172631201616406,"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."}}