Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings
Ahmed Bouajjani, Oded Maler
Springer Science & Business Media, Jun 19, 2009 - Computers - 722 pages
This volume contains the proceedings of the 21st International Conference on Computer-Aided Veri?cation (CAV) held in Grenoble, France, between June 28 and July 2, 2009. CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. Its scope ranges from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the underlying algorithms and techniques. Everyinstanceofaconferenceisspecialinitsownway.ThisCAVisspecialfor at least two reasons: ?rst, it took place in Grenoble, the place where the CAV series started 20 years ago. Secondly, there was a particularly large number of paper submissions: 135 regular papers and 34 tool papers, summing up to 169 submissions. They all went through an active review process, with each submissionreviewedbyfourmembersoftheProgramCommittee.Wealsosought external reviews from experts in certain areas. Authors had the opportunity to respond to the initial reviews during an author response period. All these inputs wereusedbytheProgramCommitteeinselectinga?nalprogramwith36 regular papers and 16 tool papers. In addition to the presentation of these papers, the program included the following: – Four invited tutorials: • Rachid Guerraoui (EPFL Lausanne, Switzerland): Transactional M- ory: Glimmer of a Theory. • Jaeha Kim (Stanford, USA): Mixed-Signal System Veri?cation: A High- Speed Link Example. • Jean Krivine (Institut des Hautes Etudes Scienti?ques, France): M- elling Epigenetic Information Maintenance: A Kappa Tutorial. • JosephSifakis (CNRS-VERIMAG,France):Component-BasedConstr- tion of Real-Time Systems in BIP.
What people are saying - Write a review
We haven't found any reviews in the usual places.
abstraction algorithm allows analysis applied approach array assignment assume automatically Boolean bound called checking clauses complexity computation concurrent condition consider consists constraints construction contains context corresponding counter deﬁned deﬁnition denote dependency described diﬀerent domain equivalent event example execution exists expression extension Figure ﬁnite ﬁrst formal formula function given global Heidelberg holds implementation initial input instance integer invariants iteration language linear LNCS logic loop memory method Note obtained operations optimal pair path performance possible predicate present problem procedure proof properties reachable reduce relation represent require respectively rule satisﬁability semantics sequence simulation solution solver solving speciﬁcation Springer step strategy structure symbolic techniques Theorem theory thread tion tool transaction transition translation validation variables veriﬁcation