This volume contains the proceedings of CHARME 2001, the Eleventh Advanced Research Working Conference on Correct Hardware Design and Veri?cation Methods. CHARME 2001 is the 11th in a series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and hardware-like systems. Previous events in the 'CHARME' series were held in Bad Herrenalb (1999), Montreal (1997), Frankfurt (1995), Arles (1993), and Torino (1991). This series of meetings has been organized in cooperation with IFIP WG 10.5 and WG 10.2. Prior meetings, stretching backto the earliest days of formal hardware veri?cation, were held under various names in Miami (1990), Leuven (1989), Glasgow (1988), Grenoble (1986), Edinburgh (1985), and Darmstadt (1984). The convention is now well-established whereby the European CHARME conference alternates with its biennial counterpart, the International Conference on Formal Methods in Computer-Aided Design (FMCAD), which is held on even-numbered years in the USA. The conference tookplace during 4-7 September 2001 at the Institute for System Level Integration in Livingston, Scotland. It was co-hosted by the - stitute and the Department of Computing Science of Glasgow University and co-sponsored by the IFIP TC10/WG10.5 Working Group on Design and En- neering of Electronic Systems. CHARME 2001 also included a scienti?c session and social program held jointly with the 14th International Conference on Th- rem Proving in Higher Order Logics (TPHOLs), which was co-located in nearby Edinburgh.

This book constitutes the refereed proceedings of the International Workshop on OpenMP Applications and Tools, WOMPAT 2001, held in West Lafayette, IN, USA in July 2001.The 15 full papers presented were carefully reviewed and revised for inclusion in the volume. The book presents a state-of-the-art overview on OpenMP shared memory parallel programming. The papers are organized in topical sections on benchmarking, compiler implementation and optimization, tools and tool technology, OpenMP experience, NUMA machines and clusters, and OpenMP extensions.

This book constitutes the refereed proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, held in Paris, France in July 2001.The 33 revised full papers presented were carefully reviewed and selected from 106 regular paper submissions; also included are 13 reviewed tool presentations selected from 27 submissions. The book offers topical sections on model checking and theorem proving, automata techniques, verification core technology, BDD and decision trees, abstraction and refinement, combinations, infinite state systems, temporal logics and verification, microprocessor verification and cache coherence, SAT and applications, and timed automata.

This book constitutes the refereed proceedings of the Third International Workshop on Grid Computing, GRID 2002, held in Baltimore, MD, USA in November 2002.The 22 revised full papers and 6 work-in-progress papers presented were carefully reviewed and selected from 78 submissions. The papers are organized in topical sections on applications and frameworks, optimization and performance, programming models, resource discovery and management, security and policy management, scheduling, grid infrastructure and services, and data services.

Performance of Web Services provides innovative techniques to improve the performance of Web Services, as well as QoS (Quality of Service) requirements. This includes Qos performance, reliability and security. The author presents two levels of Web Services: the "kernel" (ithe SOAP engine which delivers messages from one point to another through various networks), and the "server side" (which processes heavy load / requests). The primary objective of this book is execution of applications delivered in a timely fashion. Case studies and examples are provided throughout this book.

This book constitutes the thoroughly refereed post-proceedings of the 6th International Workshop on DNA-Based Computers, DNA 2000, held in Leiden, The Netherlands, in June 2000.The 16 revised full papers presented together with two invited papers were carefully reviewed and selected from 33 submissions. All current aspects of DNA computing, ranging from theoretical and foundational issues to algorithms, are addressed, from the computer science point of view as well as from the molecular biology point of view.

User-Centred Requirements Engineering: Theory and Practice reviews requirements engineering research and practice over the past 10 years. In this book, Alistair Sutcliffe introduces the field of Requirements Engineering, and describes a framework for RE research and practice to date. He explains the psychological background behind RE problems - providing some understanding about why RE is difficult and how human understanding can cause the problems we observe in getting requirements right. The book discusses communication and requirements analysis, and gives practical guidance for requirements elicitation, modelling and validation, along with details of a practical RE method for scenario-based requirements analysis and requirements for safety critical systems. Whilst primarily a research text for graduate courses, this book is also intended as a useful reference for practitioners who want an in-depth treatment of the subject to date.

This book constitutes the refereed proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2002, held in Grenoble, France, in April 2002.The 28 revised full papers presented together with an extended abstract of an invited paper were carefully reviewed and selected from a total of 67 submissions. Among the topics addressed are algebraic, categorical, logical, and geometric theories, models and methods which support the specification, synthesis, verification, analysis, and transformation of sequential, concurrent, distributed, and mobile programs and software systems.

