Talks by Chinese Academicians

Colleagues and students are cordially invited to attend a lecture given by Chinese Academician on 4 November 2011 (Friday).

Register for the talk.

A Formal Semantics for Automated Program Debugging

A Formal Semantics for Automated Program Debugging

Speaker: Professor LI Wei, State Key Laboratory of Software Development Environment Beihang University

Date: 4 November 2011 (Friday)
Time: 11:30-12:30pm
Venue: Leung Yat Shing Lecture Theater (LT-F) (near lifts 25/26), HKUST

Abstract:

A debugging process starts when a successful test case finds that its outcome is not consistent with the expected results. Debugging is a hard job for programmers, and its efficiency still heavily depends on programmers' insight and their experiences, even in the presence of a host of debugging tools and theories.

This works aims to build an operational semantic framework for automated debugging. We divide a general debugging process into three phases: tracing process, locating process, and fixing process. The first two phases are accomplished by a tracing procedure and a locating procedure, respectively. The tracing procedure reproduces the execution of the successful test cases with well-designed data structures, and saves necessary information for the locating procedure.

The locating procedure will use the information obtained by the tracing procedure to locate ill-designed statements and generates an equation system, which will be used to fix the bug. We provide a structural operational semantics with trace stacks, to define the functions of the tracing procedure. We also give a structural operational semantics for debugging, to specify the functions of locating procedure. We show that both procedures guarantee to terminate.

It turns out that for a given successful test case, there exist three different types of solutions: 1. the bug is solvable, and the program can be repaired; 2. there exists a structural design error in the program; while the equations generated at each round of the locating procedure are solvable, a new bug may arise when fixing the old bug; and 3. there exists a logical design error, and the fixing equations are not solvable.

About the Speaker:

New Technology from the Quantum World - Quantum Information

New Technology from the Quantum World - Quantum Information

Speaker: Prof GUO Guangcan, Director, Key Laboratory of Quantum Information

Date: 4 November 2011 (Friday)
Time: 11:30-12:30pm
Venue: Room 3006 (via lift 4), HKUST

Abstract:

The fundamental feature of the quantum world is its uncertainty, whose strangeness is usually beyond the comprehensions of the people from the classical world. As our exploration in the quantum world grows deeper, we naturally look forward to new technologies based on its unique characters, with the aim to apply these novel technologies in the classical world of certainty. This leads to the birth of quantum information. In this presentation, I will first discuss briefly the intriguing features of the quantum world, and then introduce the fundamental principles as well as the latest development for quantum cryptography and quantum computation.

About the Speaker: