{"id":"W3098557859","doi":"10.1145/3368089.3409757","title":"ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code","year":2020,"lang":"en","type":"article","venue":"","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":43,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Equivalence (formal languages); Symbolic execution; Computer science; Symbolic trajectory evaluation; Abstraction; Programming language; Program analysis; Formal equivalence checking; Abstraction model checking; Model checking; Theoretical computer science; Symbolic data analysis; Static analysis; Algorithm; Mathematics; Discrete 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.00986147,0.002245301,0.002013061,0.004196802,0.001483635,0.002908377,0.006040263,0.001896013,0.008468037],"category_scores_gemma":[0.04088115,0.001586834,0.00433795,0.002332539,0.00365809,0.008187623,0.01060769,0.005245195,0.003317409],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001934268,"about_ca_system_score_gemma":0.004104488,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0065219,"about_ca_topic_score_gemma":0.00782364,"domain_scores_codex":[0.9785293,0.006678573,0.00139229,0.003355545,0.008717801,0.001326402],"domain_scores_gemma":[0.9647397,0.01245721,0.001507614,0.01612226,0.004652713,0.0005205032],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0008940438,0.0007507177,0.008142159,0.001391185,0.0005510164,0.000705107,0.001440142,0.1055876,0.03768654,0.1679815,0.01830976,0.6565602],"study_design_scores_gemma":[0.0003102915,0.0005027151,0.001564909,0.0003755412,0.0002825231,0.000444887,0.0003012324,0.6869183,0.03857138,0.2377648,0.03279209,0.0001714516],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.008780707,0.0003535219,0.970327,0.0001765578,0.0001185591,0.0002886982,0.0002138465,0.01709701,0.002644113],"genre_scores_gemma":[0.1678487,0.0003384892,0.8192948,0.0004487628,0.00009583166,0.000596188,0.001758428,0.006118656,0.003500174],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.00986147,"threshold_uncertainty_score":0.05215305,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05157918219343462,"score_gpt":0.3174457627915477,"score_spread":0.2658665805981131,"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."}}