This book is the first comprehensive approach to the construction and the management of cooperative information systems. From a set of input database schemes describing the information content of multiple sources, the techniques presented yield a structured, integrated and consistent description of the information content represented in a suitable data repository. The author builds his work on skilled and controlled use of results and methods from various fields of computer science, such as data mining, algorithmic learning, knowledge representation, database management, etc. The approach presented has been implemented in the prototype system DIKE, Database Intensional Knowledge Extractor, which has been studied in various application contexts.

This book provides a detailed account of real-time systems, including program structures for real-time, phases development analysis, and formal specification and verification methods of reactive systems.Real-Time and Multi-Agent Systems brings together the 3 key fields of current and future data-processing:- Distributed systems and applications;- Parallel scientific computing;- Real-time and manufacturing systems.It covers the basic concepts and theories, methods, techniques and tools currently used in the specification and implementation of applications and contains lots of examples as well as complete case studies.

This volume contains the papers presented at the International Workshop on Tools for Working with Guidelines, (TFWWG 2000), held in Biarritz, France, in October 2000. It is the final outcome of the International Special Interest Group on Tools for Working with Guidelines.Human-computer interaction guidelines have been recognized as a uniquely relevant source for improving the usability of user interfaces for interactive systems. The range of interactive techniques exploited by these interactive systems is rapidly expanding to include multimodal user interfaces, virtual reality systems, highly interactive web-based applications, and three-dimensional user interfaces. Therefore, the scope of guidelines' sources is rapidly expanding as well, and so are the tools that should support users who employ guidelines to ensure some form of usability.Tools For Working With Guidelines (TFWWG) covers not only software tools that designers, developers, and human factors experts can use to manage multiple types of guidelines, but also looks at techniques addressing organizational, sociological, and technological issues.

