Completeness Thresholds for Memory Safety of Array Traversing Programs
We report on intermediate results of – to the best of our knowledge – the first study of completeness thresholds for (partially) bounded memory safety proofs. Specifically, we consider heap-manipulating programs that iterate over arrays without allocating or freeing memory. In this setting, we present the first notion of completeness thresholds for program verification which reduce unbounded memory safety proofs to (partially) bounded ones. Moreover, we demonstrate that we can characterise completeness thresholds for simple classes of array traversing programs. Finally, we suggest avenues of research to scale this technique theoretically, i.e., to larger classes of programs (heap manipulation, tree-like data structures), and practically by highlighting automation opportunities.
Sat 17 JunDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:50 | SOAP: Session 4 - Program Verification and Dynamic AnalysisSOAP at Magnolia 18 Chair(s): Liana Hadarean Amazon Web Services | ||
16:00 35mKeynote | Applications of Symbolic ExecutionInvited Talk SOAP William Hallahan Binghamton | ||
16:35 25mTalk | Completeness Thresholds for Memory Safety of Array Traversing Programs SOAP DOI | ||
17:00 25mTalk | Crosys: Cross Architectural Dynamic Analysis SOAP Sangrok Lee The Affiliated Institute of ETRI, Jieun Lee The Affiliated Institute of ETRI, Jaeyong Ko The Affiliated Institute of ETRI, Jaewoo Shim The Affiliated Institute of ETRI DOI | ||
17:25 25mTalk | RaceInjector: Injecting Races to Evaluate and Learn Dynamic Race Detection Algorithms (Virtual) SOAP Michael Wang Massachusetts Institute of Technology, Shashank Srikant MIT, Malavika Samak CSAIL, MIT, Una-May O’Reilly Massachusetts Institute of Technology DOI |