9th Asian School on Computer Science

Date : 22-29 November, 1996
Venue : Rayong, Thailand
Organized by : Asian Institute of Technology (Thailand)
Institut National de Recherche en Informatique et en Automatique (France)

The Asian School on Computer Science is series of courses organized by the Asian Institute of Technology jointly with INRIA (France). One of the main objectives of the school is to assist university lecturers and researchers in the Asian region in keeping themselves updated with the fast growing research activities in computer science.

Interested researchers or Post-graduate students are welcome.

The school is to be held prior to the 1996 Asian Computer Science Conference (2-5 December, 1996), Singapore.

TOPIC : Synthesis and Verification of Finite-State Machines Based Systems

SPEAKERS :

Gerard Berry
Ecole des Mines/INRIA, France
Nicolas Halbwachs
CNRS, France
Ellen Sentovich
Cadence Berkeley Laboratories, USA

ABSTRACT :

Automatic sythesis and verification of computer systems is a domain of growing importance, since errors in these systems can have dramatic economic or human consequences. In some application domains, synthesis and verification can be automatically driven on a finite model (state graph) of the system. Such methods concern circuits --- which are intrinsically finite-state --- but also communication protocols, and industrial control systems, the critical properties of which can often be analyzed on a finite model. This approach has been intensively studied during the last 15 years; also, it gave raise to actual verification tools, and to large scale applications. Adressed problems concern specification (what is to be verified, and how to express it?)

Application Areas

- Circuit synthesis, optimization, and verification
- Software and Hardware synthesis, optimization, and verification from Synchronous Languages

COURSE OUTLINE :

Explicitly Given Finite State Machines

- Software Implementation
- Bisimulation techniques for verification
- Linear-time and branching-time temporal logics

Implicitly Given Finite State Machines

- Representation by Boolean Logic Networks
- Standard Boolean techniques (sums of products, kernels, don't cares, etc...)
- Binary Decision Diagrams (BDDs)
- Latch and Logic minimization
- Implicit state space exploration: dealing with the state explosion problem
- Implicit temporal logic verification
- Verification by Observers

Real-Time verification

- Adding counters to FSMs
- Exact and approximate verification techniques

REGISTRATION :

US$1,200 (twin-shared accomodation (8 nights), three meals and two coffee breaks per day, BKK-Rayong-BKK, course materials and attendences of all sessions)

SCHEDULE : Click here

SPONSORS :

National Science and Technology Development Agency (NSTDA)
Foundation for Computer and Communications Education (C & C Education Foundation)

CONTACT :

Ms. Orapin Charoenchai
Computer Science and Information Management
Asian Institute of Technology
Km. 42 Paholyothin Highway
Klong Luang, Pathumthani 12120
Thailand
Phone : +66 2 524 5716
Fax : +66 2 524 5721
E-mail : orapin@cs.ait.ac.th