Crypto2000wasthe20thAnnualCryptoconference. Itwassponsoredbythe InternationalAssociationforCryptologicResearch(IACR)incooperationwith theIEEEComputerSocietyTechnicalCommitteeonSecurityandPrivacyand theComputerScienceDepartmentoftheUniversityofCaliforniaatSantaB- bara. Theconferencereceived120submissions,andtheprogramcommittee- lected32oftheseforpresentation. Extendedabstractsofrevisedversionsof thesepapersareintheseproceedings. Theauthorsbearfullresponsibilityfor thecontentsoftheirpapers. Theconferenceprogramincludedtwoinvitedlectures. DonCoppersmith's presentation"ThedevelopmentofDES"recordedhisinvolvementwithoneof themostimportantcryptographicdevelopmentsever,namelytheDataEncr- tionStandard,andwasparticularlyaptgiventheimminentselectionofthe AdvancedEncryptionStandard. Mart'?nAbadi'spresentation"Tamingthe- versary"wasaboutbridgingthegapbetweenusefulbutperhapssimplisticthreat abstractionsandrigorousadversarialmodels,orperhaps,evenmoregenerally, betweenviewpointsofthesecurityandcryptographycommunities. Anabstract correspondingtoMart'?n'stalkisincludedintheseproceedings. Theconferenceprogramalsoincludeditstraditional"rumpsession"ofshort, informalorimpromptupresentations,chairedthistimebyStuartHaber. These presentationsarenotre?ectedintheseproceedings. Anelectronicsubmissionprocesswasavailableandrecommended,butforthe ?rsttimeusedawebinterfaceratherthanemail. (Perhapsasaresult,therewere nohardcopysubmissions. )Thesubmissionreviewprocesshadthreephases. In the?rstphase,programcommitteememberscompiledreports(assistedattheir discretionbysub-refereesoftheirchoice,butwithoutinteractionwithother programcommitteemembers)andenteredthem,viawebforms,intoweb-review softwarerunningatUCSD. Inthesecondphase,committeemembersusedthe softwaretobrowseeachother'sreports,discuss,andupdatetheirownreports. Lastlytherewasaprogramcommitteemeetingtodiscussthedi?cultcases. Iamextremelygratefultotheprogramcommitteemembersfortheiren- mousinvestmentoftime,e?ort,andadrenalineinthedi?cultanddelicate processofreviewandselection. (Alistofprogramcommitteemembersands- refereestheyinvokedcanbefoundonsucceedingpagesofthisvolume. )Ialso thanktheauthorsofsubmittedpapers-inequalmeasureregardlessofwhether theirpaperswereacceptedornot-fortheirsubmissions. Itistheworkofthis bodyofresearchersthatmakesthisconferencepossible. IthankRebeccaWrightforhostingtheprogramcommitteemeetingatthe AT&TbuildinginNewYorkCityandmanagingthelocalarrangements,and RanCanettifororganizingthepost-PC-meetingdinnerwithhischaracteristic gastronomicandoenophilic?air. VI Preface Theweb-reviewsoftwareweusedwaswrittenforEurocrypt2000byWim MoreauandJorisClaessensunderthedirectionofEurocrypt2000programchair BartPreneel,andIthankthemforallowingustodeploytheirusefulandcolorful tool. IammostgratefultoChanathipNamprempre(aka. Meaw)whoprovided systems,logistical,andmoralsupportfortheentireCrypto2000process. She wrotethesoftwarefortheweb-basedsubmissions,adaptedandranthew- reviewsoftwareatUCSD,andcompiledthe?nalabstractsintotheproceedings youseehere. ShetypesfasterthanIspeak. IamgratefultoHugoKrawczykforhisinsightandadvice,providedovera longperiodoftimewithhisusualcombinationofhonestyandcharm,andto himandotherpastprogramcommitteechairs,mostnotablyMichaelWiener andBartPreneel,forrepliestothehostofquestionsIposedduringthep- cess. InadditionIreceivedusefuladvicefrommanymembersofourcommunity includingSilvioMicali,TalRabin,RonRivest,PhilRogaway,andAdiShamir. FinallythankstoMattFranklinwhoasgeneralchairwasinchargeofthelocal organizationand?nances,and,ontheIACRside,toChristianCachin,Kevin McCurley,andPaulVanOorschot. ChairingaCryptoprogramcommitteeisalearningprocess. Ihavecometo appreciateevenmorethanbeforethequalityandvarietyofworkinour?eld, andIhopethepapersinthisvolumecontributefurthertoitsdevelopment. June2000 MihirBellare ProgramChair,Crypto2000 CRYPTO2000 August20-24,2000,SantaBarbara,California,USA Sponsoredbythe InternationalAssociationforCryptologicResearch(IACR) incooperationwith IEEEComputerSocietyTechnicalCommitteeonSecurityandPrivacy, ComputerScienceDepartment,UniversityofCalifornia,SantaBarbara GeneralChair MatthewFranklin,XeroxPaloAltoResearchCenter,USA ProgramChair MihirBellare,UniversityofCalifornia,SanDiego,USA ProgramCommittee AlexBiryukov...WeizmannInstituteofScience,Israel DanBoneh...StanfordUniversity,USA ChristianCachin...IBMResearch,Switzerland RanCanetti...IBMResearch,USA RonaldCramer...ETHZurich,Switzerland YairFrankel...CertCo,USA ShaiHalevi...IBMResearch,USA ArjenLenstra...Citibank,USA MitsuruMatsui...MitsubishiElectricCorporation,Japan PaulVanOorschot...EntrustTechnologies,Canada BartPreneel...KatholiekeUniversiteitLeuven,Belgium PhillipRogaway. ..UniversityofCalifornia,Davis,USA VictorShoup...IBMZurich,Switzerland JessicaStaddon...BellLabsResearch,PaloAlto,USA JacquesStern...EcoleNormaleSup'erieure,France DougStinson...UniversityofWaterloo,Canada SalilVadhan...MassachusettsInstituteofTechnology,USA DavidWagner...UniversityofCalifornia,Berkeley,USA RebeccaWright...AT&TLaboratoriesResearch,USA Advisorymembers MichaelWiener(Crypto1999programchair). . EntrustTechnologies,Canada JoeKilian(Crypto2001programchair)...Intermemory,USA VIII Organization Sub-Referees BillAiello,JeeheaAn,OlivierBaudron,DonBeaver,JoshBenaloh,JohnBlack, SimonBlackburn,AlexandraBoldyreva,NikitaBorisov,VictorBoyko,Jan- menisch,SureshChari,ScottContini,DonCoppersmith,ClaudeCr'epeau,Ivan Damg?ard,AnandDesai,GiovanniDiCrescenzo,YevgeniyDodis,Matthias Fitzi,MattFranklin,RosarioGennaro,GuangGong,LuisGranboulan,Nick Howgrave-Graham,RussellImpagliazzo,YuvalIshai,MarkusJakobsson,Stas Jarecki,ThomasJohansson,CharanjitJutla,JoeKilian,EyalKushilevitz,Moses Liskov,StefanLucks,AnnaLysyanskaya,PhilipMacKenzie,SubhamoyMaitra, TalMalkin,BarbaraMasucci,AlfredMenezes,DanieleMicciancio,SaraMiner, IliaMironov,MoniNaor,PhongNguyen,RafailOstrovsky,ErezPetrank,Birgit P?tzmann,BennyPinkas,DavidPointcheval,GuillaumePoupard,TalRabin, CharlieRacko? ,Zul?karRamzan,OmerReingold,LeoReyzin,PankajRohatgi, AmitSahai,LouisSalvail,ClausSchnorr,MikeSemanko,BobSilverman,Joe Silverman,DanSimon,NigelSmart,BenSmeets,AdamSmith,MartinStrauss, GaneshSundaram,SergeVaudenay,FrederikVercauteren,BernhardvonSt- gel,RuizhongWei,SusanneGudrunWetzel,ColinWilliams,StefanWolf,Felix Wu,YiqunLisaYin,AmirYoussef,RobertZuccherato TableofContents XTRandNTRU TheXTRPublicKeySystem...1 ArjenK. Lenstra,EricR. Verheul AChosen-CiphertextAttackagainstNTRU...20 ' ElianeJaulmes,AntoineJoux PrivacyforDatabases PrivacyPreservingDataMining ...36 YehudaLindell,BennyPinkas ReducingtheServersComputationinPrivateInformationRetrieval: PIRwithPreprocessing...55 AmosBeimel,YuvalIshai,TalMalkin SecureDistributedComputationandApplications ParallelReducibilityforInformation-TheoreticallySecureComputation...74 YevgeniyDodis,SilvioMicali OptimisticFairSecureComputation...93 ChristianCachin,JanCamenisch ACryptographicSolutiontoaGameTheoreticProblem...112 YevgeniyDodis,ShaiHalevi,TalRabin AlgebraicCryptosystems Di?erentialFaultAttacksonEllipticCurveCryptosystems...131 IngridBiehl,BerndMeyer,VolkerMul ..ler QuantumPublic-KeyCryptosystems ...1 47 TatsuakiOkamoto,KeisukeTanaka,ShigenoriUchiyama NewPublic-KeyCryptosystemUsingBraidGroups ...166 KiHyoungKo,SangJinLee,JungHeeCheon,JaeWooHan, Ju-sungKang,ChoonsikPark MessageAuthentication KeyRecoveryandForgeryAttacksontheMacDESMACAlgorithm ...184 DonCoppersmith,LarsR. Knudsen,ChrisJ. Mitchell X TableofContents CBCMACsforArbitrary-LengthMessages:TheThree-KeyConstructions 197 JohnBlack,PhillipRogaway L-collisionAttacksagainstRandomizedMACs...216 MichaelSemanko DigitalSignatures OntheExactSecurityofFullDomainHash...229 Jean-S' ebastienCoron TimedCommitments...236 DanBoneh,MoniNaor APracticalandProvably SecureCoalition-ResistantGroupSignatureScheme...255 GiuseppeAteniese,JanCamenisch,MarcJoye,GeneTsudik ProvablySecurePartiallyBlindSignatures...271 MasayukiAbe,TatsuakiOkamoto Cryptanalysis n WeaknessesintheSL (IF )HashingScheme...287 2 2 RainerSteinwandt,MarkusGrassl,WilliGeiselmann,ThomasBeth FastCorrelationAttacksthroughReconstructionofLinearPolynomials . . 300 ThomasJohansson,FredrikJ.. onsson TraitorTracingandBroadcastEncryption SequentialTraitorTracing...

