Our Contributions A simple program logic (SCAP)for modular verification of (1)compiled C code &(2)manually-written assembly code Stack-Based Reasoning Definition Control Abstraction System Formalization function call/return SCAP SEC 4 tail call optimization [34,8] SCAP SEC 4.3 All systems are lemma libraries built on a single CAPO framework! multi-return function call [32] SCAP-II SEC 5.2 weak continuation [30] SCAP-IΠ SEC 5.2 setjmp/longjmp [20] SCAP-II SEC 5.3 coroutines [10] CAP-CR SEC 6.1 coroutines function call [10] SCAP-CR SEC 6.2 threads [15] FCCAP TR [13]No ’s! Our Contributions A simple program logic (SCAP) for modular verification of (1) compiled C code & (2) manually-written assembly code All systems are lemma libraries built on a single CAP0 framework!