| 1 | <!doctype html><html lang="en"><head> |
| 2 | <meta charset="utf-8" /> |
| 3 | <meta name="author" content="bandali" /> |
| 4 | <meta name="viewport" content="width=device-width, initial-scale=1" /> |
| 5 | <title>curriculum vitae — bandali</title> |
| 6 | <link rel="icon" href="data:,"> |
| 7 | <link rel="canonical" href="https://bndl.org/cv" /> |
| 8 | <link rel="alternate" href="bandali-cv.txt" title="plain text" type="text/plain" /> |
| 9 | <style> |
| 10 | body{line-height:1.6;padding:0 2em;}p,ul,dt,dd{max-width:37.5em} |
| 11 | .box{background:#f8f8f8;border:1px solid #e6e6e6;border-radius:4px; |
| 12 | font-size:0.95em;padding:0.6em 0.9em;} |
| 13 | #link-grid{display:grid;grid:none / auto 1fr;gap:0.2em 1em;} |
| 14 | #link-grid dd{margin-left:0} |
| 15 | .tex{font-family:"Tex Gyre Termes",serif;text-transform:uppercase;} |
| 16 | .tex span{font-size:0.75em;margin-left:-0.05em;margin-right:-0.20em;} |
| 17 | .tex sub{font-size:1em;margin-left:-0.1667em;margin-right:-0.125em; |
| 18 | vertical-align:-0.5ex;}.tex sup{font-size:0.85em;margin-left:-0.36em; |
| 19 | margin-right:-0.15em;vertical-align:0.15em;} |
| 20 | #copy,#license{font-size:0.84em;line-height:1.3;} |
| 21 | #copy{margin-bottom:0.5em}#license{margin-top:0.5em} |
| 22 | @media(prefers-color-scheme:dark){body{background:#1c1c1c;color:white;} |
| 23 | a:link{color:#acdeff}a:visited{color:#f8f}a:active{color:#e00} |
| 24 | .box{background:#1b1d1e;border-color:#373c34;}} |
| 25 | </style></head> |
| 26 | <body> |
| 27 | <h1><a href=".">bandali</a>'s curriculum vitae</h1> |
| 28 | |
| 29 | <p class="box">also available in plain text |
| 30 | as <a href="bandali-cv.txt">bandali-cv.txt</a></p> |
| 31 | |
| 32 | <dl id="link-grid"> |
| 33 | <dt>Site</dt> |
| 34 | <dd><a href="https://kelar.org/~bandali/">kelar.org/~bandali</a></dd> |
| 35 | <dt>Email</dt> |
| 36 | <dd>bandali@kelar.org<br />bandali@gnu.org<br />bandali@uwaterloo.ca</dd> |
| 37 | <dt>Phone</dt> |
| 38 | <dd>available upon request via email</dd> |
| 39 | <dt>Last update</dt> |
| 40 | <dd>November 1, 2021</dd> |
| 41 | </dl> |
| 42 | |
| 43 | <h2>Summary of Qualifications</h2> |
| 44 | |
| 45 | <ul> |
| 46 | <li>Experience in building software for diverse areas and platforms in |
| 47 | various programming languages such as C, Python, and Haskell.</li> |
| 48 | <li>Passionate about applying scientific and engineering methods while |
| 49 | designing and building software systems.</li> |
| 50 | <li>Using formal specification techniques to find specification-level |
| 51 | bugs early in the design stage rather than implementation.</li> |
| 52 | <li>GNU/Linux system administration on both the client and the server |
| 53 | side.</li> |
| 54 | <li>Problem-solving and communication skills, honed through research |
| 55 | and teaching roles held in graduate school, as well as holding |
| 56 | tutorials discussing complex concepts with fellow students and peers |
| 57 | throughout undergraduate studies and high school.</li> |
| 58 | <li>Organizational and teamwork skills, strengthened thanks to |
| 59 | community service in form of volunteer activities including organizing |
| 60 | the EmacsConf conference and volunteer work for charities such as the |
| 61 | Free Software Foundation and St. Brigid's Summer Camp.</li> |
| 62 | </ul> |
| 63 | |
| 64 | <h2>Education</h2> |
| 65 | |
| 66 | <dl> |
| 67 | <dt>Master of Mathematics in Computer Science, University of Waterloo, |
| 68 | 2020</dt> |
| 69 | <dd>Research focus: formal logic, model checking, verification</dd> |
| 70 | <dd>Thesis: <a href="#mmath">A Comprehensive Study of Declarative |
| 71 | Modelling Languages</a></dd> |
| 72 | <dd>Supervisor: <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy |
| 73 | A. Day</a></dd> |
| 74 | <dd>GPA: 3.7/4.0</dd> |
| 75 | |
| 76 | <dt>Bachelor of Science with Honours in Computer Science, |
| 77 | York University, 2017</dt> |
| 78 | <dd>Favourite courses: System Specification & Refinement, |
| 79 | Software Requirements Engineering, Software Design, Operating Systems, |
| 80 | Computational Complexity, Design & Analysis |
| 81 | of Algorithms</dd> |
| 82 | <dd>GPA: 7.84/9.0</dd> |
| 83 | </dl> |
| 84 | |
| 85 | <h2 id="research">Research Interests</h2> |
| 86 | |
| 87 | <p>formal logic, model checking, theorem proving, verification</p> |
| 88 | |
| 89 | <h2>Publications & Presentations</h2> |
| 90 | |
| 91 | <p>The complete bibliography of my publications is available as a |
| 92 | <span class="tex">B<span>ib</span>T<sub>e</sub>X</span> bibliography |
| 93 | file, <a href="bandali.bib">bandali.bib</a>.</p> |
| 94 | |
| 95 | <h3>Papers</h3> |
| 96 | |
| 97 | <dl> |
| 98 | <dt>A Comparison of the Declarative Modelling Languages B, DASH, and |
| 99 | TLA<sup>+</sup> |
| 100 | <small> |
| 101 | [ <a href="https://p.bndl.org/modre2018-declarative.pdf">pdf</a> |
| 102 | | <a href="https://cs.uwaterloo.ca/~nday/artifacts/2018-modre/">models</a> |
| 103 | ] |
| 104 | </small> |
| 105 | </dt> |
| 106 | <dd> |
| 107 | Ali Abbassi, <a href="https://bndl.org">Amin Bandali</a>, |
| 108 | <a href="https://cs.uwaterloo.ca/~nday/">Nancy A. Day</a>, Jose Serna<br /> |
| 109 | <em>8th IEEE International Model-Driven Requirements Engineering Workshop, MoDRE@RE 2018</em><br /> |
| 110 | Copyright © 2018 IEEE. All Rights Reserved. Sadly. |
| 111 | </dd> |
| 112 | </dl> |
| 113 | |
| 114 | <h3>Theses</h3> |
| 115 | |
| 116 | <dl> |
| 117 | <dt id="mmath">A Comprehensive Study of Declarative Modelling |
| 118 | Languages |
| 119 | <small> |
| 120 | [ <a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a> |
| 121 | | <a href="https://hdl.handle.net/10012/16059">hdl</a> |
| 122 | | <a href="https://bndl.org/mmath">http</a> |
| 123 | ] |
| 124 | </small> |
| 125 | </dt> |
| 126 | <dd> |
| 127 | <a href="https://bndl.org">Amin Bandali</a><br /> |
| 128 | <em><abbr title="Master of Mathematics">MMath</abbr> Thesis, |
| 129 | University of Waterloo, David R. Cheriton School of Computer Science, |
| 130 | July 2020.</em> |
| 131 | </dd> |
| 132 | </dl> |
| 133 | |
| 134 | <h3>Talks</h3> |
| 135 | |
| 136 | <dl> |
| 137 | <dt>Jami and how it empowers users |
| 138 | <small> |
| 139 | [ <a href="https://p.bndl.org/bandali-jami-libreplanet-2021.pdf">pdf</a> |
| 140 | (<a href="https://p.bndl.org/bandali-jami-libreplanet-2021-with-notes.pdf">with |
| 141 | notes</a>) |
| 142 | | <a href="https://bndl.org/2020/03/20/libreplanet-2021">http</a> |
| 143 | ] |
| 144 | </small> |
| 145 | </dt> |
| 146 | <dd> |
| 147 | <a href="https://bndl.org">Amin Bandali</a><br /> |
| 148 | <em>Presented at the LibrePlanet 2021 Conference, March 20, 2021.</em> |
| 149 | </dd> |
| 150 | |
| 151 | <dt>The Magic of Specifications and Type Systems |
| 152 | <small> |
| 153 | [ <a href="https://p.bndl.org/cucsc-2017-slides.pdf">slides</a> |
| 154 | | <a href="https://p.bndl.org/eecs4080-poster.pdf">poster</a> |
| 155 | ] |
| 156 | </small> |
| 157 | </dt> |
| 158 | <dd> |
| 159 | <a href="https://bndl.org">Amin Bandali</a>, |
| 160 | <a href="https://github.com/cipher1024">Simon Hudon</a>, |
| 161 | <a href="https://www.eecs.yorku.ca/~jonathan/">Jonathan S. Ostroff</a><br /> |
| 162 | <em>Slides presented at the Canadian Undergraduate Computer Science |
| 163 | Conference 2017, University of Toronto, Canada, June 15–17, 2017.<br /> |
| 164 | Poster presented at the Lassonde Undergraduate Summer Student Research |
| 165 | Conference, York University, Toronto, Canada, August 15, 2017.</em> |
| 166 | </dd> |
| 167 | |
| 168 | <dt>Introducing YULUG</dt> |
| 169 | <dd> |
| 170 | <a href="https://bndl.org">Amin Bandali</a><br /> |
| 171 | <em>Slides introducing YULUG — (GNU/)Linux User Group at York |
| 172 | University — presented at a Computing Students Hub (CSHub) tech |
| 173 | talk at York University, Toronto, Canada, February 12, 2015.</em> |
| 174 | </dd> |
| 175 | </dl> |
| 176 | |
| 177 | <h2>Work & Research Experience</h2> |
| 178 | |
| 179 | <dl> |
| 180 | <dt>Savoir-faire Linux</dt> |
| 181 | <dd>fall 2020–present | Free Software Consultant | Consultant en |
| 182 | logiciel libre</dd> |
| 183 | <dd> |
| 184 | <dl> |
| 185 | <dd>I am part of the Jami core development team at Savoir-faire Linux, |
| 186 | where I work on various parts of Jami as a Free Software Consultant. |
| 187 | These include working on and maintaining the GTK-based jami-gnome |
| 188 | client application written in C++ and C, and packaging Jami for |
| 189 | various GNU/Linux distributions and other platforms. I also serve as |
| 190 | a community liaison between the Jami core team and the wider free |
| 191 | software community around Jami, with the goal of helping facilitate |
| 192 | the communications and relations between the two.</dd> |
| 193 | </dl> |
| 194 | </dd> |
| 195 | |
| 196 | <dt>Free Software Foundation (FSF)</dt> |
| 197 | <dd>spring 2020 | Intern</dd> |
| 198 | <dd> |
| 199 | <dl> |
| 200 | <dd>Working with the FSF tech team in a sysadmin role on a variety of |
| 201 | tasks including installation of the Sourcehut free software forge on |
| 202 | the FSF infrastructure for evaluation for the FSF forge project, as |
| 203 | well as a series of enhancements |
| 204 | for <a href="https://www.gnu.org">www.gnu.org</a>.</dd> |
| 205 | </dl> |
| 206 | </dd> |
| 207 | |
| 208 | <dt>Cheriton School of Science, University of Waterloo</dt> |
| 209 | <dd>winter 2018–spring 2020 | TA, IA, RA <sup>[*]</sup></dd> |
| 210 | <dd> |
| 211 | <dl> |
| 212 | <dd>SE 465 (Software Testing and Quality Assurance): TA in winter |
| 213 | 2020</dd> |
| 214 | <dd>SE 212 (Logic and Computation): <a href="se212-f19">IA in |
| 215 | Fall 2019</a>, TA in fall 2018</dd> |
| 216 | <dd>SE 463 (Software Requirement Specification and Analysis): TA in |
| 217 | spring 2019 and 2018</dd> |
| 218 | <dd>CS 136 (Elementary Algorithm Design and Data Abstraction): TA in |
| 219 | winter 2018</dd> |
| 220 | </dl> |
| 221 | </dd> |
| 222 | <dd><small>[*] Teaching Assistant (marking exams and assignments), |
| 223 | Instructional Apprentice (holding tutorials and marking), Research |
| 224 | Assistant (doing research for/with supervisor)</small></dd> |
| 225 | |
| 226 | <dt>Department of Electrical Engineering & Computer Science, York |
| 227 | University</dt> |
| 228 | <dd>fall 2017 | Teaching Assistant</dd> |
| 229 | <dd> |
| 230 | <dl> |
| 231 | <dd>EECS 1012 (Net-Centric Introduction to Computing): TA in fall |
| 232 | 2017, running labs and marking labs and exams</dd> |
| 233 | </dl> |
| 234 | </dd> |
| 235 | |
| 236 | <dt>Software Engineering Lab, York University</dt> |
| 237 | <dd> |
| 238 | <dl> |
| 239 | <dt>summer 2017 | Research Assistant</dt> |
| 240 | <dd>Worked on an implementation |
| 241 | of <a href="https://bertrandmeyer.com/2014/12/07/lampsort/">Lampsort</a> |
| 242 | in Eiffel. Extended |
| 243 | the <a href="https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/">mathmodels</a> |
| 244 | library, implementing a <code>rational</code> class for working with |
| 245 | arbitrarily large rational numbers.</dd> |
| 246 | </dl> |
| 247 | </dd> |
| 248 | <dd> |
| 249 | <dl> |
| 250 | <dt>summer 2016 | Research Student</dt> |
| 251 | <dd>Worked on <em>Literate Unit-B</em>, the verifier for Unit-B, a new |
| 252 | formal method focused on formal verification of reactive, concurrent, |
| 253 | and distributed systems. From the Literate Unit-B codebase (written |
| 254 | in Haskell), decoupled the logic module and used it to build |
| 255 | <em>Unit-B Web</em>, a web interface using Literate Unit-B to do |
| 256 | predicate calculus proofs. Unit-B Web, also written in Haskell, |
| 257 | supports the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span> |
| 258 | syntax of the Unit-B logic, renders user input on the page, and calls |
| 259 | the sequent prover of the logic module, which uses the Z3 SMT solver |
| 260 | to check the validity of user input.</dd> |
| 261 | <dd>Separated Literate Unit-B's type checker from its parser in a |
| 262 | large refactoring, allowing easier substitution of other type checking |
| 263 | algorithms, and in preparation for implementing subtyping.</dd> |
| 264 | </dl> |
| 265 | </dd> |
| 266 | |
| 267 | <dt>Lotek Wireless Inc.</dt> |
| 268 | <dd> |
| 269 | <dl> |
| 270 | <dt>summer 2016 | Software Developer</dt> |
| 271 | <dd>Designed and developed an Employee Portal web application in C# |
| 272 | and the MVC framework, used by employees for accessing various data |
| 273 | catalogs and archives.</dd> |
| 274 | </dl> |
| 275 | </dd> |
| 276 | <dd> |
| 277 | <dl> |
| 278 | <dt>summer 2015 | Computer Programmer</dt> |
| 279 | <dd>Designed and implemented various applications in C# and C for |
| 280 | analyzing and testing a satellite pass prediction algorithm for |
| 281 | predicting the pass windows of Argos satellites, for scheduling send |
| 282 | times of data collected by the company's wildlife tracking |
| 283 | products.</dd> |
| 284 | </dl> |
| 285 | </dd> |
| 286 | |
| 287 | <dt>Athlete Builder</dt> |
| 288 | <dd> |
| 289 | <dl> |
| 290 | <dt>2013–2014 | Software Developer</dt> |
| 291 | <dd>Developed the Backend of Athlete Builder platform in C# and |
| 292 | MVC.</dd> |
| 293 | <dd>Key role in development of the platform core.</dd> |
| 294 | <dd>Developed the alpha version of Athlete Builder Android application |
| 295 | in Java.</dd> |
| 296 | </dl> |
| 297 | </dd> |
| 298 | </dl> |
| 299 | |
| 300 | <h2>Skills</h2> |
| 301 | <dl> |
| 302 | <dt>Programming languages</dt> |
| 303 | <dd>C, C++, Haskell, Emacs Lisp, Guile Scheme, Python, Eiffel, Bash, |
| 304 | C#, Java, JavaScript</dd> |
| 305 | <dt>Tools</dt> |
| 306 | <dd>GNU Emacs, Git, Alloy, TLA<sup>+</sup>, |
| 307 | ProB, <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span>, continuous |
| 308 | integration systems</dd> |
| 309 | <dt>Platforms</dt> |
| 310 | <dd>GNU/Linux distributions, including Trisquel, GNU Guix, Debian</dd> |
| 311 | <dt>Languages</dt> |
| 312 | <dd>Persian (mother tongue), English (native proficiency; IELTS: 9.0), |
| 313 | French (beginner)</dd> |
| 314 | </dl> |
| 315 | |
| 316 | <h2>Community Service</h2> |
| 317 | <dl> |
| 318 | <dt>EmacsConf conference</dt> |
| 319 | <dd> |
| 320 | <dl> |
| 321 | <dt>2019–present</dt> |
| 322 | <dd>Chief organizer and maintainer of conference infrastructure, |
| 323 | including the streaming servers.</dd> |
| 324 | <dt>2015</dt> |
| 325 | <dd>One of the organizers and in charge of setting up and maintaining |
| 326 | vital pieces of infrastructure.</dd> |
| 327 | </dl> |
| 328 | </dd> |
| 329 | <dt>Computer Science Club (CSC) of the University of Waterloo</dt> |
| 330 | <dd>Served as the CSC System Administrator in Winter and Spring 2020. |
| 331 | Present member of the CSC Systems Committee, overseeing and |
| 332 | maintaining a large fleet of GNU/Linux servers for CSC members, as |
| 333 | well as running the CSC mirror for free software projects.</dd> |
| 334 | <dd>Notable projects |
| 335 | include <a href="https://mailman.csclub.uwaterloo.ca/pipermail/csc-general/2020-July/000837.html">launching |
| 336 | the CSC web IRC client</a> as part of an effort in bringing modern |
| 337 | user freedom- and privacy-respecting communication tools to club |
| 338 | members.</dd> |
| 339 | <dt>Free/libre software contributions</dt> |
| 340 | <dd>Co-maintainer |
| 341 | of <a href="https://www.gnu.org/software/gnuzilla/gnuzilla.html">GNUzilla |
| 342 | and IceCat</a>, the GNU version of the Mozilla suite and the Firefox |
| 343 | browser respectively.</dd> |
| 344 | <dd>Maintainer |
| 345 | of <a href="https://www.gnu.org/software/emacs/erc.html">ERC</a>, the |
| 346 | powerful, modular, and extensible IRC client distributed with GNU |
| 347 | Emacs.</dd> |
| 348 | <dd>Committer and regular contributor |
| 349 | to <a href="https://www.gnu.org/software/emacs/emacs.html">GNU |
| 350 | Emacs</a> and <a href="https://guix.gnu.org">GNU Guix</a>.</dd> |
| 351 | <dd><a href="https://www.gnu.org/people/webmeisters.html#bandali">GNU |
| 352 | webmaster</a> |
| 353 | and <a href="https://savannah.gnu.org/maintenance/SavannahHacker/">GNU |
| 354 | Savannah hacker</a>.</dd> |
| 355 | <dt>Volunteer work</dt> |
| 356 | <dd> |
| 357 | <dl> |
| 358 | <dt>spring 2013 | Application Developer for VONICAL Inc.</dt> |
| 359 | <dd>Worked on development of the Employment Accessibility Resource |
| 360 | Network (EARN) portal using the Anahita social networking platform, |
| 361 | written in PHP and running on GNU/Linux.</dd> |
| 362 | <dt>winter 2013 | Mobile & Web Developer for Hire Works Inc.</dt> |
| 363 | <dd>Worked on a variety of web and mobile development projects for |
| 364 | Hire Works.</dd> |
| 365 | <dt>summer 2012 | Web Developer for St. Brigid's Summer Camp</dt> |
| 366 | <dd>Redesigned and revamped the codebase for the photo gallery section |
| 367 | of the camp's website in PHP and JavaScript.</dd> |
| 368 | </dl> |
| 369 | </dd> |
| 370 | </dl> |
| 371 | </body> |
| 372 | </html> |