"Systems: Concepts, Methodologies and Applications, Second Edition" is brought forward by Brian Wilson Department of Systems and Information Management, Lancaster University, UK. The result of many years' experience, this book, now extensively revised and updated, emphasizes the application of systems concepts and methodologies that have been developed at Lancaster University. In particular the book is about problem solving and the relationship between theory and practice. Complementary to "Systems Thinking, Systems Practice" by Peter Checkland (Wiley, 1981), which has become a classic in the field, this book shows how systems ideas can be used to cope with real-life problems. Reviews of the first edition: "an excellent book which provides a synthesis of the action-research undertaken by the well-known Department of Systems, University of Lancaster. Wilson's lucid style of writing and the historical perspective of the Lancaster learning experience provide a strong contextural case for the concept of a human activity system to investigate 'badly-defined' [Checkland's 'soft'] systems". (Chris Beaumont, "Journal of the Operational Research Society", January 1985). "This volume, expertly compiled by Brian Wilson, is the latest and probably the clearest statement in book form of the philosophy of that department [Department of Systems, University of Lancaster]. This is a volume which deserves to be read. (E.R. Carson, Kybernetes, 12, 1985). ""Systems: Concepts, Methodologies and Applications" is Wilson's account of his professional life at Lancaster since then (1966). His careful reflection on the work of so many years deserves attention). (Trevor Williams, Futures, December 1985).

