Model Checking Software

Invited Contributions.- Residual Checking of Safety Properties.- The Case for Context-Bounded Verification of Concurrent Programs.- Combining Static and Dynamic Reasoning for the Discovery of Program Properties.- Using Dynamic Symbolic Execution to Improve Deductive Verification.- Regular Papers.- Automated Evaluation of Secure Route Discovery in MANET Protocols.- Model Checking Abstract Components within Concrete Software Environments.- Generating Compact MTBDD-Representations from Probmela Specifications.- Dynamic Delayed Duplicate Detection for External Memory Model Checking.- State Focusing: Lazy Abstraction for the Mu-Calculus.- Efficient Modeling of Concurrent Systems in BMC.- Tackling Large Verification Problems with the Swarm Tool.- Formal Verification of a Flash Memory Device Driver – An Experience Report.- Layered Duplicate Detection in External-Memory Model Checking.- Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes.- Improved On-the-Fly Equivalence Checking Using Boolean Equation Systems.- Resource-Aware Verification Using Randomized Exploration of Large State Spaces.- Incremental Hashing for Spin.- Verifying Compiler Based Refinement of Bluespec TM Specifications Using the SPIN Model Checker.- Symbolic Context-Bounded Analysis of Multithreaded Java Programs.- Efficient Stateful Dynamic Partial Order Reduction.- Symbolic String Verification: An Automata-Based Approach.- Verifying Multi-threaded C Programs with SPIN.