NEWS
Introduction to the Joint Center
Fri, 07/24/2009 - 11:54 — nateResearch on High-Confidence Software (HCS) intends to develop new cutting-edge technologies and tools that will dramatically improve the dependability of today's computer software. Successful research in HCS requires a deep knowledge and shared expertise of a large number of sub-disciplines in computer science, ranging from formal methods, programming languages, compilers, operating systems, computer security, proof assistants, software engineering, computer architecture, to embedded systems.
Prof. Zhong Shao of Joint Center from Yale University Gave Talks at School of Computer Science of USTC
Wed, 05/26/2010 - 22:52 — nateMay 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.
Sino French Laboratory(LIAMA) Visited Joint Research Center
Sat, 11/21/2009 - 00:37 — nateNov 19, 20009, 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.
Researcher Yves Bertot visited Joint Center
Mon, 09/07/2009 - 14:18 — nateSeptember 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.
Automated Theorem Prover with Machine-Checkable Proofs
Mon, 08/31/2009 - 13:44 — nate
- Login to post comments
Certifying Compiler for C-like Programming Language
Mon, 08/31/2009 - 13:43 — nate
- Login to post comments
Parallel Programming Language with Shared Resource Specification
Mon, 08/31/2009 - 13:41 — nate
- Login to post comments
Verifying Concurrent Software for Multi-Core Machines
Mon, 08/31/2009 - 13:40 — nate
- Login to post comments
Coordinated Information Processing in Wireless Sensor Networks
Mon, 08/31/2009 - 13:37 — nate
- Login to post comments
