Automated Technology for Verification and Analysis

- Invited Talks

- Verifying VLSI Circuits

- 3-Valued Abstraction for (Bounded) Model Checking

- Local Search in Model Checking

- State Space Reduction

- Exploring the Scope for Partial Order Reduction

- State Space Reduction of Linear Processes Using Control Flow Reconstruction

- A Data Symmetry Reduction Technique for Temporal-epistemic Logic

- Tools

- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets

- CLAN: A Tool for Contract Analysis and Conflict Discovery

- UnitCheck: Unit Testing and Model Checking Combined

- Probabilistic Systems

- LTL Model Checking of Time-Inhomogeneous Markov Chains

- Statistical Model Checking Using Perfect Simulation

- Quantitative Analysis under Fairness Constraints

- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems

- Medley

- Memory Usage Verification Using Hip/Sleek

- Solving Parity Games in Practice

- Automated Analysis of Data-Dependent Programs with Dynamic Memory

- Temporal Logic I

- On-the-fly Emptiness Check of Transition-Based Streett Automata

- On Minimal Odd Rankings for Büchi Complementation

- Specification Languages for Stutter-Invariant Regular Properties

- Abstraction and Refinement

- Incremental False Path Elimination for Static Software Analysis

- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement

- Don't Know for Multi-valued Systems

- Logahedra: A New Weakly Relational Domain

- Fault Tolerant Systems

- Synthesis of Fault-Tolerant Distributed Systems

- Formal Verification for High-Assurance Behavioral Synthesis

- Dynamic Observers for the Synthesis of Opaque Systems

- Temporal Logic II

- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

- LTL Model Checking for Recursive Programs

- On Detecting Regular Predicates in Distributed Systems