Model Checking Software

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 javaBeans(TM) component architecture.- Behavioural analysis of the enterprise javaBeans(TM) 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.- ASPIN-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.