Lab Affiliation(s):
Computer Science and Artificial Intelligence Laboratory
Post Doc Sponsor / Advisor:
Armando Solar-Lezama
Areas of Expertise:
  • Program Verification
  • Program Synthesis
  • Logics
Date PhD Completed:
August, 2013
Expected End Date of Post Doctoral Position:
August 15, 2015

Xiaokang Qiu

  • Post Doctoral

MIT Unit Affiliation: 

  • Electrical Engineering & Computer Science

Lab Affiliation(s): 

Computer Science and Artificial Intelligence Laboratory

Post Doc Sponsor / Advisor: 

Armando Solar-Lezama

Date PhD Completed: 

Aug, 2013

Top 3 Areas of Expertise: 

Program Verification
Program Synthesis
Logics

Expected End Date of Post Doctoral Position: 

August 15, 2015

CV: 

Research Projects: 

Strand: A logic combining heap structures and data Strand ("STRucture ANd Data") is a logic that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. More details can be found here.

Dryad: Recursive proofs for inductive tree data-structures Dryad is a dialect of separation logic with recursive definitions. Dryad provides natural proofs for general properties of structure, data, and separation. More details can be found here.

Pasket: a PAttern SKETcher Pasket is a tool for synthesizing models of the observer pattern for event-driven frameworks. More details can be found in this draft.

Thesis Title: 

Automatic Techniques for Proving Correctness of Heap-Manipulating Programs

Thesis Abstract: 

Reliability is critical for system software, such as OS kernels, mobile browsers, embedded systems and cloud systems. The correctness of these programs, especially for security, is highly desirable, as they should provide a trustworthy platform for higher-level applications and the end-users. Unfortunately, due to its inherent complexity, the verification process of these programs is typically manual/semi-automatic, tedious, and painful. Automating the reasoning behind these verification tasks and decreasing the dependence on manual help is one of the greatest challenges in software verification. This dissertation presents two logic-based automatic software verification systems, namely Strand and Dryad, that help in the task of verification of heap-manipulating programs, which is one of the most complex aspects of modern software that eludes automatic verification. Strand is a logic that combines an expressive heap-logic with an arbitrary data-logic and admits several powerful decidable fragments. The general decision procedures can be used in not only proving programs correct but also in software analysis and testing. Dryad is a family of logics, including Dryad-tree as a first-order logic for trees and Dryad-sep as a dialect of separation logic. Both the two logics are amenable to automated reasoning using the natural proof strategy, a radically new approach to software verification. Dryad and the natural proof techniques are so far the most efficient logic-based approach that can verify the full correctness of a wide variety of challenging programs, including a large number of programs from various open-source libraries. They hold promise of hatching the next-generation automatic verification techniques.

5 Recent Papers: 

Natural Proofs for Data-Structure Manipulation in C using Separation Logic

Edgar Pek, Xiaokang Qiu, P. Madhusudan

In Proc. 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14), 2014. (Acc rate: 18%)

Natural Proofs for Structure, Data, and Separation

Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, P. Madhusudan

In Proc. 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '13), 2013. (Acc rate: 17%)

Recursive Proofs for Inductive Tree Data-Structures

P. Madhusudan, Xiaokang Qiu, Andrei Stefanescu

In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '12), 2012. (Acc rate for PC submissions: 18%)

Efficient Decision Procedures for Heaps Using STRAND

P. Madhusudan, Xiaokang Qiu

In Proc. 18th International Static Analysis Symposium (SAS '11), LNCS 6887, 2011. (Acc rate: 33%)

Decidable Logics Combining Heap Structures and Data

P. Madhusudan, Gennaro Parlato, Xiaokang Qiu

In Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11), 2011. (Acc rate: 23%)

Contact Information:
32 Vassar Street
32-G716
Cambridge
MA
02139