MARC

 008250123s2024        us                              c    eng  d
■001000017164594
■00520250211153020
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798346759416
■035    ▼a(MiAaPQ)AAI31631902
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a004
■1001  ▼aKorkut,  Joomy.▼0(orcid)0000-0001-6784-7108
■24510▼aForeign  Function  Verification  Through  Metaprogramming
■260    ▼a[Sl]▼bPrinceton  University▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a165  p
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  86-06,  Section:  B.
■500    ▼aAdvisor:  Appel,  Andrew  W.
■5021  ▼aThesis  (Ph.D.)--Princeton  University,  2024.
■520    ▼aCertiCoq  is  a  compiler  from  Coq  to  C  that  is  verified  in  Coq.  Thanks  to  CertiCoq's  mechanically  checked  proof  of  compiler  correctness,  users  can  be  sure  that  programs  they  write  and  verify  in  Coq's  rich  type  system  output  the  same  results  when  compiled  to  C  (and  to  machine  language,  via  the  CompCert  verified  compiler).  However,  in  practice,  large  programs  are  rarely  written  in  a  single  language;  additional  languages  are  used  for  better  performance  or  for  capabilities  that  the  primary  language  lacks.  In  particular,  because  Coq  lacks  user-defined  primitive  types,  mutation,  and  input/output  actions,  CertiCoq-compiled  code  must  interact  with  another  language  to  have  those  capabilities.  Specifically,  Coq  code  must  be  able  to  call  C  code  and  C  code  must  be  able  to  inspect  and  generate  Coq  values  and  call  Coq  code.  But  what  happens  to  the  correctness  proofs  when  these  two  languages  interact?A  foreign  C  function  has  to  be  memory-safe,  return  the  expected  result,  and  have  only  the  expected  side  effect.  A  specification  that  expresses  these  requirements  must  combine  plain  Coq,  for  the  functional  parts,  and  a  program  logic  for  C  (such  as  the  Verified  Software  Toolchain  [VST]),  for  the  verification  of  C  functions.  While  VST  is  embedded  in  Coq,  its  specification  language  is  quite  different.  VST  proofs  about  C  foreign  functions  do  not  directly  translate  to  proofs  about  Coq  primitives  either.  Bridging  this  gap  by  connecting  plain  Coq  and  VST  theorems  requires  a  system  of  techniques  and  methods,  many  of  which  are  made  feasible  by  using  metaprogramming  as  a  general  methodological  approach.  In  this  dissertation,  I  describe  these  techniques  and  methods.  Using  these  methods,  the  user  can  relate  foreign  functions  and  types  to  their  functional  models,  generate  VST  specifications  about  the  foreign  C  functions,  and  write  plain  Coq  proofs  about  the  Coq  counterparts  of  the  foreign  functions.  I  also  provide  examples  of  Coq  programs  with  primitive  types,  mutation,  and  I/O  actions,  along  with  specifications  and  proofs  about  these  programs,  to  demonstrate  VeriFFI,  the  verified  foreign  function  interface  for  CertiCoq.
■590    ▼aSchool  code:  0181.
■650  4▼aComputer  science
■650  4▼aComputer  engineering
■650  4▼aSystems  science
■653    ▼aCompilers
■653    ▼aForeign  function  interfaces
■653    ▼aFormal  verification
■653    ▼aInteractive  theorem
■653    ▼aMetaprogramming
■690    ▼a0984
■690    ▼a0464
■690    ▼a0790
■71020▼aPrinceton  University▼bComputer  Science.
■7730  ▼tDissertations  Abstracts  International▼g86-06B.
■790    ▼a0181
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17164594▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

Preview

Export

ChatGPT Discussion

AI Recommended Related Books