Publications

On-going investigations or under submission
  • Learning concurrent program specifications
  • A Coq certified fractional permissions prover
Conference Papers
  • A Resource-Based Logic for Termination and Non-Termination Proofs
    Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin. ICFEM 2014. (pdf) (bib)
  • Shape Analysis via Second-Order Bi-Abduction (pdf) (bib) (slides) (report) (online system)
    Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin. CAV 2014.
  • A Proof Slicing Framework for Program Verification (pdf) (bib)
    Ton Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin. ICFEM 2013.
  • Decision Procedures Over Sophisticated Fractional Permissions (pdf) (bib)
    Xuan Bach Le, Cristian Gherghina, Aquinas Hobor. APLAS 2012.
  • A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification (pdf) (bib) (ppt)
    Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin. CAV 2011.
  • Structured Specifications for Better Verification of Heap-Manipulating Programs (pdf) (bib)
    Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. FM 2011.
  • Barriers in Concurrent Separation Logic (pdf) (bib) (ppt) (prototype)
    Aquinas Hobor, Cristian Gherghina. ESOP 2011.
  • A Specification Logic for Exceptions and Beyond (pdf) (bib) (ppt)
    Cristian Gherghina, Cristina David. ATVA 2010.
  • Translation and optimization for a core calculus with exceptions (pdf) (bib) (ppt)
    Cristina David, Cristian Gherghina, Wei-Ngan Chin. PEPM 2009.
Journal Papers
  • Expressive Program Verification via Structured Specifications (pdf) (bib)
    Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. STTT Vol 16 Issue 4
  • Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK (pdf) (bib)
    Joao F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin. STTT Vol 16 Issue 4
  • Barriers in Concurrent Separation Logic: Now with Tool Support! (pdf) (bib)
    Aquinas Hobor, Cristian Gherghina. LMCS (ESOP 2011).
Posters & Tool Demo
  • Synthesizing Shape Predicate via Second-Order Bi-Abduction
    Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin . APLAS 2013.
  • A HIP and SLEEK verification system (pdf) (bib)
    Wei-Ngan Chin, Cristina David, Cristian Gherghina. OOPSLA Comp 2011.
  • Automated Verification Using Unified Control Flows (pdf) (slides) (bib) (best poster award)
    Cristian Gherghina, Cristina David. TASE 2009.
  • Implementing a Modular OO Verifier (pdf)
    Cristian Gherghina, Cristina David, Huu Hai Nguyen, Wei-Ngan Chin. APLAS2007.
Technical Reports
  • A Resource-Based Logic for (Non-)Termination Proofs
    Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin. (pdf)
  • Shape Analysis via Second-Order Bi-Abduction
    Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin. (pdf)
Program committee member APLAS 2014
    AEC member POPL 2015
      Refereed for APLAS 2009, POPL 2010, ATVA 2010, ICFEM 2011, APLAS 2011, VMCAI 2012, CPP 2012, SAS 2013, ATVA 2013, PEPM 2014, FM 2014
        Coauthors