Talks on program verification

Selected Topics in Design & Verification
Vardi's fun lectures on automated verification and synthesis
Fast Interpolating Bounded Model Checking

Building a VS2013 C# project in a VS2015+ environment

Q: Warning about missing Nuget packages on compiling
A: Remove the error emitting lines in the csproj files as indicated here.

Q: ArgumentException: XXX.dll doesn't contain any UserControl types on execution
A: Mark the project containing the main program as the StartUp project.

A collection of theses on PMC

Regular model checking, Marcus Nilsson

Small Model Theorems for Verification of Parameterized Systems, Tomas Sävström

Small Model Theorem for Parameterized Systems, Frédéric Haziza

Cut-offs and Automata in Formal Verification of Infinite-State Systems, Tomáš Vojnar

Applications of Automata Learning in Verification and Synthesis, Daniel Neider

CTL vs LTL

• Syntax. A quantifier in a CTL formula are in form of a path quantifier $A,E$ following by a state quantifier $F,X,G,U,W$. A quantifier in an LTL is a combination of state quantifiers.
• States and paths. A CTL formula $\phi$ is a state formula, meaning that the temporal operators are state-based in structure: the derivation of a given formula is per-state and depends on the derivation of subformulas for subsequent states. For example, computing the set of states satisfying $AG\ φ$ relies on computing the set of states satisfying $φ$.
  In contrast, LTL formula $\psi$ is a path formula: the derivation of a given formula depends on the derivation of subformulas for suffixes of a path.
• Entailments. We write $M,s \models \phi$ and $M,p \models \psi$ for state $s$ and path $p$. Given a set $I$ of the initial states of $M$, we shall write $M ⊨ φ$ if $M, s ⊨ φ$ for all $s ∈ I$, and write $M ⊨ ψ$ if $M, s ⊨ ψ$ for all paths starting from $I$.
• LTL and CTL are incomparable. The reset property $AG (EF\ φ)$ (i.e. there is always a possibility that $\phi$ could hold, though it may never hold) cannot be expressed in LTL. The stability property $FG\ φ$ cannot be expressed in CTL.
• Structure vs traces. CTL can characterize the structure while LTL only characterizes the traces. Consider the following two systems:
  $A:$ $(s_1,s_2),\ (s_1,s_3),\ (s_2,s_4),\ (s_3,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  $B:$ $(s_1,s_2),\ (s_2,s_4),\ (s_2,s_5),\ (s_4,s_1),\ (s_5,s_1)$
  where $L(s_1)=a,\ L(s_2)=L(s_3)=b,\ L(s_4)=c,\ L(s_5)=d$. Both systems have traces $(ab(c+d))^\omega$ and thus cannot be distinguished in LTL. On the other hand, $B$ is a model of $AG(b\Rightarrow EX\ c)$ while $A$ isn't.
• There is a lot of discussion of the best logic to express properties for software verification. LTL can express important properties for software system modelling (e.g. fairness) when the CTL must have a new semantics to express them. But CTL algorithms are usually more efficient and can use BDD-based algorithms.

References

1. Making prophecies with decision predicates
2. Branching vs. Linear Time: Final Showdown

Selected Topics in Design & Verification

Model Checking and Synthesis with SMT

1. Verifying system against LTL spec → checking emptiness for NBW → finding bad lassos in run graph → checking existence of ranking functions → SMT model checking
2. Synthesizing system from LTL spec → using UF to represent transition relation and iterating through the possible numbers of states ($\le ~|B|^{|B|}$) → SMT model checking
3. In 1989, Pnueli and Rosner solved the LTL synthesis problem (2EXPTIME-complete): LTL $\phi$ → NBW (~ $2^{|\phi|}$) → DPW (~ $2^{|\phi|^{|\phi|}}$) → solve the game (~ $2^{|\phi|^{|\phi|}}$)

(DPW: deterministic parity word automata; NBW: nondeterministic Buchi word automata)

Downgrade from PHP 7 to PHP 5.6 on Ubuntu

http://askubuntu.com/questions/109404/how-do-i-install-different-upgrade-or-downgrade-php-version-in-still-supported

http://askubuntu.com/questions/761713/how-can-i-downgrade-from-php-7-to-php-5-6-on-ubuntu-16-04

Remove files from git history

http://stevelorek.com/how-to-shrink-a-git-repository.html