Cristian Gherghina

Welcome!

As of Sep 2024 I joined Deepcode / Snyk as a Software Engineer working on the Snyk static analysis tool.  Previously, between 2014 and 2024 I worked at Google Switzerland as a Software Engineer. Before that, from October 2013 until October 2014, I worked as a research fellow at Singapore University of Technology and Design .

And before I was a researcher at Computer Science Department of School of Computing, National University of Singapore working in the HIP/SLEEK separation logic verifier project, led by Professor Wei-Ngan Chin. In Nov 2012 I successfully defended my Ph.D. thesis, "Efficiently Verifying Programs with Rich Control Flows" which was developed under the supervision of Professor Wei-Ngan Chin.

My research interests are mostly focused on formal methods used in programming languages. They include programming languages semantics, specification logics, program verification, static analysis. More specifically I was involved in the development of richer specification logics aimed at helping program verifiers handle richer programming languages. I am working on making use of separation logic variants in order to verify functional correctness of java-like programs. As such I am one of the people engaged in developing the SLEEK separation logic entailment checker and HIP program verifier.

 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.

• Shape Analysis via Second-Order Bi-Abduction
  Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin. CAV 2014.

• A Proof Slicing Framework for Program Verification
  Ton Chanh Le, Cristian Gherghina, Razvan Voicu, Wei-Ngan Chin. ICFEM 2013.

• Decision Procedures Over Sophisticated Fractional Permissions
  Xuan Bach Le, Cristian Gherghina, Aquinas Hobor. APLAS 2012.

• A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification
  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
  Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. FM 2011.

• Barriers in Concurrent Separation Logic
  Aquinas Hobor, Cristian Gherghina. ESOP 2011.

• A Specification Logic for Exceptions and Beyond
  Cristian Gherghina, Cristina David. ATVA 2010.

• Translation and optimization for a core calculus with exceptions
  Cristina David, Cristian Gherghina, Wei-Ngan Chin. PEPM 2009.

Journal Papers

• Expressive Program Verification via Structured Specifications
  Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin. STTT Vol 16 Issue 4

• Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
  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!
  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
  Wei-Ngan Chin, Cristina David, Cristian Gherghina. OOPSLA Comp 2011.

• Automated Verification Using Unified Control Flows (best poster award)
  Cristian Gherghina, Cristina David. TASE 2009.

• Implementing a Modular OO Verifier
  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.

• Shape Analysis via Second-Order Bi-Abduction
  Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin.

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

• Chin Wei-Ngan Shengchao Qin Aquinas Hobor

• Razvan Voicu Cristina David Quang Loc Le

• Florin Craciun   Huu Hai Nguyen     Xuan Bach Le

• Joao F. Ferreira Guanhua He

Invited lectures

• at NUS, Singapore

  • 2014 fall: CS4215 Programming Language Implementation: lectures on "Domain Specific Languages"

  • 2013 fall: CS3234 Logic and Formal Systems: lecture on "practical, theorem proving based, program verification"

• at UPB, Bucharest

  • 2011 fall: HPC programming methods and techniques : lectures on "introduction to verification of parallel programs"

  • 2011 fall: Parallel and Distributed Systems : lectures on "introduction to verification of parallel programs"

Teaching

• at NUS, Singapore

  • 2010 Fall : CS1102 Data structures and algorithms, lab coordination and grading

  • 2010 Spring: CS5202 Foundation in Programming Languages, grading

  • 2009 Fall : CS1102 Data structures and algorithms, teaching assistant and grading

  • 2009 Fall : CS4212 Compiler Design, consultations, assignment design and grading

• at UPB, Bucharest

  • 2007 Fall : Microprocessor-based Systems Design, teaching assistant