USTC-Yale Joint Research Center for High-Confidence Software

The 3rd Asian-Pacific Summer School on Formal Methods will be held in Suzhou, China in August 13-21, 2011.

   Recently, LIANG Hongjin, FENG Xinyu and FU Ming from USTC-Yale Joint Research Center for High-Confidence Software had a paper “A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations” accepted by the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). This is the first paper accepted by POPL whose first affiliation is from Chinese mainland, and University of Science and Technology of China (USTC) becomes the first institution receiving the honor.

 
On April 25, 2011 at the invitation of USTC-Yale joint research center for confidence software, Dr. Christian Urban from German Technical University of Munich paid a visit to USTC Suzhou Institute. Dr. Christian received his PhD degree from Cambridge University in 2000 and after that he has been engaged in research work related to theorem proof in Cambridge University, Princeton University and Technical University of Munich. In recent years, he mainly focuses on theoretical fields like auto theorem proof , program language,etc.
 

On May 11, 2011, Dr.Søren Debois came to USTC-Yale joint research center and paid a two-day visit.Søren Debois got his PhD under the supervision of Lars Birkedal and Thomas Hildebrandt in 2008 at the IT University of Copenhagen, where he is currently employed as a post doc. His dissertation and subsequent research has centered on the development and application of the theory of bigraphs, notably "sortings", notions of higher-order bigraphs, notions of refinement for bigraphs, and applications of bigraphs to ubiquitous computing.

The 3rd Asian-Pacific Summer School on Formal Methods will be held in Suzhou, China in August 13-21, 2011. The objective is to teach students the principles and practice of programming with the proof assistant Coq, as in previous years (2009 and 2010), and to show them the state of art applications of proof assistants and theorem provers in formal methods.
 

On Dec 16 ,2010, Director of Sino French Laboratory for computer science, automation and applied mathematics (LIAMA), professor Vania Joloboff came to our research center and give us a masterly speech about his recently work on SlmSoC. SimSoC is a simulation software to fully simulate hardware platforms. The simulator is meant to be used by either software developers who can validate their software or by hardware developers who want to validate an architecture and calibrate hardware design to meet the application requirements.

On Nov 25,2010,Dr.Gang Tan  was invited to visit USTC-Yale joint research center for high confidence software. During that time, Gang Tan gave us a brief talk about his research, "GoNative", which is used to enable safe execution of native code in type-safe programming languages such as Java, Python, and C#.
Please check here to get more details about the talk。
Dr.Gang Tan

May 19, 2010, Professor Shao Zhong made a presentation in classroom 3124 of "Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software".Professor Yiyun Chen hosted the talk. Students of Computer Science and other interested students and teachers attended the meeting part.

 Nov 19, 2009, Director of Sino French Laboratory for computer science, automation and applied mathematics (LIAMA), professor Jean-Pierre Jouannaud and Dr. Pierre-Yves Strub came to our research center and paid a two-day visit. LIAMA is a joint lab of INRIA and universities of China including Tsinghua University. We introduced our joint work with Yale and on-going work. Post Doc. Guo Yu and Li Zhaopeng gave talks about certified operating system kernel and certifying compiler. Prof. Jouannaud and Dr.

September 3 to 5, 2009, Yves Bertot, a senior researcher of INRIA was invited to visit USTC-Yale joint research center of high confidence software. During that time, Yves Bertot gave us a brief talk about the  proof assistant "Coq" and how to formally describe programming language semantics and do static analysis with it. Post-doc Yu Guo, Zhaopeng Li and Dr. Ming Fu reported about projects on Operating System Verification, Certifying Compiler, Concurrent Program Verification, respectively. Yves Bertot had an in-depth discussion about these projects with us.