Beschreibung
InhaltsangabeInvited Contribution.- On the Construction of Automata from Linear Arithmetic Constraints.- Software and Formal Methods Tools.- An Extensible Type System for Component-Based Design.- Proof General: A Generic Tool for Proof Development.- ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation.- Formal Methods Tools.- Consistent Integration of Formal Methods.- An Architecture for Interactive Program Provers.- The PROSPER Toolkit.- CASL: From Semantics to Tools.- Timed and Hybrid Systems.- On the Construction of Live Timed Systems.- On Memory-Block Traversal Problems in Model-Checking Timed Systems.- Symbolic Model Checking for Rectangular Hybrid Systems.- Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems.- Infinite and Parameterized Systems.- Verification of Parameterized Systems Using Logic Program Transformations.- Abstracting WS1S Systems to Verify Parameterized Networks.- FMona: A Tool for Expressing Validation Techniques over Infinite State Systems.- Transitive Closures of Regular Relations for Verifying Infinite-State Systems.- Diagnostic and Test Generation.- Using Static Analysis to Improve Automatic Test Generation.- Efficient Diagnostic Generation for Boolean Equation Systems.- Efficient Model-Checking.- Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems.- Checking for CFFD-Preorder with Tester Processes.- Fair Bisimulation.- Integrating Low Level Symmetries into Reachability Analysis.- Model-Checking Tools.- Model Checking Support for the ASM High-Level Language.- A Markov Chain Model Checker.- Model Checking SDL with Spin.- Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking.- Symbolic Model-Checking.- Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation.- Symbolic Reachability Analysis Based on SAT-Solvers.- Symbolic Representation of Upward-Closed Sets.- BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems.- Visual Tools.- Tool-Based Specification of Visual Languages and Graphic Editors.- VIP: A Visual Editor and Compiler for v-Promela.- Verification of Critical Systems.- A Comparison of Two Verification Methods for Speculative Instruction Execution.- Partial Order Reductions for Security Protocol Verification.- Model Checking Security Protocols Using a Logic of Belief.- A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors.
