{"id":"W3093567397","doi":"10.1109/eurospw51379.2020.00091","title":"Towards Formal Verification of Program Obfuscation","year":2020,"lang":"en","type":"article","venue":"","topic":"Advanced Malware Detection Techniques","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Computer science; Programming language; Hoare logic; Mathematical proof; Obfuscation; Proof assistant; Formal verification; Semantics (computer science); Formal specification; Formal methods; Theoretical computer science; Program transformation; Transformation (genetics); Correctness; Mathematics","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.006698633,0.0008681494,0.0005831387,0.001195841,0.001037,0.003223613,0.002365059,0.00171302,0.002849368],"category_scores_gemma":[0.01954938,0.001078847,0.002106889,0.0006681739,0.006518447,0.00501352,0.003347832,0.004455912,0.0007099184],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002084014,"about_ca_system_score_gemma":0.00418143,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004474835,"about_ca_topic_score_gemma":0.002416805,"domain_scores_codex":[0.9944272,0.001614542,0.0004919957,0.0006363456,0.002200647,0.0006293372],"domain_scores_gemma":[0.9832259,0.0103245,0.001208855,0.002548517,0.002491355,0.0002007284],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.00008592029,0.0001255948,0.0007407898,0.0004645533,0.00004108626,0.0005312211,0.001415587,0.05830851,0.02221897,0.8937639,0.001396985,0.02090677],"study_design_scores_gemma":[0.0001217297,0.0001344112,0.0002751339,0.000287951,0.00009510131,0.0002948326,0.0003181704,0.3401907,0.06861411,0.5627962,0.02679466,0.0000770627],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"other","genre_scores_codex":[0.005939761,0.0000502865,0.9910396,0.0003109071,0.00003970213,0.00008668071,0.00005879475,0.001118141,0.001356145],"genre_scores_gemma":[0.2965404,0.0005706545,0.6974907,0.0005486688,0.0001178105,0.0005474818,0.0003731837,0.0006325419,0.003178586],"genre_candidate":"other","genre_consensus":null,"teacher_disagreement_score":0.006698633,"threshold_uncertainty_score":0.0354262,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02819997502982263,"score_gpt":0.292323756021341,"score_spread":0.2641237809915183,"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."}}