Satisfiability Modulo Theories for Model Checking.- SMT-Based Software Model Checking.- Symbolic Object Code Analysis.- Model Checking in Context.- Experimental Comparison of Concolic and Random Testing for Java Card Applets.- Combining SPIN with ns-2 for Protocol Optimization.- Automatic Generation of Model Checking Scripts Based on Environment Modeling.- Implementation and Performance of Model Checking.- Model Checking: Cleared for Take Off.- Context-Enhanced Directed Model Checking.- Efficient Explicit-State Model Checking on General Purpose Graphics Processors.- The SpinJa Model Checker.- LTL and Büchi Automata.- On the Virtue of Patience: Minimizing Büchi Automata.- Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance.- Nevertrace Claims for Model Checking.- Infinite State Models.- A False History of True Concurrency: From Petri to Tools.- Analysing Mu-Calculus Properties of Pushdown Systems.- Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains.- An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models.- Concurrent Software.- Context-Bounded Translations for Concurrent Software: An Empirical Evaluation.- One Stack to Run Them All.