Cristian Gherghina
Welcome!
As of Nov 2014 I joined Google Switzerland as a Software Engineer.
Previously, from October 2013 until October 2014, I worked as 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
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 4Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
Joao F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin. STTT Vol 16 Issue 4Barriers 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
Teaching
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
Contact
Office address: Google Zurich, Switzerland
Email: cris at [fam_name].xyz