Sertifitseeritud kood: linke

Sissejuhatusi

• Proof-Carrying Code (Peter Lee's page) (aegunud)
• Proof-Carrying Code (George Necula's page) (aegunud)
• Greg Morrisett's 2004 course on language-based security

Projekte

• The ConCert Project at CMU
• The Fox Project at CMU
• Language-based security at Cornell
• Typed Assembly Language (TAL)
• The TILT Compiler Project at Cornell
• PCC at Princeton
• The FLINT Project at Yale
• The MRG Project at Edinburgh/LMU

Inimesi

• Andrew Appel
• Karl Crary
• Amy Felty
• Robert Harper
• Peter Lee
• Greg Morrisett
• George Necula
• Frank Pfenning
• David Walker
• Zhong Shao

Seminariteemasid

• Programmiloogikad: Hoare'i loogika, nõrgima eeltingimuse arvutus
• A Poetzsch-Heffter, P Müller, A programming logic for sequential Java, ESOP'99
• Baitkoodiloogikad
• C Quigley, A programming logic for Java bytecode programs, TPHOLs'03/PhD'04
• N Benton, A typed logic for stacks and jumps, draft
• Tüübisüsteemid
• B Pierce, Foundational calculi for programming languages, CRC Handbook of CS&E
• L Cardelli, Type systems, CRC Handbook of CS&E
• Turvatüübid
• D Volpano, G Smith, A type-based approach to program security, TAPSOFT'97
• Tüübid ressursijuhtimises
• Loogilised raamvärgid, LF
• R Harper, F Honsell, G Plotkin, A framework for defining logics, LICS'87/JACM'93
• F Pfenning, Elf: a language for logic definition and verified meta-programming, LICS'89
• F Pfenning, Logical Frameworks, Handbook of Autom Reasoning '01
• Kokkuvõtvalt PCCst ja tüübitud assemblerist
• C Colby, K Crary, R Harper, P Lee, F Pfenning, Automated techniques for provably safe mobile code, TCS'03
• Konventsionaalne PCC
• G C Necula, Proof-carrying code, POPL'97
• G C Necula, P Lee, The design and implementation of a certifying compiler, PLDI'98
• C Colby, P Lee, G C Necula, F Blau, M Plesko, K Cline, A certifying compiler for Java, PLDI'00
• Foundational PCC
• A W Appel, A P Felty, A semantic model of types and machine instructions for proof-carrying code, POPL'00
• A W Appel, Foundational proof-carrying code, LICS'01
• Oraaklistringid
• G C Necula, S P Rahul, Oracle-based checking of untrusted software, POPL'01
• Temporal logic PCC
• A Bernard, P Lee, Temporal logic for proof-carrying code, CADE'02
• Typed Assembly Language
• G Morrisett, D Walker, K Crary, N Glew, From System F to Typed Assembly Language, POPL'98/TOPLAS'99
• G Morrisett, K Crary, N Glew, D Grossman, R Samuels, F Smith, D Walker, S Weirich, S Zdancewic, TALx86: a realistic typed assembly language, WCSSS'99
• Lightweight bytecode verification
• E Rose, K H Rose, Lightweight bytecode verification, OOPSLA'98 WS/ JAR'03