Neural Networks are a new, interdisciplinary tool for information processing. Neurocomputing being successfully introduced to structural problems which are difficult or even impossible to be analysed by standard computers (hard computing). The book is devoted to foundations and applications of NNs in the structural mechanics and design of structures.

This book constitutes the refereed proceedings of the 9th Annual European Symposium on Algorithms, ESA 2001, held in Aarhus, Denmark, in August 2001.
The 41 revised full papers presented together with three invited contributions were carefully reviewed and selected from 102 submissions. The papers are organized in topical sections on caching and prefetching, online algorithms, data structures, optimization and approximation, sequences, scheduling, shortest paths, geometry, distributed algorithms, graph algorithms, pricing, broadcasting and multicasting, graph labeling and graph drawing, and graphs.

This book constitutes the thoroughly refereed post-proceedings of the 4th International Workshop on Algorithm Engineering, WAE 2000, held in Saarbrücken, Germany in September 2000. The 19 revised full papers presented together with one invited paper were carefully reviewed and selected from a total of 30 submissions. Among the topics addressed are software repositories allowing for the use and experimentation with efficient discrete algorithms; novel uses of discrete algorithms; methodological issues on algorithms and data structures; and methodological issues on converting user requirements into efficient algorithmic and implementation solutions.

Middleware is everywhere. Ever since the advent of sockets and other virtu- circuit abstractions, researchers have been looking for ways to incorporate high- value concepts into distributed systems platforms. Most distributed applications, especially Internet applications, are now programmed using such middleware platforms. Prior to 1998, there were several major conferences and workshops at which research into middleware was reported, including ICODP (International C- ference on Open Distributed Processing), ICDP (International Conference on Distributed Platforms) and SDNE (Services in Distributed and Networked - vironments). Middleware'98was a synthesis of these three conferences. Middleware 2000 continued the excellent tradition of Middleware'98. It p- vided a single venue for reporting state-of-the-art results in the provision of distributed systems platforms. The focus of Middleware 2000 was the design, implementation, deployment, and evaluation of distributed systems platforms and architectures for future networked environments. Among the 70 initial submissions to Middleware 2000, 21 papers were - lected for inclusion in the technical program of the conference. Every paper was reviewed by four members of the program committee. The papers were judged - cording to their originality, presentation quality, and relevance to the conference topics. The accepted papers cover various subjects such as caching, re?ection, quality of service, and transactions.

Computers are gaining more and more control over systems that we use or rely on in our daily lives, privately as well as professionally. In safety-critical applications, as well as in others, it is of paramount importance that systems controled by a computer or computing systems themselves reliably behave in accordance with the specification and requirements, in other words: here correctness of the system, of its software and hardware is crucial. In order to cope with this callenge, software engineers and computer scientists need to understand the foundations of programming, how different formal theories are linked together, how compilers correctly translate high-level programs into machine code, and why transformations performed are justifiable. This book presents 17 mutually reviewed invited papers organized in sections on methodology, programming, automation, compilation, and application.

