Symbolic executions

Symbolic Execution Tutorial

Symbolic Execution for Software Testing: Three Decades Later

Graph logics

The paper Simulate transitive closure using FO logic uses first-order theorem provers to prove transitive closures of certain binary predicates.

Courcelle's theorem

React.js tips

http://blog.revathskumar.com/2015/08/reactjs-things-i-learned-after-building-first-app.html

Converts videos to WebM with aconv/ffmpeg

Using aconv:
http://daniemon.com/blog/how-to-convert-videos-to-webm-with-ffmpeg/

Using ffmpeg:
http://trac.ffmpeg.org/wiki/Encode/VP8

Example code:

ffmpeg -i $INPUT -c:v libvpx -crf 4 -b:v 10M -c:a libvorbis $OUTPUT

The above command converts the input file to webm with a variable bitrate in a constant quality mode, which ensures that every frame achieve a certain quality level. In this command, -b:v 10M sets the maximum allowed bitrate to 10 MBit/s and -crf 4 sets the constant quality to 4 (best quality).

Dafny resources

Online verifier and tutorial
Using Dafny in Visual Studio

Overviews

1. Getting Started with Dafny (with language reference); a shorter html version.
2. Using Dafny, an Automatic Program Verifier (slide)
3. Dafny: An Automatic Program Verifier for Functional Correctness

4. Dafny: Statically Verifying Functional Correctness.
5. Type system of Dafny / Proving theorems with Dafny.

Lecture notes

Verified programming in Dafny

Forums & blogs

Dafny questions on StackOverflow / The official Dafny forum / Lexical scope

Advanced topics

Non-determinism
Data refinement
Calculational proof
Triggers

Git notes

Basics

Add new changes to the last commit:

git commit FILES --amend (-m "new messages")

See staged changes

git diff --staged

Modify commit and update date

git commit --amend --date="Mon Mar 7 22:40:51 2016 +0800"
GIT_COMMITTER_DATE="Mon Mar 7 22:40:51 2016 +0800" git commit --amend

Delete remote branch at repo origin

git push origin :BRANCH_NAME

reflog helps you recover a deleted branch or a commit deleted by hard-reset:

git log --walk-reflogs                  # get SHA of the deleted commit

To recover a commit, use

git reset --hard COMMIT_SHA             # recover the deleted commit

To recover a branch, use

git branch BRANCH_NAME BRANCH_HEAD_SHA  # recover the branch

Work with branch

1. First checkout to a feature branch and work there.
2. Go back to the master branch and make commits.
3. Rebase master in the feature branch.

Create a new branch starting from a commit:

git branch BRANCH_NAME COMMIT_SHA

Some Git log formats:

git log --oneline
git log --oneline --stat
git log --oneline --graph
git log --oneline --patch

Use recursive merge instead of fast-forward merge to keep commits in the feature branch after merging:

git checkout master
git merge --no-ff BRANCH_NAME

Fix line feeds

1. Suppose you have a project of which the contributors work on both Linux/OSX and Windows. On Linux/Cygwin/OSX, you should set

git config --global core.autocrlf input

to fix Windows LFs that get introduced. On Windows, you should set

git config --global core.autocrlf true

to change LF to CR/LF on checkout and convert back to LF on commit. So the line feeds in the project are always LF. When running the Git installer for Windows, you should choose "Checkout Windows-style, commit Unix-style line endings", which automatically sets core.autocrlf to true.

2. Sometimes, your project contains files for both Linux and Windows (e.g., a .NET project with Cygwin bash scripts). In such case, the line-feed conflicts cannot be resolved by simply setting autocrlf. One solution to this problem is to set

git config --global core.whitespace cr-at-eol

This basically tells Git that an end-of-line CR is not an error. As a result, those annoying ^M characters in Windows files no longer appear at the end of lines in git diff, git show, etc. Note that extra spaces at the end of a line still show as errors (highlighted in red) in the diff.

Submodules

1. Clone a repo as a submodule of the current repo

git submodule add REPO_URL DIRNAME
cd DIRNAME
git checkout master

2. Note that if we commit changes in a submodule, we also have to commit its parent repo to point to head of the new submodule. Hence, whenever you update a submodule, you need to commit and push twice---one for the submodule and one for its parent repo. To avoid chores, you can do the following in the parent repo:
a) Use git push --recurse-submodules=check. This option can check whether you have un-pushed submodules. Or
b) Use git push --recurse-submodules=on-demand. This way submodules that need it will be pushed automatically.

3. To clone a repo that contains submodules, we have to initialize the submodules after clone the repo:

git submodule init

Update the submodules to get the files inside:

git submodule update

Note that each time after you update a submodule, you will be put in a "headless" state, i.e., in a non-existing branch. We have to checkout to a branch (such as master) and do our work there.

IDE shortcuts

Visual Studio:
http://visualstudioshortcuts.com/2015/

IntelliJ Idea:
https://www.jetbrains.com/idea/docs/IntelliJIDEA_ReferenceCard.pdf