Tabla de Contenidos: “…Invited Keynotes -- From model checking to a temporal proof -- Model checking if your life depends on it: a view from intel’s trenches -- Model checking if your life depends on it: a view from intel’s trenches -- Technical Papers and Tool Reports -- Model-checking in finite state-space systems with fine-grained abstractions using SPIN -- Implementing LTL model checking with net unfoldings -- Directed explicit model checking with HSF-SPIN -- Directed explicit model checking with HSF-SPIN -- Addressing dynamic issues of program model checking -- Addressing dynamic issues of program model checking -- Automatically validating temporal safety properties of interfaces -- Automatically validating temporal safety properties of interfaces -- Verification experiments on the MASCARA protocol -- Verification experiments on the MASCARA protocol -- Using SPIN for feature interaction analysis - a case study -- Using SPIN for feature interaction analysis - a case study -- Behavioural analysis of the enterprise javaBeansTM component architecture -- Behavioural analysis of the enterprise javaBeansTM component architecture -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- p2b: A translation utility for linking promela and symbolic model checking (tool paper) -- Transformations for model checking distributed java programs -- Transformations for model checking distributed java programs -- Distributed LTL model-checking in SPIN -- Distributed LTL model-checking in SPIN -- Parallel state space construction for model-checking -- Parallel state space construction for model-checking -- Model checking systems of replicated processes with spin -- Model checking systems of replicated processes with spin -- A SPIN-based model checker for telecommunication protocols -- A SPIN-based model checker for telecommunication protocols -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Modeling and verifying a price model for congestion control in computer networks using promela/spin -- Invited Project Summaries -- A model checking project at philips research -- Applications of model checking at honeywell laboratories -- Coarse-granular model checking in practice…”

Versión digital - Biblioteca Digital Hispánica