2 %% Copyright 2016-2019 Amin Bandali <bandali@gnu.org>
4 % This work may be distributed and/or modified under the
5 % conditions of the LaTeX Project Public License, either version 1.3
6 % of this license or (at your option) any later version.
7 % The latest version of this license is in
8 % http://www.latex-project.org/lppl.txt
9 % and version 1.3 or later is part of all distributions of LaTeX
10 % version 2005/12/01 or later.
12 % Based on Jason R. Blevins's Curriculum Vitae template,
13 % Copyright (C) 2004-2016 Jason R. Blevins <jrblevin@sdf.org>
14 % http://jblevins.org/
16 \documentclass[12pt,letterpaper
]{article
}
23 % To enable correct spacing
30 \setmainfont[Scale=
0.95,SmallCapsFont=
{Equity Caps A
},RawFeature=+c2sc
]{Equity Text A
}
31 \setsansfont[SmallCapsFont=
{Concourse C4
}]{Concourse T4
}
32 \setmonofont[Scale=
0.9]{Triplicate T4c
}
33 \newfontfamily{\tallnums}[RawFeature=
{+ss02
}]{Equity Text A
}
34 \newfontfamily{\largersans}[Scale=
1.05,SmallCapsFont=
{Concourse C4
}]{Concourse T4
}
35 \newcommand{\amper}{{\fontspec[Scale=
.9]{Equity Text A
}\selectfont\itshape\&
}}
37 \newcommand{\tla}{TLA$
{}^+$
}
39 \def\name{Amin Bandali
}
41 % The following metadata will show up in the PDF properties
46 pdfkeywords =
{Formal Methods, Formal Logic, Model Checking,
47 Verification, Type Systems, Proof Systems, Interactive Provers,
48 Programming Languages, Functional Programming, Haskell, Rust
},
49 pdftitle =
{\name: Curriculum Vitae
},
50 pdfsubject =
{Curriculum Vitae
},
61 \fancyhf{}% to clear existing header/footer
62 \renewcommand\headrulewidth{0pt
}
63 \cfoot{\vspace*
{-
.25em
}\textsc{Bandali CV --- page
\thepage \xspace of
66 % Custom section fonts
68 \sectionfont{\rmfamily\mdseries\Large}
69 \subsectionfont{\rmfamily\mdseries\itshape\large}
71 % Other possible font commands include:
72 % \ttfamily for teletype,
73 % \sffamily for sans serif,
75 % \scshape for small caps,
76 % \normalsize, \large, \Large, \LARGE sizes.
78 % Don't indent paragraphs.
79 \setlength\parindent{0em
}
81 % Make lists without bullets and compact spacing
82 \renewenvironment{itemize
}{
84 \setlength{\leftmargin}{1.5em
}
85 \setlength{\itemsep}{0.25em
}
86 \setlength{\parskip}{0pt
}
87 \setlength{\parsep}{0.25em
}
92 \setlist[enumerate
]{itemsep=
0.25em
}
101 % Alternatively, print name centered and bold:
102 %\centerline{\huge \bf \name}
106 \begin{minipage
}[t
]{0.495\textwidth}
107 site:
\href{https://bandali.eu.org
}{https://bandali.eu.org
} \\
108 email:
\href{mailto:abandali@uwaterloo.ca
}{abandali@uwaterloo.ca
} \\
109 phone: available upon request
117 \setlength\itemsep{.75em
}
119 \item {\large Master of Mathematics (Computer Science)
}\, |\,
{\small 2018--present
}
121 \textit{University of Waterloo
}, Canada
124 \item Supervised by Dr. Nancy Day | GPA:
3.7/
4.0 | Expected
125 completion: December
2019
126 \item Research focusing on formal logic, model checking, and verification.
129 \item {\large B.Sc. Honours Computer Science
}\, |\,
{\small 2013--
2017}
131 \textit{York University
}, Toronto, Canada
135 \item Relevant courses: System Specification
\amper\
136 Refinement, Software Requirements Eng., Software Design, Operating
137 Systems, Computational Complexity, Design
\amper\ Analysis of Algorithms.
138 \item Finished first year (
2013-
14) at
\textit{Carleton University
} with a GPA
139 of
11.0/
12.0, then transferred to
\textit{York University
} in Fall
2014.
144 \section*
{Publications
}
147 \item {\large \tallnums MoDRE
2018}
150 \item {\largersans A Comparison of the Declarative Modelling
151 Languages B, Dash, and
\tla}
152 \textsf{\footnotesize
153 (
\href{https://bandali.eu.org/papers/
2018-AbBaDaSe-modre.pdf
}{pdf
},
154 \href{https://bandali.eu.org/papers/
2018-AbBaDaSe-modre.bib
}{bib
})
}
156 Ali Abbassi, Amin Bandali, Nancy A. Day, and Jose Serna\\
157 \textit{2018 IEEE
8th International Model-Driven Requirements
158 Engineering Workshop (MoDRE)
}
163 \section*
{Work
\amper\ Research Experience
}
167 \item {\large Cheriton School of Computer Science,
} University of Waterloo\, |\,
{\small 2018--present
}
169 \textit{Teaching Assistant
}
172 \item I was a TA for
\textsf{\small SE
212}, Logic and
173 Computation, taught by Dr. Day in Fall
2018.
174 \item I was a TA for
\textsf{\small SE
463}, Software Requirements
175 Specification and Analysis, taught by Prof. Atlee.
176 \item I was a TA for
\textsf{\small CS
136}, Elementary Algorithm
177 Design and Data Abstraction.
180 \item {\large EECS Department,
} York University\, |\,
{\small fall
2017}
182 \textit{Teaching Assistant
}
185 \item I was a TA for
\textsf{\small EECS
1012}, Net-Centric
186 Introduction to Computing, taught by Dr. Brown.
189 \item {\large Software Engineering Lab,
} York University\, |\,
{\small summer
192 \textit{Research Assistant
}
195 \item I worked on an implementation of
196 \href{https://bertrandmeyer.com/
2014/
12/
07/lampsort/
}{\textit{Lampsort
}} in
197 Eiffel. I also extended the
198 \href{https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/
}{\texttt{mathmodels
}}
199 library, implementing a
\textsc{RATIONAL
} class for working with arbitrarily
200 large rational numbers.
203 \item {\large Software Engineering Lab,
} York University\, |\,
{\small summer
206 \textit{Research Student
}
209 \item As an undergraduate research student, I worked on
\textit{Literate
210 Unit-B
}, the verifier for Unit-B, a new formal method focused on formal
211 verification of reactive, concurrent and distributed systems.
213 From the Literate Unit-B codebase (written in Haskell), I decoupled the
214 logic module and used it to build
\textit{Unit-B Web
}, a web interface using
215 Literate Unit-B to do predicate calculus proofs.
\linebreak Unit-B Web, also
216 written in Haskell, supports the
\LaTeX\ syntax of the Unit-B logic, renders
217 user input on the page, and calls the sequent prover of the logic module,
218 which uses the
\textsc{z3 smt
} solver to check the validity of user input.
220 \item Further, I separated Literate Unit-B's type checker from its parser,
221 allowing easier substitution of other type checking algorithms and in
222 preparation for implementing subtyping.
226 \section*
{Conference Presentations
}
229 \item {\large \tallnums CUCSC
2017}
232 \item {\largersans The Magic of Specifications and Type Systems
}
233 (
\href{https://bandali.eu.org/presentations/cucsc-
2017-slides.pdf
}{slides
}),
234 at Canadian Undergraduate Computer Science Conference, University of
235 Toronto, Canada, Jun
15--
17 2017.
238 \item {\large \tallnums Lassonde USSR Conference
2017}
241 \item {\largersans The Magic of Specifications and Type Systems
}
242 (
\href{https://bandali.eu.org/presentations/eecs4080-poster.pdf
}{poster
}),
243 at Lassonde Undergraduate Summer Student Research Conference, York University,
244 Toronto, Canada, August
15,
2017.
249 \section*
{Professional Experience
}
251 \item {\large Lotek Wireless Inc.,
} Newmarket, Canada\, |\,
{\small
252 summer
2015 \amper\
2016}
254 \textit{Software Developer
}
257 \item Designed and implemented various applications in C\# and C to test and
258 analyze a satellite pass prediction algorithm for predicting the pass
259 windows of Argos satellites, for scheduling send times of data collected by
260 company's wildlife tracking products.
262 \item Designed and developed an Employee Portal web application in C\# and the
263 MVC framework, used by employees for accessing various data catalogs and
268 \pagebreak % TODO: remove if necessary
270 \item {\large Athlete Builder,
} Ottawa, Canada\, |\,
{\small 2013--
2014}
272 \textit{Software Developer
}
275 \item Developed the Backend of Athlete Builder platform in C\# and MVC.
276 \item Was a key role in development of the platform core.
277 \item Developed the alpha version of Athlete Builder Android app in Java.
281 \section*
{Volunteer Activities
}
285 \item {\large EmacsConf
2015,
} \href{http://emacsconf.org
}{emacsconf.org
}\, |\,
291 \item EmacsConf is a conference about the joy of Emacs and writing Emacs
292 Lisp. I was a key organizer and in charge of setting up and maintaining
293 several vital pieces of the EmacsConf infrastructure.
297 \item {\large VONICAL Inc.,
} Ottawa, Canada\, |\,
{\small spring
2013}
299 \textit{Application Developer
}
302 \item As a volunteer, worked on development of EARN (Employment Accessibility
303 Resource Network) portal using the Anahita social networking platform, in
308 \item {\large Hire Works Inc.,
} Ottawa, Canada\, |\,
{\small winter
2013}
310 \textit{Mobile \& Web Developer
}
313 \item As a volunteer, I worked on a variety of web and mobile projects for
318 \item {\large St. Brigid's Summer Camp,
} Ottawa, Canada\, |\,
{\small summer
321 \textit{Web Developer
}
324 \item As a volunteer, I re-designed and coded (from scratch) an updated and
325 revamped version of the photo gallery section of St. Brigid Summer Camp's
326 website in PHP and JavaScript. A refactored version of my code is deployed
334 \section*
{Recent Projects
}
337 \item \textit{Unit-B Web:
} The web interface for Unit-B, as mentioned in the
338 \textit{Research Experience
} section.\\
339 Source code available at
340 \href{https://github.com/unitb/unitb-web
}{https://github.com/unitb/unitb-web
}
342 \item \textit{tex2png-hs:
} A tool for easily converting
\TeX\ and
\LaTeX\ to
343 \textsc{PNG
} images.
\texttt{tex2png-hs
} is a Haskell port of Xyne's
344 \texttt{tex2png
} tool. It is a wrapper around
\texttt{latex
} and
345 \texttt{dvipng
} and provides several options for modifying its behaviour, such
346 as cropping the whitespace around the content, specifying the
\textsc{DPI
}, or
347 inputting a full
document.
348 Source code available at
349 \href{https://github.com/unitb/tex2png-hs
}{https://github.com/unitb/tex2png-hs
}
351 \item For more projects, visit my personal site at
352 \href{https://bandali.eu.org
}{https://bandali.eu.org
}.
355 \section*
{Miscellaneous
}
358 \item \textit{Programming Languages:
} Haskell, Rust, Eiffel, Python, C, Emacs
359 Lisp, C\#, JavaScript.
360 \item \textit{Tools:
} Emacs, Liquid Haskell, Git, Zsh,
\LaTeX, CI Systems
361 (e.g. Travis CI), Rodin.
362 \item \textit{Platforms:
} Arch Linux, Ubuntu and other distros, Android, macOS,
364 \item \textit{Languages:
} Persian (mother tongue), English (fluent), French
369 % \section*{Achievements}
372 % \item Was among the top 1\% incoming students in Carleton University's
373 % undergraduate Computer Science program, and a top student in the faculty of
375 % \item Highest standing in Computer Science in grade 11 (92\%) and grade 12
376 % (100\%) at High school at Glebe~Collegiate~Institute.
377 % \item Ranked in the top 25\% in the Canadian Senior Mathematics Contest held by
378 % University of Waterloo, in 2013 (grade 11).
379 % \item Graduated from high school with an average of 95\%; and designated as an Ontario Scholar.
385 {\small Last updated:
\today}