Yanyan's Wiki 操作系统 (2023)

A List of Papers

Reading papers may be hard, especially when essential background knowledge is missing. Ask your advisor (or peers) for help.

Studies

  1. setuid demystified. USENIX Security'02.
  2. Learning from mistakes — A comprehensive study on real world concurrency bug characteristics. ASPLOS'08.
  3. Understanding integer overflow in C/C++. ICSE'12.
  4. All file systems are not created equal: On the complexity of crafting crash-consistent applications. OSDI'14.
  5. Ad hoc transactions in Web applications: The good, the bad, and the ugly. SIGMOD'22.

Compilers

  1. LLVM: A compilation framework for lifelong program analysis & transformation. CGO'04.
  2. QEMU, a fast and portable dynamic translator. USENIX ATC'05.
  3. Stochastic superoptimization. ASPLOS'13.
  4. Copy-and-patch compilation: A fast compilation algorithm for high-level languages and bytecode. OOPSLA'21.

Static Analysis and Checking

  1. Bugs as deviant behavior: A general approach to inferring errors in systems code. SOSP'01.
  2. Finding bugs is easy. OOPSLA'04.
  3. Pointer Analysis. NOW Books, 2015.

Dynamic Analysis and Trace

  1. Efficient path profiling. MICRO'96.
  2. ReVirt: Enabling intrusion analysis through virtual-machine logging and replay. OSDI'02.
  3. Valgrind: A framework for heavyweight dynamic binary instrumentation. PLDI'07.
  4. FastTrack: Efficient and precise dynamic race detection. PLDI'09.
  5. AddressSanitizer: A fast address sanity checker. USENIX ATC'12.

Debugging

  1. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering (TSE), 28(2), 2002.
  2. Bug isolation via remote program sampling. PLDI'03.
  3. Repair of boolean programs with an application to C. CAV'06.
  4. Automatically finding patches using genetic programming. ICSE'09.

Testing and Validation

  1. EXPLODE: A lightweight, general system for finding serious storage system errors. OSDI'06.
  2. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI'08.
  3. CrystalBall: Predicting and preventing inconsistencies in deployed distributed systems. NSDI'09.
  4. Compiler validation via equivalence modulo inputs. PLDI'14.
  5. IJON: Exploring deep state spaces via fuzzing. SP'20.

Verification

  1. The existence of refinement mappings. Theoretical Computer Science (TCS), 82(2), 1991.
  2. Proof-carrying code. POPL'97.
  3. Model checking for programming languages using VeriSoft. POPL'97.
  4. An extensible SAT-solver. SAT'03.
  5. Hyperkernel: Push-button verification of an OS kernel. SOSP'17.

Synthesis

  1. Synthesis: Dreams $\Rightarrow$ programs. IEEE Transactions on Software Engineering (TSE), 5(4), 1979.
  2. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering (TSE), 27(2), 2001.
  3. Combinatorial sketching for finite programs. ASPLOS'06.
  4. Scaling enumerative program synthesis via divide and conquer. TACAS'17.
  5. Multi-modal program inference: A marriage of pre-trained language models and component-based synthesis. OOPSLA'21.
Creative Commons License    苏 ICP 备 2020049101 号