This volume constitutes the proceedings of the "Second International Workshop on Cooperative Buildings (CoBuild'99) - Integrating Information, Organizations, and Architecture" held at the Carnegie Museum of Art in Pittsburgh on October 1-2, 1999. The success of the First International Workshop on Cooperative Buildings (CoBuild'98), held at GMD in Darmstadt in February 1998, showed that there is a demand for an appropriate forum to present research about the intersection of information technology, organizational innovation, and architecture. Thus, it was decided to organize a follow-up event. The decision of where to organize CoBuild'99 was straight forward. Since we had many high quality contributions from the United States (U. S. ) presented at CoBuild'98, we wanted to hold the second workshop in the U. S. reaching out to a large audience and at the same time turning it into an international series of events held in different places in the world. Due to the excellent work carried out at Carnegie Mellon University, it was an obvious choice to ask Volker Hartkopf from the Department of Architecture and Jane Siegel from the Human Computer Interaction Institute to be conference cochairs for CoBuild'99. The workshop is organized in cooperation with the German National Research Center for Information Technology (GMD), in particular the Integrated Publication and Information Systems Institute (IPSI) in Darmstadt providing continuity between the events.

Formal methods are coming of age. Mathematical techniques and tools are now regarded as an important part of the development process in a wide range of industrial and governmental organisations. A transfer of technology into the mainstream of systems development is slowly, but surely, taking place. FM'99, the First World Congress on Formal Methods in the Development of Computing Systems, is a result, and a measure, of this new-found maturity. It brings an impressive array of industrial and applications-oriented papers that show how formal methods have been used to tackle real problems. These proceedings are a record of the technical symposium ofFM'99: alo- side the papers describingapplicationsofformalmethods, youwill ndtechnical reports, papers, andabstracts detailing new advances in formaltechniques, from mathematical foundations to practical tools. The World Congress is the successor to the four Formal Methods Europe Symposia, which in turn succeeded the four VDM Europe Symposia. This s- cession re?ects an increasing openness within the international community of researchers and practitioners: papers were submitted covering a wide variety of formal methods and application areas. The programmecommittee re?ects the Congress's international nature, with a membership of 84 leading researchersfrom 38 di erent countries.The comm- tee was divided into 19 tracks, each with its own chair to oversee the reviewing process. Our collective task was a di cult one: there were 259 high-quality s- missions from 35 di erent countries.

Static analysis is increasingly recognized as a fundamental reasearch area aimed at studying and developing tools for high performance implementations and v- i cation systems for all programming language paradigms. The last two decades have witnessed substantial developments in this eld, ranging from theoretical frameworks to design, implementation, and application of analyzers in optim- ing compilers. Since 1994, SAS has been the annual conference and forum for researchers in all aspects of static analysis. This volume contains the proceedings of the 6th International Symposium on Static Analysis (SAS'99) which was held in Venice, Italy, on 22{24 September 1999. The previous SAS conferences were held in Namur (Belgium), Glasgow (UK), Aachen (Germany), Paris (France), and Pisa (Italy). The program committee selected 18 papers out of 42 submissions on the basis of at least three reviews. The resulting volume o ers to the reader a complete landscape of the research in this area. The papers contribute to the following topics: foundations of static analysis, abstract domain design, and applications of static analysis to di erent programming paradigms (concurrent, synchronous, imperative, object oriented, logical, and functional). In particular, several papers use static analysis for obtaining state space reduction in concurrent systems. New application elds are also addressed, such as the problems of security and secrecy.

Written by psychologists, this book focuses on the design of computer systems from the perspective of the user. The authors place human beings firmly at the centre of system design and so assess their cognitive and physical attributes as well as their social needs. The model used specifically takes into consideration the way in which computer technology needs to be designed in order to take account of all these human factors.
The text comprises a careful mix of theory and applications and is spiced throughout with practical examples of do's and don'ts in designing systems.

This book constitutes the refereed proceedings of the 11th International Conference on Computer Aided Verification, CAV'99, held in Trento, Italy in July 1999 as part of FLoC'99.
The 34 revised full papers presented were carefully reviewed and selected from a total of 107 submissions. Also included are six invited contributions and five tool presentations. The book is organized in topical sections on processor verification, protocol verification and testing, infinite state spaces, theory of verification, linear temporal logic, modeling of systems, symbolic model checking, theorem proving, automata-theoretic methods, and abstraction.

This volume provides the reader with a comprehensive introduction to system specification and design methods, with particular emphasis on structured and formal methods, method integration, concurrency and safety-critical systems. It contains both new material by Michael Hinchey and Jonathan Bowen, along with reprints of classic articles on high-integrity systems which have never before appeared together in a single volume. Among these classic articles are contributions from such leading names as Leslie Lamport, Nancy Leveson, and C.A.R. Hoare. Also included is a Foreword by David Lorge Parnas. High-Integrity System Specification and Design will provide practitioners and researchers convenient access to a range of essential essays - both classic and state-of-the-art - in a single volume. It provides them with details of specification and design approaches for this type of system, an overview of the development process, and evidence of how various classes of high- integrity systems may be approached and developed successfully.

This volume contains the proceedings of the 6th International Conference of the BCS Specialist Group on Information Systems Methodologies. The conference brought together papers on methodology issues related to the development and management of emerging technology based information systems. As usual there was a good range of papers addressing the 'soft' and 'hard' aspects of IS development and management. Methodologies for Developing and Managing Emerging Technology-based Information Systems will be of interest to practitioners who are engaged in systems development and modifying or aligning existing methodologies to practice.