{"id":"W2135655782","doi":"10.1109/hldvt.2000.889562","title":"Compositional verification of an ATM switch module using interface recognizer/suppliers (IRS)","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Montréal","funders":"","keywords":"Interface (matter); Computer science; Automaton; Programming language; Model checking; Application programming interface; Distributed computing; Embedded system; Theoretical computer science; Parallel computing","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.0003693884,0.0001067602,0.0001297771,0.00009936555,0.00009416521,0.00005952527,0.0006305767,0.00006636295,0.0001786783],"category_scores_gemma":[0.00003370511,0.0001086572,0.00004007734,0.0003401747,0.00006260289,0.001024346,0.00008385296,0.00009393585,0.00006047632],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008829116,"about_ca_system_score_gemma":0.00001772501,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003014013,"about_ca_topic_score_gemma":0.000001249298,"domain_scores_codex":[0.9988168,0.0001105967,0.0003163912,0.0003277621,0.0002624544,0.0001660302],"domain_scores_gemma":[0.9989816,0.00004028231,0.0001594245,0.0006045518,0.0001414641,0.0000727045],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00003782054,0.0006342119,0.0003906502,0.00005462625,0.00004164837,0.000001782455,0.002076074,0.008663132,0.6997494,0.1579965,0.0005622642,0.1297919],"study_design_scores_gemma":[0.0001500178,0.00006773872,0.0009643685,0.00001048814,0.000004079267,0.00001594686,0.00003324315,0.7822052,0.2150825,0.00113685,0.0002166007,0.0001129996],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.2541934,0.00002256496,0.7426168,0.00009977425,0.0002100675,0.0001141102,0.000002903513,0.00008875424,0.002651577],"genre_scores_gemma":[0.4760535,0.000003417942,0.5238187,0.00003742889,0.00001764665,0.000003954111,0.00000316212,0.000004956802,0.00005727402],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7735421,"threshold_uncertainty_score":0.4430912,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0702460859643823,"score_gpt":0.3131514938470953,"score_spread":0.242905407882713,"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."}}