Computer Aided Verification

Tutorials and Invited Papers.- Alternative Approaches to Hardware Verification.- The Compositional Specification of Timed Systems — A Tutorial.- Timed Automata.- Ståalmarck’s Method with Extensions to Quantified Boolean Formulas.- Verification of Parameterized Systems by Dynamic Induction.- Formal Methods for Conformance Testing: Theory Can Be Practical.- Processor Verification.- Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach.- Verifying Safety Properties of a PowerPC? Microprocessor Using Symbolic Model Checking without BDDs.- Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists.- Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study.- Protocol Verification and Testing.- Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol.- Test Generation Derived from Model-Checking.- Latency Insensitive Protocols.- Infinite State Space.- Handling Global Conditions in Parametrized System Verification.- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis.- Experience with Predicate Abstraction.- Theory of Verification.- Model Checking of Safety Properties.- A Complete Finite Prefix for Process Algebra.- The Mathematical Foundation of Symbolic Trajectory Evaluation.- Assume-Guarantee Refinement between Different Time Scales.- Linear Temporal Logic.- Efficient Decision Procedures for Model Checking of Linear Time Logic Properties.- Stutter-Invariant Languages, ?-Automata, and Temporal Logic.- Improved Automata Generation for Linear Temporal Logic.- Modeling of Systems.- On the Representation of Probabilities over Structured Domains.- Model Checking Partial State Spaces with 3-Valued Temporal Logics.- Elementary Microarchitecture Algebra.- Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems.- Symbolic Model-Checking.- Stepwise CTL Model Checking of State/Event Systems.- Optimizing Symbolic Model Checking for Constraint-Rich Models.- Efficient Timed Reachability Analysis Using Clock Difference Diagrams.- Theorem Proving.- Mechanizing Proofs of Computation Equivalence.- Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation.- Automatic Verification of Combinational and Pipelined FFT Circuits.- Automata-Theoretic Methods.- Efficient Analysis of Cyclic Definitions.- A Theory of Restrictions for Logics and Automata.- Model Checking Based on Sequential ATPG.- Automatic Verification of Abstract State Machines.- Abstraction.- Abstract and Model Check while You Prove.- Deciding Equality Formulas by Small Domains Instantiations.- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions.- Tool Presentations.- A Toolbox for the Analysis of Discrete Event Dynamic Systems.- TIPPtool: Compositional Specification and Analysis of Markovian Performance Models.- Java Bytecode Verification by Model Checking.- NuSMV: A New Symbolic Model Verifier.- PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols.