[UAI] CHARME 2001 Call For Participation

From: simon gay (simon@dcs.gla.ac.uk)
Date: Wed May 30 2001 - 10:00:29 PDT

  • Next message: Compulog Americas: "[UAI] CFP: ICTAI'01"

    [ 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 charme2001@dcs.gla.ac.uk

    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



    This archive was generated by hypermail 2b29 : Wed May 30 2001 - 10:02:55 PDT