{"id":"W4404986931","doi":"10.1109/tse.2025.3631361","title":"Portus: Linking Alloy with SMT-based Finite Model Finding","year":2025,"lang":"en","type":"preprint","venue":"IEEE Transactions on Software Engineering","topic":"Aluminum Alloy Microstructure Properties","field":"Engineering","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia; University of Waterloo","funders":"Natural Sciences and Engineering Research Council of Canada; Alliance de recherche numérique du Canada","keywords":"Alloy; Computer science; Business; Materials science; Metallurgy","routes":{"ca_aff":true,"ca_fund":true,"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","research_integrity"],"consensus_categories":[],"category_scores_codex":[0.0001392145,0.001025169,0.0007336681,0.0008246885,0.0001783218,0.0001778827,0.0005710809,0.0007141144,0.00004027397],"category_scores_gemma":[0.00002555633,0.001061846,0.0003190349,0.0003844026,0.0000526708,0.0001748488,0.00001262858,0.002468701,0.00001462906],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005581541,"about_ca_system_score_gemma":0.0002891408,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001719946,"about_ca_topic_score_gemma":0.00002452829,"domain_scores_codex":[0.9974572,0.00001819669,0.000608143,0.0007485208,0.0004409799,0.0007269685],"domain_scores_gemma":[0.9983971,0.000313155,0.00008506019,0.0009101022,0.0001215378,0.000173091],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00003390937,0.00002422358,0.00002289787,0.001574709,0.0003510897,0.0000252243,0.0003498795,0.9944524,0.001041999,0.000005121261,0.00003356238,0.002084987],"study_design_scores_gemma":[0.0004461269,0.00003714835,0.00001152431,0.002583146,0.000222982,0.00000678901,0.00001397493,0.9599358,0.0353624,0.00001423712,0.0002928361,0.00107298],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01571904,0.0004216144,0.9767015,0.0000154458,0.002034558,0.0005554991,0.0004406516,0.00404253,0.0000691879],"genre_scores_gemma":[0.8356336,0.00008357341,0.1630182,0.00007828433,0.0001016264,0.0003249185,0.00006700812,0.0002910726,0.0004017601],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8199145,"threshold_uncertainty_score":0.9998326,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01443710603047649,"score_gpt":0.2063790920354117,"score_spread":0.1919419860049352,"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."}}