SURVEY:SUMMARY:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] not_applicable SURVEY:SUMMARY:CLASSIFICATION[practical,theoretical,hardware] practical SURVEY:SUMMARY:CORRECT_CODE_LOCATION[string] SURVEY:SUMMARY:PUBLISHED_CODE[not_applicable, yes, no] no SURVEY:SUMMARY:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] not_applicable SURVEY:SUMMARY:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] not_applicable SURVEY:AUTHOR1:BUILD_COMMENT[string] SURVEY:AUTHOR1:BUILD_DIFFICULTY[not_applicable, reasonable_effort, code_problematic or string] not_applicable SURVEY:AUTHOR1:BUILD_DIFFICULTY_COMMENT[string] none SURVEY:AUTHOR1:CLASSIFICATION[practical,theoretical,hardware] practical SURVEY:AUTHOR1:CLASSIFICATION_COMMENT[string] SURVEY:AUTHOR1:CORRECT_CODE_LOCATION[string] SURVEY:AUTHOR1:PUBLIC_COMMENT[string] Large percentage of the work associated to this paper is theoretical. The details of the soundness proof and formalisation is available in the technical report. The code is part of a confidential project that has not been disclosed by Microsoft. I hope that that project will be open-sourced. SURVEY:AUTHOR1:PUBLISHED_CODE[not_applicable, yes, no] no SURVEY:AUTHOR1:SAME_VERSION[not_applicable, yes, no_but_available, no_and_not_available] not_applicable SURVEY:AUTHOR1:SAME_VERSION_COMMENT[string] none SURVEY:AUTHOR1:STUDY_FOUND_CORRECT_CODE[not_applicable, yes, no] not_applicable