Date: Wed, 14 Mar 2001 16:16:03 -0800 (PST) From: Jeff Foster <jfoster@EECS.Berkeley.EDU> Subject: workshop announcement (fwd) Message-ID: <Pine.LNX.4.30.0103141610510.20085-100000@lagaffe.cs.berkeley.edu> This workshop may be of interest to some of you. I'm not sure whether I should have forwarded this to everyone, but I couldn't tell from the announcement header how widely circulated the cfp was. (Did everyone already get this announcement through some other channel?) Jeff ---------- Forwarded message ---------- Date: Wed, 14 Mar 2001 12:52:05 -0500 (EST) From: Scott Stoller <stoller@cs.sunysb.edu> To: types@cis.upenn.edu Cc: stoller@cs.sunysb.edu Subject: workshop announcement [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----] [This workshop is not mainly about types, but it is related. Static analysis is mentioned twice in the CFP, and types are an important form of static analysis. Papers like "Types for safe locking" are relevant to the workshop, because locking disciplines can be used to optimize model checking. -- Scott Stoller] Workshop on Software Model Checking http://www.cs.sunysb.edu/~stoller/softmc01/ July 23, 2001 Paris, France The growing importance of model checking in hardware verification and the difficulty of producing correct software are driving a growing interest in the application of model checking to software. This leads to many challenges of scientific and practical interest, both in core model checking technology and in supporting techniques, such as program analyses and transformations that help automate abstraction of the data state and reduction of the control state. This workshop covers all aspects of software model checking and supporting techniques, ranging from verification of high-level requirements specifications to model checking of low-level bytecode. Theoretical results and case studies are equally welcome. Techniques that provide limited guarantees or that work for limited classes of properties are also of interest. We especially encourage submissions that deal with general-purpose programming languages or other languages with similar features. Topics of interest include but are not limited to: * Model checking for conventional programming languages or other languages with similar features, such as recursion, references, dynamic memory allocation, or object-oriented constructs. * Model checking for design notations: UML (including Statecharts), RSML, etc. * Static analysis and state-space reductions: slicing, partial-order reductions, symmetry reductions, etc. * Abstraction for software model checking * Applications of model checking to software verification/debugging * State-less model checking * Advanced testing approaches, e.g., test-case generation via model checking. * Heuristic search for model checking The workshop has a dual mission: it aims to introduce people to the field of software model checking and to be a forum for describing new research. Hence, the workshop will consist of invited presentations by leaders in the field and a selection from the submitted papers. We expect to publish the proceedings in Electronic Notes in Theoretical Computer Science, in a volume that also contains papers from other post-CAV'01 workshops. The workshop will be held after CAV'01 in the same location (la Mutualite). CAV'01 follows FMICS'01 and SAS'01. ==== INVITED SPEAKERS ==== The invited speakers will describe their leading-edge work in combining the power of static analysis and model checking. This is an important direction for the field of software model checking and is an especially appropriate topic at a workshop co-located with SAS'01 and CAV'01. Sriram Rajamani will describe the SLAM Project. John Hatcliff will describe the Bandera Project. ==== SUBMISSION INFORMATION ==== Submissions should be in PostScript format. The body of each submission should start with a short abstract and should be at most 10 pages long. The submission may include in addition an appendix containing technical details, which reviewers may read or not, at their discretion. The submission should contain the contact author's physical and e-mail addresses and phone number. Submissions should be sent by email to softmc01@cs.sunysb.edu . ==== DATES ==== Submission deadline: May 15, 2001 Acceptance notification: June 15, 2001 Final version: July 1, 2001 ==== CO-CHAIRS ==== Scott Stoller Willem Visser Computer Science Dept. Automated Software Engineering group State Univ. of New York at Stony Brook NASA Ames Research Center ==== PROGRAM COMMITTEE ==== Tom Ball, Microsoft Research David Dill, Stanford University Hubert Garavel, INRIA Rhone-Alpes / VASY Patrice Godefroid, Bell Laboratories, Lucent Technologies Susanne Graf, Verimag Gerard Holzmann Bell Laboratories, Lucent Technologies Scott Stoller, State University of New York at Stony Brook Willem Visser, NASA Ames Research Center
This archive was generated by hypermail 2b30 : 11/04/02 PST