Scalable Certification of Native Code: Experience from Compiling to TALx86 Export

@techreport{citeulike:270557, abstract = {Certifying compilation allows a compiler to produce annotations that prove that target code abides by a specified safety policy. An independent verifier can check the code without needing to trust the compiler. For such a system to be generally useful, the safety policy should be expressive enough to allow different compilers to effectively produce certifiable code.}, author = {Grossman, Dan and Morrisett, Greg}, citeulike-article-id = {270557}, citeulike-linkout-0 = {http://citeseer.ist.psu.edu/704364.html}, citeulike-linkout-1 = {http://citeseer.lcs.mit.edu/704364.html}, citeulike-linkout-2 = {http://citeseer.ifi.unizh.ch/704364.html}, citeulike-linkout-3 = {http://citeseer.comp.nus.edu.sg/704364.html}, keywords = {typed-assembly-language}, month = {February,}, number = {TR2000-1783}, posted-at = {2005-08-01 05:49:25}, priority = {2}, title = {Scalable Certification of Native Code: Experience from Compiling to TALx86}, url = {http://citeseer.ist.psu.edu/704364.html}, year = {2000} }

TY - RPRT ID - citeulike:270557 L3 - citeulike-article-id:270557 N2 - Certifying compilation allows a compiler to produce annotations that prove that target code abides by a specified safety policy. An independent verifier can check the code without needing to trust the compiler. For such a system to be generally useful, the safety policy should be expressive enough to allow different compilers to effectively produce certifiable code. IS - TR2000-1783 TI - Scalable Certification of Native Code: Experience from Compiling to TALx86 KW - typed-assembly-language AU - Grossman, Dan AU - Morrisett, Greg PY - 2000/2,// UR - http://citeseer.ist.psu.edu/704364.html ER -