Model checking safety properties

Regular model checking

Regular Model Checking Made Simple and Efficient

Regular Model Checking Without Transducers

Model Checking of Safety Properties

Finite presentations of infinite structures: Paper / Slide

DOA Tools and Mods

Documents

• Overview - http://bbs.3dmgame.com/thread-4791938-1-1.html
• Editing texture - https://www.ptt.cc/bbs/AC_In/M.1429727192.A.74B.html
• Using AutoLink - http://w11.zetaboards.com/SFxT_Mods/topic/11582418/1/

DLC Tools

• AutoLink Homepage
• Collection of DLC tools
• TMC to DLC convertor
• Texture editor

Mods

http://saafrats.deviantart.com/gallery/
http://www.loverslab.com/files/download/2627-doa5lr-h-lod-nude-mod-curvy-body/
http://www.loverslab.com/topic/56672-doa5lr-saafrats-h-lod-nude-mod-v10-curvy-body-mod/

Offline MySQL migration

http://serverfault.com/questions/659048/can-i-copy-the-entire-var-lib-mysql-folder-to-a-different-server-mysql-vs-mar

C# performance notes

• for v.s foreach
  1. for loops on List are a bit more than 2 times cheaper than foreach loops on List.
  2. Looping on Array is around 2 times cheaper than looping on List.
  3. As a consequence, looping on Array using for is 5 times cheaper than looping on List using foreach.
  4. LinkedList only allows foreach loops, as it would take quadratic time to loop a LinkedList through indices.
  5. Looping overheads: for < foreach; Array ~ List < ArrayList < LinkedList
• Everything stored in an ArrayList is an object. So be careful of the boxing/unboxing overhead.
• String concatenation overheads are negligible outside loops. 

Fill and sign PDF forms online

http://www.pdfescape.com/

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

Loop invariant resources

Synthesis

Inferring loop invariants using post-conditions:
http://se.ethz.ch/~meyer/publications/proofs/invariant_inference.pdf

Generating loop invariants using predicate abstraction
https://hal.inria.fr/inria-00615623/document

Boogie uses abstract interpretation to infer loop invariants:
http://research.microsoft.com/en-us/um/people/leino/papers/krml160.pdf

Tools

Boogie overview slide
http://webcourse.cs.technion.ac.il/236800/Winter2010-2011/ho/WCFiles/Boogie.pdf

Log usernames and passwords for SSH attacks

https://github.com/wedaa/LongTail-Log-Analysis/blob/master/install_openssh.sh

NF, HNF and WHNF

WHNF: a lambda expr or a constructor
HNF: a lambda expr where the function body is a NF
NF: a term that contains no beta regex

A discussion in SO about stack overflow is particularly interesting to me. I thought the strict version of foldl evaluates to NF, but it in fact only evaluates to WHNF. This is why summing up tuples doesn't evaluate the components, another thing I misunderstood.