The seminar will be held at 新竹市 交通大學 電機資訊大樓 七樓 on Decemer 29 (Monday), 1997. A map of NCTU is available at http://www.cis.nctu.edu.tw/~plas/gif/nctucampus.gif.
Students are especially welcomed to attend this seminar series. There is no registration fee for the seminars. Free lunches will be provided. To help plan the event, however, please send a plain-text e-mail to firstname.lastname@example.org or fax to (03) 5721490 楊武 with your name (both in Chinese and English) and your current affiliation if you plan to attend. Further information about this event, including abstracts of the talks, will be available from WWW at http://www.cis.nctu.edu.tw/~plas/plas1997.html.
Campus accommodation is available. The cost is $600 per night per room (for a room with 2 beds). If you need to reserve a guest room, please send your order to email@example.com. Since the room is on the first-come first-serve base, please reserve the room as early as possible.
In this talk, we survey some of the recent results in the verification of infinite-state systems. In particular, we focus on the equivalence problem and the model checking problem. Given two infinite-state systems, the equivalence problem is to determine whether the two systems are `equivalent' with respect to a certain notion of equivalence. The model checking problem is that of deciding whether a given infinite-state system satisfies a formula in a certain temporal logic. The families of infinite-state systems addressed in this talk include Petri nets, pushdown automata, Basic Process Algebra, Basic Parallel Processes, and more.
Concurrent programs can be very subtle and error-prone. The difficulty is due not to the size of the code, but to the intrinsic complexity of concurrency. Researchers continue to make serious mistakes in designing mutual exclusion algorithms even of the size less than 20 statements. The mistakes can be traced to poor understandings on the subtleties of either concurrent processes or the hardware primitives. Verification disciplines could have prevented such mistakes. In this talk, we will examine two particular small programs that use the fetch_and_store primitives. Both were published in recent IEEE periodicals but were later found incorrect by our group, one violating mutual exclusion and the other deadlock freedom. We will illustrate some verification techniques that are easy to apply manually. By showing what were done wrong and what could have been done right, we are reminded, once again, that manual verification on concurrent algorithms, with some reasonable level of rigor, is not as difficult as we usually perceive. And the benifit is clear: better understandings of one's own design.
We describe the design and implementation of system architecture to support object introspection in C++. An introspective object permits observation and change to its own state by a general mechanism that is applicable to objects of all classes. This general mechanism allows the construction of applications where objects are late-binding and the interactions between them are highly dynamic.
Unlike Java, which provides full support for object introspection, C++ has limited built-in introspective capability via its Run-Time Type Information (RTTI) and related facilities. For example, in C++ one cannot query an object for methods that can be applied to it. We show how such introspective information can be collected at compile-time by parsing class declarations, and be used to build a supporting environment for object introspection at run-time.
Our approach is non-intrusive because it requires no change to the original class declarations and libraries, and it guarantees compatibility between objects before and after the addition of introspective capability. This is important if one wants to integrate third-party class libraries, which are often supplied as black boxes and allow no modification, into highly dynamic applications. We show two applications that are built on top of our introspective environment. The first is a generic facility for automatic I/O support of complex C++ objects. The other is a class exerciser that allows interactive execution of dynamically loaded C++ class libraries.
(Joint work with Tyng-Ruey Chuang and Chien-Min Wang)
Generalized quantifiers are frequently-used phrases such as:
three, Chamberlin's three, more than three, fewer than three, at most three, exactly three, all but three, half, no more than three, not more than half, most but not all, at least two and not more than three, more than half but not all, neither Chamberlin's nor Astrahan's.
Since these quantifiers can be quite complex and are difficult to characterize, they are not treated explicitly by most query languages. Unfortunately, as shown in the introduction section, this lack of treatment forces users to write long and error-prone queries.
In this paper, we will show that a well-defined subset of quantifiers, reducible-to-safe quantifiers, can be implemented with operators supported by SQL2. Syntactic sugaring is then designed for these quantifiers to show they can be incorporated into SQL2 effectively, in a way that permits shorter, more natural queries.
We concentrate our discussion and implementation on SQL2, since it is the dominant query language, and most databases support some kind of SQL-like interface. However, our discussion also should be applicable to other query interfaces.