[ We apologise if you receive this message more than once. ]
+----------------------------+
| Call for Participation |
| CHARME 2001 |
+----------------------------+
11th Advanced Research Working Conference on
Correct Hardware Design and Verification Methods
4-7 September 2001
Livingston-Edinburgh (Scotland)
http://www.dcs.gla.ac.uk/CHARME2001/
Co-sponsored by the IFIP TC10/WG10.5 Working Group on
Design and Engineering of Electronic Systems
CHARME 2001 is the eleventh in a series of working conferences devoted
to the development and use of leading-edge formal techniques and tools
for the design and verification of hardware and systems. It is the
biennial counterpart of FMCAD, which takes place every even year in
the USA.
The aim of CHARME 2001 is to bring together researchers and users from
academia and industry working in this active area of research. This
year, a special focus on technology interchange will be realised
through:
- a half day of tutorials aimed at industrial participation
- joint sessions and invited presentation with the 14th International
Conference on Theorem Proving in Higher Order Logics: TPHOLs 2001,
which will be co-located in Edinburgh.
The event will be held 4-7 September 2001 and hosted by the Institute for
System Level Integration in Livingston, Scotland, with a joint day with
TPHOLs in Edinburgh.
REGISTRATION
Registration is now open. Please visit the CHARME 2001 web site,
http://www.dcs.gla.ac.uk/CHARME2001, to register. A reduced registration fee
is available when registering for both CHARME 2001 and TPHOLs 2001 (see
below).
INVITED SPEAKERS
Steven D. Johnson, Indiana University
View from the Fringe of the Fringe
(Joint with TPHOLs 2001)
Alan Mycroft, University of Cambridge
Hardware Synthesis using SAFL and Application to Processor Design
ACCOMMODATION
Information on accommodation is now available on the CHARME 2001 web
site.
RELATED EVENTS
CHARME 2001 will be co-located with the 14th International Conference
on Theorem Proving in Higher Order Logics (TPHOLs 2001), which will be
held during 3 - 6 September 2001 in Edinburgh. A joint half-day
session is planned for Wednesday 5th September. Further information
on TPHOLs 2001 is available at http://www.dcs.gla.ac.uk/TPHOLs2001.
SPONSORS
CHARME 2001 is sponsored by the following organizations:
o Intel
o Siemens
o Esterel Technologies
CONTACT
Enquiries should be addressed to [EMAIL PROTECTED]
OUTLINE PROGRAMME
Tuesday 4th, morning: tutorials, afternoon: technical sessions.
Wednesday 5th: Joint technical sessions with TPHOLs 2001;
excursion; conference dinner.
Thursday 6th, Friday 7th: Technical sessions.
FULL PAPERS ACCEPTED TO DATE
Gerard Berry and Ellen Sentovich
Multicloc Esterel
Ricky Butler, V�ctor Carre�o, Gilles Dowek, and C�sar Mu�oz
Formal Verification of Conflict Detection Algorithms
Pankajkumar Chauhan, E. Clarke, S. Jha, J. Kukula, H. Veith, and D. Wang
Using Combinatorial Optimization Methods for Quantification Scheduling
Paul Curzon, Sofiene Tahar, and Iskander Kort
Hierarchical Verification Using an MDG-HOL Hybrid Tool
Nancy Day, Mark Aagaard, Byron Cook, and Robert Jones
A Framework for Microprocessor Correctness Statements
Eric Gascard and Laurence Pierre
Induction-Oriented Formal Verification in
Symmetric Interconnection Networks
Mark Greenstreet and Anthony Winstanley
Temporal Properties of Self-Timed Rings
Alan Hu and Alvin Albrecht
Register Transformations with Multiple Clock Domains
Christian Jacobi and Christoph Berg
Formal Verification of the VAMP Floating Point Unit
Roope Kaivola and Katherine Kohatsu
Proof Engineering in the Large: Formal Verification of
Pentium 4 Floating-Point Divider
Gila Kamhi, Fady Copty, Amitai Irron, Osnat Weissberg, and Nathan Kropp
Efficient Debugging in a Formal Verification Environment
Xuandong Li, Pei Yu, Zhao Jianhua, Li Yong, Zheng Tao, Zheng Guoliang
Efficient Verification of a Class of Linear Hybrid Automata
Using Linear Programming
Andrew Martin, Jayanta Bhadra, Jacob Abraham, and Magdy Abadir
Using Abstract Specifications to Verify PowerPC Custom
Memories by Symbolic Trajectory Evaluation
Stephen McKeever and Wayne Luk
Towards Provably-Correct Hardware Compilation Tools
Based on Pass Separation Techniques
Oliver M�ller and Rajeev Alur
Heuristics for Hierarchical Partitioning with
Application to Model Checking
Claus Schroeter and Javier Esparza
Net Reductions for LTL Model-Checking
Ofer Shtrichman
Pruning Techniques for the SAT-based Bounded Model Checking Problem
Satnam Singh, Mary Sheeran, and Koen Claessen
The Formal Specification and Verification of a Sorter Core
Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila,
and Marisa Venturini Zilli
Exploiting Transition Locality in Automatic Verification
Huibiao Zhu, Jonathan Bowen, and He Jifeng
From Operational Semantics to Denotational Semantics for Verilog
SHORT PAPERS ACCEPTED TO DATE
Dirk Beyer
Efficient Reachability Analysis and Refinement Checking of
Timed Automata Using BDDs
Ji He and Kenneth J. Turner
Specifying Hardware Timing with ET-LOTOS
Rajesh Radhakrishnan, E. Teica and R. Vemuri
Verification of Legal Schedules Using RTL Transformations
Tiberiu Seceleanu and Juha Plosila
Synchronous Pipeline Design in Action Systems
Fran�ois Siewe and Dang Van Hung
Deriving Real-Time Programs from Duration Calculus Specifications
Kenneth J. Turner and Ji He
Formally-Based Design Evaluation
Shmuel Ur, Gil Ratzaby, and Yaron Wolfsthal
Coverability Analysis Using Symbolic Model Checking
Karen Yorav, Sagi Katz, and Ron Kiper
Reproducing Synchronization Bugs with Model Checking
