Symbolic model checking is a formal technique for the verification of
finite-state concurrent systems. Symbolic model checkers (e.g. SMV,
VIS) have been used to verify industrial systems, ranging from
hardware to communication protocols to safety critical plants and
procedures. Symbolic model checking is applied in technology transfer
projects, and is the core technique for several industrial
verification tools.
The aim of the workshop is to bring together active developers and
users of symbolic model checkers, compare state of the art model
checking techniques (e.g. compositional reasoning, abstraction,
partitioning), discuss experimental results and experience reports,
and promising directions for future research.
Program
More than 20 papers were submitted to SMC99, 9 of which were selected
by the program committee to be presented.
The complete program of SMC99 can be found here. It
includes presentations by two keynote speakers:
Accepted contributions appear in the workshop proceedings, published
as Electronic Notes in Theoretical Computer Science (ENTCS).
To ensure dissemination, the proceedings will be electronically
available from the workshop web page for a limited time before and
after the workshop, and on hardcopy for the participants. The
proceedings will also be electronically available from the ENTCS
repository.
The publication of selected papers on a journal special issue is
currently being evaluated.
Sponsorship
We gratefully ackowledge the sponsorship provided by IBM Haifa
Research Laboratory for the preparation of the proceedings.
Important Dates
Submission deadline:
March 26
Notification of acceptance:
May 17
Final version due:
June 13
SMC99:
July 6
CAV & CADE:
July 7 - 10
LICS & RTA:
July 2 - 5
Costs
Registration to the workshop will include copy of the proceedings,
lunch, and two coffee breaks for all participants. On-site
registration might not guarantee the availability of proceedings.
Please refer to the on-line registration
forms for the details.