The best way to contact me is via email .
You can also find me on DBLP, GitHub, LinkedIn, StackOverflow, and Twitter.
In 2016 I founded Pygmal Technologies. Our flagship product is the SPACE operating environment in virtual reality.
Dramatically Reducing Software Vulnerabilities (pdf)
Mike Gordon's Hoare Logic lecture notes
I am an advocate of System Prevalence and I think this page explains the idea very well.
C Preprocessor tricks, tips, and idioms
The Lost Art of C Structure Packing
Lisp as an Alternative to Java, Common Lisp Implementations: A Survey
Quantitative Economics in Julia
Systems Benchmarking Crimes, Pythagorean means
Scaling in the Linux Networking Stack
A talk on scientific research in China (in Chinese)
What's New in CPUs Since the 80s and How Does It Affect Programmers?
Diving Deep with Dependency Injection (explains how AngularJS $injector works)
Data-binding Revolutions with Object.observe() (explains how AngularJS works)
Root cause analysis (RCA) is a method of problem solving that tries to identify the root causes of faults or problems.
Gerrit is a good choice for code review; Meld is a good choice for visual diff.
Queueing in the Linux Network Stack
Static Linking Considered Harmful
What Does Haskell Have to Do with C++?
Programming Languages Etc. Reading Group
The Case for Formal Verification (2013)
Modern Microprocessors - A 90 Minute Guide!
Comprehensive formal verification of an OS microkernel
Operating system verification - an overview
Let's Encrypt is a new Certificate Authority: It's free, automated, and open.
The Mezzo programming language
The SO_REUSEPORT socket option
CommonMark (previously Standard Markdown)
Use of Formal Methods at Amazon Web Services
Tags and boost::parameter
Backporting bug fixes: Towards LTS Haskell
Monitor keystrokes in Vim and educate me with better alternative keystrokes
Principles of Eventual Consistency (Volume 1, Issue 1-2)
Formal Models and Techniques for Analyzing Security Protocols: A Tutorial (Volume 1, Issue 3)
A Framework For Efficient Modular Heap Analysis (Volume 1, Issue 4)
Pointer Analysis (Volume 2, Issue 1)
Static Analysis and Verification of Aerospace Software by Abstract Interpretation (Volume 2, Issue 2-3)
UseDNS no # Add to /etc/ssh/sshd_config options single-request-reopen # Add to /etc/resolv.conf
pdftk draft.pdf output uncompressed.pdf uncompress less uncompressed.pdf # check general structure grep -a DRAFT uncompressed.pdf # check specific lines cat uncompressed.pdf | sed 's/DRAFT//g' > without-draft.pdf
pdfjam ch1.pdf --landscape --nup 2x1 --a4paper --outfile ch1-2x1.pdf pdf2ps ch1-2x1.pdf ch1-2x1.ps pdfjam all.pdf --trim '2cm 3cm 2.5cm 1.5cm' --clip true --outfile /dev/stdout |\ pdfjam --frame true --nup '2x2' --a4paper --outfile all-2x2-trim.pdf
sudo apt-get install texlive-full latex-cjk-all \usepackage{CJKutf8} \begin{CJK}{UTF8}{gkai}中文\end{CJK}