# PL Some resources about PL(verification). ## Conferences [Most Influential POPL Paper Award](https://www.sigplan.org/Awards/POPL/) [Most Influential PLDI Paper Award](https://www.sigplan.org/Awards/PLDI/) ## Courses [软件理论基础与实践](https://xiongyingfei.github.io/SF/2021/lectures.html) [Formal Semantics of Programming Languages](https://cs.nju.edu.cn/hongjin/teaching/semantics/index.htm) [Principles of Computer Systems](https://6826.csail.mit.edu/2020/) ## Papers [Finding and understanding bugs in C compilers](https://dl.acm.org/doi/10.1145/1993498.1993532) [Scaling symbolic evaluation for automated verification of systems code with Serval](https://unsat.cs.washington.edu/papers/nelson-serval.pdf) [Using concurrent relational logic with helpers for verifying the AtomFS file system](https://dl.acm.org/doi/10.1145/3341301.3359644) [A lightweight symbolic virtual machine for solver-aided host languages](https://dl.acm.org/doi/10.1145/2666356.2594340) [A Verified, Efficient Embedding of a Verifiable Assembly Language](https://dl.acm.org/doi/10.1145/3290376) [Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development](https://link.springer.com/chapter/10.1007/978-3-642-14203-1_34) [Finding Code That Explodes under Symbolic Evaluation](https://dl.acm.org/doi/abs/10.1145/3276519) [Growing Solver-Aided Languages with ROSETTE](https://dl.acm.org/doi/abs/10.1145/2509578.2509586) [Hyperkernel: Push-Button Verification of an OS Kernel](https://dl.acm.org/doi/abs/10.1145/3132747.3132748) [Ironclad Apps: End-to-End Security via Automated Full-System Verification](https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel) [Push-Button Verification of File Systems via Crash Refinement](https://www.usenix.org/conference/osdi16/technical-sessions/presentation/sigurbjarnarson) [Refinement reflection: complete verification with SMT](https://dl.acm.org/doi/abs/10.1145/3158141) [Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System](https://dl.acm.org/doi/abs/10.1145/1806596.1806610) [SpaceSearch: A Library for Building and Verifying Solver-Aided Tools](https://dl.acm.org/doi/abs/10.1145/3110269) [Satisfiability modulo theories: introduction and applications](https://dl.acm.org/doi/abs/10.1145/1995376.1995394) [Symbolic Execution for Software Testing Three Decades Later](https://dl.acm.org/doi/10.1145/2408776.2408795) ## Videos Solver-Aided Programming for All ## Books [Coq'Art](https://www.labri.fr/perso/casteran/CoqArt/) [types and programming languages](https://www.amazon.com/Types-Programming-Languages-MIT-Press/dp/0262162091) [practical foundations for programming languages](https://www.cs.cmu.edu/~rwh/pfpl/) ## Tools [Rosette](https://docs.racket-lang.org/rosette-guide/index.html) [CDCL](https://cse442-17f.github.io/Conflict-Driven-Clause-Learning/) ## Tutorials [serval-tutorial-sosp19](https://github.com/uw-unsat/serval-tutorial-sosp19)

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：