{"id":"W1965117069","doi":"10.1145/2070336.2070357","title":"Enhancing spark's contract checking facilities using symbolic execution","year":2011,"lang":"en","type":"article","venue":"ACM SIGAda Ada Letters","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Symbolic execution; SPARK (programming language); Software engineering; Usability; Programming language; Automation; Design by contract; Software; Model checking; Formal methods; Software development; Software construction; Operating system; Engineering","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.0004274587,0.0002322444,0.0002369738,0.0001618429,0.0002311758,0.0001537665,0.001129902,0.00007785767,0.00001645273],"category_scores_gemma":[0.0006658025,0.0002353335,0.00008849719,0.0002667883,0.00008096747,0.0006870411,0.0003569728,0.0002240853,0.00001649797],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001108538,"about_ca_system_score_gemma":0.00005834852,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002534472,"about_ca_topic_score_gemma":0.0000192405,"domain_scores_codex":[0.9983309,0.00008130987,0.0003205443,0.0004564108,0.0003170657,0.0004938057],"domain_scores_gemma":[0.9983162,0.0003672179,0.0001606518,0.001000208,0.00006111559,0.00009460219],"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.00006784341,0.0002793124,0.06071586,0.0003747757,0.0002516285,0.0008546796,0.05269439,0.0003116131,0.8082952,0.008330189,0.01831818,0.0495063],"study_design_scores_gemma":[0.001228695,0.0003122605,0.03805285,0.001617564,0.0001034061,0.0006850293,0.0003126153,0.03913156,0.8567352,0.05570467,0.002881142,0.003235026],"study_design_candidate":"bench_or_experimental","study_design_consensus":"bench_or_experimental","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.5225955,0.00007852902,0.4722466,0.0003226624,0.0003216614,0.0001093473,0.000001216757,0.004124087,0.0002004109],"genre_scores_gemma":[0.7346786,0.000002133751,0.2635339,0.001669248,0.00007775585,0.0000109367,0.000001140761,0.00001459841,0.00001171913],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.2120831,"threshold_uncertainty_score":0.9596623,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06601541650421534,"score_gpt":0.2562466960245205,"score_spread":0.1902312795203052,"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."}}