CV.tex

\newif\iftechnical\technicaltrue

%% start of file `template.tex'.
%% Copyright 2006-2015 Xavier Danaux (xdanaux@gmail.com).
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License version 1.3c,
% available at http://www.latex-project.org/lppl/.


\documentclass[10pt]{moderncv}        % possible options include font size ('10pt', '11pt' and '12pt'), paper size ('a4paper', 'letterpaper', 'a5paper', 'legalpaper', 'executivepaper' and 'landscape') and font family ('sans' and 'roman')

% moderncv themes
\moderncvstyle{classic}                             % style options are 'casual' (default), 'classic', 'banking', 'oldstyle' and 'fancy'
\moderncvcolor{blue}                               % color options 'black', 'blue' (default), 'burgundy', 'green', 'grey', 'orange', 'purple' and 'red'
%\renewcommand{\familydefault}{\sfdefault}         % to set the default font; use '\sfdefault' for the default sans serif font, '\rmdefault' for the default roman one, or any tex font name
%\nopagenumbers{}                                  % uncomment to suppress automatic page numbering for CVs longer than one page

% character encoding
%\usepackage[utf8]{inputenc}                       % if you are not using xelatex or lualatex, replace by the encoding you are using
%\usepackage{CJKutf8}                              % if you need to use CJK to typeset your resume in Chinese, Japanese or Korean


\usepackage{fontawesome5}  % for extra icons
\usepackage{enumitem}  % manage spacing for enum
% prevent orphan section titles at the last line
\usepackage{needspace}
\let\oldsection=\section
\renewcommand{\section}{%
  \needspace{\baselineskip}
  \oldsection
}

% adjust the page margins
\usepackage[scale=0.8]{geometry}
% \usepackage{titlesec}                            % used to change the section spacing
% \setlength{\hintscolumnwidth}{2.25cm}              % if you want to change the width of the column with the dates
%\setlength{\makecvtitlenamewidth}{10cm}           % for the 'classic' style, if you want to force the width allocated to your name and avoid line breaks. be careful though, the length is normally calculated to avoid any overlap with your personal info; use this at your own typographical risks...

% personal data
\name{Cheng}{Zhang}
\title{Curriculum vitae}
\email{czhang03@bu.edu}                               % optional, remove / comment the line if not wanted
\homepage{czhang03.github.io}              % optional, remove / comment the line if not wanted
\social[github]{czhang03}                              % optional, remove / comment the line if not wanted

% uncomment the following on resumes
% \extrainfo{\faFile{}~\href{https://cdn.jsdelivr.net/gh/czhang03/CV@master/CV.pdf}{Full Curriculum vitae}}


% bibliography adjustments (only useful if you make citations in your resume, or print a list of publications using BibTeX)
%   to show numerical labels in the bibliography (default is to show no labels)
\makeatletter\renewcommand*{\bibliographyitemlabel}{\@biblabel{\arabic{enumiv}}}\makeatother
%   to redefine the bibliography heading string ("Publications")
%\renewcommand{\refname}{Articles}

% bibliography with multiple entries
%\usepackage{multibib}
%\newcites{book,misc}{{Books},{Others}}
%----------------------------------------------------------------------------------
%            content
%----------------------------------------------------------------------------------
\begin{document}
%\begin{CJK*}{UTF8}{gbsn}                          % to typeset your resume in Chinese using CJK
%-----       resume       --------------------------------------------------------

% Display the CV title
\makecvtitle{}

% set the space between \cventry
\setlength{\parskip}{2.5px}
\linespread{1.3}
\selectfont


\section{Education}

\cventry{2018 --- 2024}
{Computer Science, Ph.D.} {}
{Boston University}
{Boston, MA, USA}
{\textbf{Thesis}: Two Variants of Kleene Algebra and Their Applications.}  % description

% \cventry{2022}
% {Oregon Programming Language Summer School (OPLSS)}{}
% {University of Oregon}{Eugene, OR}
% {
% This year, the school focused on types, semantics, and program reasoning;
% I have attended courses involving proof theory,
% type theory, algebraic effect system, program verification in Coq etc.}


% \cventry{2021}
% {Oregon Programming Language Summer School (OPLSS)}{}
% {University of Oregon}{Eugene, OR}
% {This year, this summer school focused on foundation of programming and security;
% I have attended courses involving verification of probabilistic programs,
% session type for concurrent programming, 
% and categorical semantics of advanced type systems, etc.}


\cventry{2014 --- 2018}
{Mathematics, B.A.} {with department honor, magna cum laude}
{Wheaton College}
{Norton, MA, USA}
{\textbf{Honor Thesis}: \href{http://hdl.handle.net/11040/24570}{King in Generalized Tournaments}.\\
\textbf{Minors}: Computer Science, Economics.
}

\cventry{2016 --- 2017}
{Economics, Study Aboard} {}
{London School Of Economics}
{London, UK}
{}  % description

\section{Employment}

\cventry{2024 -- Now}
{PostDoc Research Fellow}
{University College London (UCL)}
{London, UK}{}
{Supervised by Alexandra Silva.}

\cventry{2021 --- 2024}
{Graduate Researcher}
{Boston University}
{Boston, MA, USA}{}
{
Supervised by Marco Gaboardi; worked with Arthur de Amorim (now professor at RIT)
% Study various extensions of Kleene Algebra, and their use in program analysis
% of imperative/functional programs, probabilistic programs, distributed systems, networks, etc.
% My researches provide easier, even automated, proofs for program analysis.
}

\cventry{2019 --- 2020}
{Teaching Fellow}
{Boston University}
{Boston, MA, USA}{}
{%
  % Taught Principle of Programming Language, Introduction to Computer Science,
  % Algebra Algorithm, Geometric Algorithm, etc.
}

\section{Publications And Drafts}

\cventry{2025}
{Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz, Marco Gaboardi}
{\href{https://github.com/qcfu-bu/rust-gkat}{Efficient Symbolic Algorithms For GKAT equivalence}}
{Draft}
{}{}

\cventry{2025}
{Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi}
{Domain Reasoning In TopKAT: Reduction and Completeness}
{Theory and Practice of Static Analysis (TPSA)}
{}{}

\cventry{2025}
{Cheng Zhang, Tobias Kappé, David E. Narváez, Nico Naus}
{\href{https://arxiv.org/abs/2411.13220}{CF-GKAT: Control Flow Verification in Nearly Linear Time}}
{Principle Of Programming Language (POPL)}
{}{}

\cventry{2025}
{Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi}
{\href{https://hal.science/hal-04534715/}{Kleene algebra with commutativity conditions is undecidable}}
{Computer Science Logic (CSL)}
{}{}

\cventry{2024}
{Cheng Zhang}
{Two Variants of Kleene Algebra and Their Applications}
{Ph.D. Thesis}
{}{}

\cventry{2024}
{Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi}
{\href{https://arxiv.org/abs/2404.18417}{Domain Reasoning In TopKAT}}
{International Colloquium on Automata, Languages and Programming (ICALP)}
{}{}

\cventry{2023}
{Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi}
{\href{https://doi.org/10.1145/3609027.3609407}{A Dependently Typed Language with Dynamic Equality}}
{The workshop on Type-Driven Development (TyDe)}
{}{}

\cventry{2022}
{Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi}
{\href{https://arxiv.org/abs/2108.07707}{On Incorrectness Logic and Kleene Algebra With Top and Tests}}
{Principle Of Programming Language (POPL)}
{}{}

\cventry{2020}
{Mark Lemay, Cheng Zhang, William Blair}
{\href{https://icfp20.sigplan.org/details/tyde-2020-papers/7/Developing-a-Dependently-Typed-Language-with-Runtime-Proof-Search-Extended-Abstract-}
{Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)}}
{Workshop on Type-Driven Development (TyDe)}
{}{}

\cventry{2018}
{Cheng Zhang}
{\href{http://hdl.handle.net/11040/24570}{King in Generalized Tournaments}}
{Wheaton College Honor Thesis}
{}{}

\cventry{2018}
{Cheng Zhang, Weiqi Feng, Emma Steffens, Alvaro de Landaluce, Scott Kleinman, Mark D. LeBlanc}
{\href{https://dl.acm.org/doi/10.5555/3205191.3205205}{Lexos 2017: Building Reliable Software in Python}}
{Journal of Computing Sciences in Colleges}
{}{}


\section{Research Talks}

\cventry{2023}
{Cheng Zhang}
{GKAT with Indicator Variables, Fast Decompilation Verification}
{BU Principles of Programming and Verification (POPV) Seminar}
{}{}

\cventry{2023}
{Cheng Zhang}
{A Practical Tutorial to KAT and its Extensions}
{Systems Software Research Group at Virginia Tech}
{}{}

\cventry{2022}
{Cheng Zhang}
{Kleene Algebra and Its Applications in Verification}
{Boston Computation Club}
{}{}

\cventry{2022}
{Cheng Zhang}
{On Incorrectness Logic Kleene Algebra With Test}
{Cornell Programming Language Discussion Group (PLDG)}
{}{}

\cventry{2022}
{Cheng Zhang}
{On Incorrectness Logic Kleene Algebra With Test}
{Principle Of Programming Languages (POPL)}
{}{}

\cventry{2018}
{Cheng Zhang, Mark D. LeBlanc}
{Lexos 2017: Building Reliable Software in Python}
{Journal of Computing Sciences in Colleges}
{}{}

\cventry{2018}
{Cheng Zhang}
{Kings in Quasi-transitive Oriented Graph}
{Wheaton Summit For Woman In STEM}
{}{}

\section{Research Grant}

\cventry{2024}{SPARK: Scalable Program Analysis And Reasoning With Kleene Algebra}{MSCA Postdoctoral Fellowships (in submission)}{}{}{}


\section{Professional Services}

\cventry{2025}{Artifact Reviewer}
{Object-Oriented Programming, Systems, Languages \& Applications (OOPSLA)}{}{}{}

\cventry{2021 --- 2024}
{Organizer}
{Principle of Programming and Verification (POPV) Seminar}
{Boston University}{}
{%
% Invite seminar speakers and coordinate time of the talks;
% maintain seminar webpage, mailing list, and calendar;
% distribute details of the seminar to participants every week;
% and host speakers during the seminars.
}

\cventry{2024}{Artifact Reviewer}
{Principles of Programming languages (POPL)}{}{}{}

\cventry{2024}{Student Volunteer}
{Oregon Programming Language Summer School (OPLSS)}{}{}{}

\cventry{2023}
{Artifact Reviewer}
{European Symposium on Programming (ESOP)}{}{}{}

\cventry{2023}{Student Volunteer}{Logic in Computer Science (LICS)}
{}{}{}

\cventry{2022}{Student Volunteer}{Oregon Programming Language Summer School (OPLSS)}
{}{}{}

\cventry{2020 --- 2024}
{Organizer}
{Category Theory Reading Group}
{Boston University}{Boston, MA}
{%
% Identify and distribute weekly reading materials;
% host and schedule the weekly discussions.
}

\cventry{2020 --- 2022}
{Organizer}
{Rocq Proof Assistant Reading Group}
{Boston University}{Boston, MA}
{%
% Identify and distribute weekly reading materials;
% host and schedule the weekly discussions.
}

\section{Teaching Experience}

\cventry{2020}{Teaching Assistant}{CS 230: Principle of Programming Language}{Boston University}{}{}

\cventry{2020}{Teaching Assistant}{CS 111: Introduction to Computer Science 1}{Boston University}{}{}

\cventry{2020}{Teaching Assistant}{CS 112: Introduction to Computer Science 2}{Boston University}{}{}

\cventry{2020}{Teaching Assistant}{CS 235: Algebraic Algorithm}{Boston University}{}{}

\cventry{2019}{Teaching Assistant}{CS 132: Geometric Algorithm}{Boston University}{}{}

\cventry{2019}{Teaching Assistant}{CS 230: Principle of Programming Language}{Boston University}{}{}

\cventry{2019}
{Grader}
{CS 511 Formal Method}
{Boston University}{}
{%
% Provided solutions to homework problems, graded the homework,
% organize useful statistics for the professor, 
% and provided hints and answered questions piazza when necessary.
}

\cventry{2017 --- 2018}
{Grader}
{MATH 241 Theory of Probability}
{Wheaton College}{}
{%
% Graded homework, gave feedback to students on each individual homework,
% and provide informative statistics to the professor on the homework.
}

 
\section{Honors And Fellowships}
\cvitem{2022}{Meta Ph.D. Research Fellowship Finalist in Programminag Languages}
\cvitem{2018 --- Now} {Phi Beta Kappa Honor Society Member.}
\cvitem{2018}{Boston University Dean's Fellowship.}
\cvitem{2018}{Phi Beta Kappa Graduate Scholarship.}
\cvitem{2018} {Madeleine F. Clark Wallace Mathematics Prize.}
\cvitem{2018}{Fred Kollett Prize in Mathematics \& Computer Science.}
\cvitem{2017}{Weaton College Faculty-Student Research Awards.}
\cvitem{2016}{Wheaton Fellows.}
\cvitem{2014 --- 2018}{Wheaton College International Scholarship.}
\cvitem{2014 --- 2018}{Wheaton College Dean's Lists.}

% \section{Research Projects}

% \cventry{2024}
% {A Symbolic Decision Procedure For Guarded Kleene Algebra With Tests}
% {}{}{}
% {Guarded Kleene Algebra With Tests is an efficient framework for program verifications. In this work, we marry GKAT with symbolic automaton, further improving its efficiency.
% Unlike previous works with KAT, our algorithm was able to offload the solving of complex boolean logic to a fast external solver like z3.
% This work also gives the exact complexity bound of GKAT.}

% \cventry{2024}
% {Guarded Kleene Algebra With Tests And Control Flow Verification}
% {}{}{}
% {Correctness of compilation and decompilation remains a challenging step in producing fully verified software. 
% One of the difficulties is caused by the increasingly complex algorithm used for efficient control flow restructuring.
% In this work, we designed an algorithm to automatically verify the correctness control-flow restructuring. This algorithm is not only sound and complete with regard to trace equivalences, but also able to handle a wide range of control-flow structures like goto, break, return, and indicator variables. 
% Furthermore, we provide a preliminary implementation, and experiments. As part of our experiments, we were able to verify random programs with millions of command in seconds, while running on a laptop.}

% \cventry{2022 --- 2024}
% {Kleene Algebra With Commutative Hypothesis}
% {}{}{}
% {Researchers has long known the importance of commutative hypothesis in Kleene Algebra.
% However, with recent work, commutative hypothesis was put on the center stage as the foundation of relational verifications. 
% Unfortunately, the theory of KA with commutativity hypothesis is not as well-developed as its applications. 
% Specifically, the decidability of Kleene algebra with commutativity hypothesis has remained open for almost three decades.
% In this work, we took on this long-standing open problem, and proven that the Kleene Algebra with commutativity hypothesis is undecidable.
% In fact, we were able to obtain our undecidability result with only the left unfolding rule, and omitted induction rules. This means a large class of theories sitting between idempotent semiring with left unfolding, and the regular languages are all undecidable with commutativity hypothesis.}

% \cventry{2021 --- 2022}
% {Probabilistic Incorrectness Logic and Kleene Algebra}
% {}{}{}
% {Examine the mathematical foundation of probabilistic Incorrectness logic.
% This work may give rise to a method reason about correctness and incorrectness in probabilistic programs.}

% \cventry{2020 --- 2022}
% {Algebraic Formulation Of Incorrectness Logic}
% {}{}{}
% {Provide an algebraic formulation of Incorrectness Logic in TopKAT.
% Our work leads to simpler proofs for program incorrectness, 
% and demonstrates ways to automatically certify bugs in programs.
% We showed that TopKAT is a minimal framework to model incorrectness,
% as it is impossible to encode incorrectness logic in KAT.
% After that, we proved many meta-theoretical property of TopKAT,
% including incompleteness with relational model, 
% completeness of general relational model and language model, 
% complexity of deciding equality, and expressivity of general relational model.
% }

% \cventry{2017 --- 2018}
% {Mathematics Honor Thesis}
% {Wheaton College} {Norton, MA}{}
% {Studied kings in generalizations of tournament,
% with a special focus on quasi-transitive oriented graphs.
% I have shown that all the quasi-transitive oriented graphs
% can be condensed into a tournament via tie component condensation, 
% and tie component condensation of quasi-transitive 
% oriented graphs is the most efficient condensation to tournament.
% }

% \cventry{2015 --- 2018}
% {Software Lead}
% {Lexomics Research Group, Wheaton College}
% {Norton, MA}{}
% {
%   Led a group of undergraduate engineers through a major factorization of 
%   the natrual language processing (NLP) software 
%   \href{https://github.com/WheatonCS/Lexos}{Lexos}.
%   In the process, 
%   I have designed a new architecture for side-effect management,
%   transitioned the code base to a scalable functional-first paradigm,
%   implemented industry-standard software development workflows,
%   and provided detailed documentations and guides for the entire system.
% }



% \section{Technical Skills}

% \iftechnical
% \cvline{}{\textbf{Programming}: Haskell, ATS, Python, TypeScript.}
% \cvline{}{\textbf{Formal Methods}: Coq, MathComp, Z3.}
% \cvline{}{\textbf{Data Processing}: Panda, Scikit-Learn, Numpy, R.}
% \cvitem{}{\textbf{Tools}: Git, \LaTeX, SSH, Jupyter Notebook.}
% \else
% \cvline{}{\textbf{Programming Languages}: Haskell, Ocaml, ATS, TypeScript, C\#, Java, C++.}
% \cvline{}{\textbf{Scripting Languages}: Python, Powershell, JavaScript, Mathematica.}
% \cvline{}{\textbf{Formal Methods}: Coq, Lean, MathComp Z3, EasyCrypt, Agda.}
% \cvline{}{\textbf{Data Processing}: Panda, Scikit-Learn, Numpy, SQL, R, Stata.}
% \cvitem{}{\textbf{Tools}: Git, \LaTeX, SSH, Jupyter Notebook.}
% \fi


% \section{Selected Coursework}

% \cventry{2018 --- Now}
% {Computer Science, \iftechnical Doctor of Philosophy\else Ph.D.\fi} {}
% {Boston University} {} {}  % description
% \cvlistdoubleitem{Computer Network}{Cryptography}
% \cvlistdoubleitem{Formal Method}{Compilers}
% \cvlistdoubleitem{Overview On Type Systems}{Complexity Thoery}


% \cventry{2014 --- 2018}
% {Mathematics, \iftechnical Bachelor of Art\else B.A.\fi} {}
% {Wheaton College} {} {}
% \cvlistdoubleitem{Complex Analysis}{Real Analysis}
% \cvlistdoubleitem{Graph Thoery}{Theory Of Computation}
% \cvlistdoubleitem{Mathematical Statistics}{Advanced Cryptography}

% \cventry{2016 --- 2017}
% {Economics, Study Aboard} {}
% {London School Of Economics} {} {}  % description
% \cvlistdoubleitem{Game Thoery}{Economatrics}
% \cvlistdoubleitem{Abstract Algebra I}{Abstract Algebra II}


\end{document}