{"id":"W2517913729","doi":"10.1109/csf.2016.24","title":"Runtime Verification of k-Safety Hyperproperties in HyperLTL","year":2016,"lang":"en","type":"article","venue":"","topic":"Security and Verification in Computing","field":"Computer Science","cited_by":62,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Computer science; TRACE (psycholinguistics); Runtime verification; Temporal logic; Information flow; Programming language; Service (business); Theoretical computer science; Distributed computing; Formal verification","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.0003076559,0.00005527384,0.00009213394,0.00008268175,0.00003302961,0.00001716395,0.0004761524,0.00003377322,0.00005130584],"category_scores_gemma":[0.00005367069,0.00003571379,0.00002497028,0.0002498578,0.00004095035,0.0003238022,0.00008081773,0.00003026139,0.00007004118],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002916319,"about_ca_system_score_gemma":0.00003848714,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0000396424,"about_ca_topic_score_gemma":0.00000406757,"domain_scores_codex":[0.9992378,0.00004213257,0.0002834885,0.0001981901,0.0001258193,0.000112602],"domain_scores_gemma":[0.9993587,0.00009306129,0.00006793423,0.0003959593,0.00006202265,0.00002236417],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00002081862,0.0001267483,0.007527313,0.00001492509,0.00000729943,9.215474e-7,0.001442194,0.00004244242,0.07591192,0.6532634,0.0004244806,0.2612175],"study_design_scores_gemma":[0.003128265,0.0002925325,0.2652939,0.0003633994,0.000007893051,0.00003035255,0.0004157786,0.135411,0.4704617,0.02199907,0.1015308,0.001065286],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1278735,0.00008774814,0.853763,0.003309077,0.0002408481,0.000114781,8.984151e-7,0.0001323106,0.01447781],"genre_scores_gemma":[0.9747644,0.00002102206,0.02481893,0.00009921792,0.0000173467,0.000003543867,3.307773e-7,0.000002719634,0.0002724828],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8468909,"threshold_uncertainty_score":0.1456366,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01451861681611869,"score_gpt":0.2142110994329634,"score_spread":0.1996924826168447,"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."}}