ThisvolumecontainstheproceedingsoftheconferenceonComputer AidedVe- ?cation, CAV 2004, held in Boston, Massachusetts, USA, July13-17,2004.CAV 2004 was the 16th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical - sults to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. The conference has traditionally drawn participation from researchersas well as practitioners in both academia and industry. CAV 2004 was colocated with the ACM International Symposium on So- ware Testing and Analysis (ISSTA 2004), and was partially sponsored by the ACMSIGSOFT.Thecolocationre?ectstheincreasingsynergybetweenresearch on veri?cation and testing, and emerging applications of formal veri?cation to softwareanalysis.Joint CAV-ISSTA events included a distinguished plenary l- ture by David Harel and a special session exploring various approaches to the speci?cation and veri?cation of concurrent software organized by Shaz Qade

This volume contains the proceedings of the 7th Workshop on Hybrid Systems: Computation and Control (HSCC 2004) held in Philadelphia, USA, from March 25 to 27, 2004. The annual workshop on hybrid systems attracts researchers from academia and industry interested in modeling, analysis, and implemen- tion of dynamic and reactive systems involving both discrete and continuous behaviors. The previous workshops in the HSCC series were held in Berkeley, USA(1998), Nijmegen, TheNetherlands(1999), Pittsburgh, USA(2000), Rome, Italy (2001), Palo Alto, USA (2002), and Prague, Czech Republic (2003). This year s HSCC was organized in cooperation with ACM SIGBED (Special Interest Group on Embedded Systems) and was technically co-sponsored by the IEEE Control Systems Society. The program consisted of 4 invited talks and 43 regular papers selected from 117 regular submissions. The program covered topics such as tools for analysis and veri?cation, control and optimization, modeling, and engineering applica- ons, as in past years, and emerging directions in programming language support and implementation. The program also contained one special session focusing on the interplay between biomolecular networks, systems biology, formal methods, andthecontrolofhybridsystem

This book constitutes the refereed proceedings of the 8th International Conference on Computer Aided Verification, CAV '96, held in New Brunswick, NJ, USA, in July/August 1996 as part of the FLoC '96 federated conference.
The volume presents 32 revised full research contributions selected from a total of 93 submissions; also included are 20 carefully selected descriptions of tools and case studies. The set of papers reports the state-of-the-art of the theory and practice of computer assisted formal analysis methods for software and hardware systems; a certain emphasis is placed on verification tools and the algorithms and techniques that are needed for their implementation.

This reference book documents the scientific outcome of the DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems, held at Rutgers University in New Brunswick, NJ, in October 1995.
A hybrid system consists of digital devices that interact with analog environments. Computer science contributes expertise on the analog aspects of this emerging field of interdisciplinary research and design. The 48 revised full papers included were strictly refereed; they present the state of the art in this dynamic field with contributions by leading experts. Also available are the predecessor volumes published in the same series as LNCS 999 and LNCS 736.