| 1 | curriculum vitae |
| 2 | |
| 3 | Amin Bandali |
| 4 | |
| 5 | ------------------------------------------ |
| 6 | site: https://bndl.org |
| 7 | email: bandali@gnu.org |
| 8 | bandali@uwaterloo.ca |
| 9 | phone: available upon request via email |
| 10 | |
| 11 | this file: https://bndl.org/bandali-cv.txt |
| 12 | last update: 2021-08-31 |
| 13 | ------------------------------------------ |
| 14 | |
| 15 | |
| 16 | SUMMARY OF QUALIFICATIONS |
| 17 | |
| 18 | - Experience in building software for diverse areas and platforms |
| 19 | in various programming languages such as C, Python, and Haskell. |
| 20 | |
| 21 | - Passionate about applying scientific and engineering methods |
| 22 | while designing and building software systems. |
| 23 | |
| 24 | - Using formal specification techniques to find specification-level |
| 25 | bugs early in the design stage rather than implementation. |
| 26 | |
| 27 | - GNU/Linux system administration on both the client and the server |
| 28 | side. |
| 29 | |
| 30 | - Problem-solving and communication skills, honed through research |
| 31 | and teaching roles held in graduate school, as well as holding |
| 32 | tutorials discussing complex concepts with fellow students and |
| 33 | peers throughout undergraduate studies and high school. |
| 34 | |
| 35 | - Organizational and teamwork skills, strengthened thanks to |
| 36 | community service in form of volunteer activities including |
| 37 | organizing the EmacsConf conference and volunteer work for |
| 38 | charities such as the Free Software Foundation and St. Brigid's |
| 39 | Summer Camp. |
| 40 | |
| 41 | |
| 42 | EDUCATION |
| 43 | |
| 44 | Master of Mathematics in Computer Science, University of Waterloo, |
| 45 | 2020 |
| 46 | |
| 47 | Research focus: |
| 48 | formal logic, model checking, verification |
| 49 | Thesis: |
| 50 | A Comprehensive Study of Declarative Modelling Languages |
| 51 | Supervisor: |
| 52 | Prof. Nancy A. Day |
| 53 | GPA: |
| 54 | 3.7/4.0 |
| 55 | |
| 56 | Bachelor of Science with Honours in Computer Science, York |
| 57 | University, 2017 |
| 58 | |
| 59 | Favourite courses: |
| 60 | System Specification & Refinement, Software Requirements |
| 61 | Engineering, Software Design, Operating Systems, Computational |
| 62 | Complexity, Design & Analysis of Algorithms |
| 63 | GPA: |
| 64 | 7.84/9.0 |
| 65 | |
| 66 | |
| 67 | RESEARCH INTERESTS |
| 68 | |
| 69 | formal logic, model checking, theorem proving, verification |
| 70 | |
| 71 | |
| 72 | PUBLICATIONS & PRESENTATIONS |
| 73 | |
| 74 | The complete bibliography of my publications is available as |
| 75 | a BibTeX bibliography file from https://bndl.org/bandali.bib. |
| 76 | |
| 77 | PAPERS |
| 78 | |
| 79 | A Comparison of the Declarative Modelling Languages B, DASH, |
| 80 | and TLA+ |
| 81 | |
| 82 | Ali Abbassi, Amin Bandali, Nancy A. Day, Jose Serna |
| 83 | 8th IEEE International Model-Driven Requirements |
| 84 | Engineering Workshop, MoDRE@RE 2018 |
| 85 | Copyright (c) 2018 IEEE. All Rights Reserved. Sadly. |
| 86 | |
| 87 | pdf: https://p.bndl.org/modre2018-declarative.pdf |
| 88 | models: https://cs.uwaterloo.ca/~nday/artifacts/2018-modre/ |
| 89 | |
| 90 | THESES |
| 91 | |
| 92 | A Comprehensive Study of Declarative Modelling Languages |
| 93 | |
| 94 | Amin Bandali |
| 95 | MMath Thesis, University of Waterloo, David R. Cheriton |
| 96 | School of Computer Science, July 2020. |
| 97 | |
| 98 | pdf: https://p.bndl.org/bandali-mmath-thesis.pdf |
| 99 | hdl: https://hdl.handle.net/10012/16059 |
| 100 | http: https://bndl.org/mmath.html |
| 101 | |
| 102 | TALKS |
| 103 | |
| 104 | Jami and how it empowers users |
| 105 | |
| 106 | Amin Bandali |
| 107 | Presented at the LibrePlanet 2021 Conference, March 20, 2021. |
| 108 | |
| 109 | slides: https://p.bndl.org/bandali-jami-libreplanet-2021.pdf |
| 110 | slides with notes: |
| 111 | https://p.bndl.org/bandali-jami-libreplanet-2021-with-notes.pdf |
| 112 | http: https://bndl.org/libreplanet-2021.html |
| 113 | |
| 114 | The Magic of Specifications and Type Systems |
| 115 | |
| 116 | Amin Bandali, Simon Hudon, Jonathan S. Ostroff |
| 117 | Slides presented at the Canadian Undergraduate Computer Science |
| 118 | Conference 2017, University of Toronto, Canada, June 15-17, |
| 119 | 2017. |
| 120 | Poster presented at the Lassonde Undergraduate Summer Student |
| 121 | Research Conference, York University, Toronto, Canada, |
| 122 | August 15, 2017. |
| 123 | |
| 124 | slides: https://p.bndl.org/cucsc-2017-slides.pdf |
| 125 | poster: https://p.bndl.org/eecs4080-poster.pdf |
| 126 | |
| 127 | Introducing YULUG |
| 128 | |
| 129 | Amin Bandali |
| 130 | Slides introducing YULUG -- (GNU/)Linux User Group at York |
| 131 | University -- presented at a Computing Students Hub (CSHub) tech |
| 132 | talk at York University, Toronto, Canada, February 12, 2015. |
| 133 | |
| 134 | |
| 135 | WORK & RESEARCH EXPERIENCE |
| 136 | |
| 137 | Savoir-faire Linux |
| 138 | |
| 139 | fall 2020-present | Free Software Consultant |
| 140 | | Consultant en logiciel libre |
| 141 | |
| 142 | I am part of the Jami core development team at Savoir-faire |
| 143 | Linux, where I get to work on various parts of Jami as a Free |
| 144 | Software Consultant. These include working on and maintaining |
| 145 | the GTK+-based jami-gnome client application written in C++ and |
| 146 | C, and packaging Jami for various GNU/Linux distributions and |
| 147 | other platforms. I also serve as a community liaison between |
| 148 | the Jami core team and the wider free software community around |
| 149 | Jami, with the goal of helping facilitate the communications and |
| 150 | relations between the two. |
| 151 | |
| 152 | Free Software Foundation (FSF) |
| 153 | |
| 154 | spring 2020 | Intern |
| 155 | |
| 156 | Working with the FSF tech team in a sysadmin role on a variety |
| 157 | of tasks including installation of the Sourcehut free software |
| 158 | forge on the FSF infrastructure for evaluation for the FSF forge |
| 159 | project, as well as a series of enhancements for www.gnu.org. |
| 160 | |
| 161 | Cheriton School of Science, University of Waterloo |
| 162 | |
| 163 | winter 2018-spring 2020 | TA, IA, RA [*] |
| 164 | |
| 165 | SE 465 (Software Testing and Quality Assurance): |
| 166 | TA in winter 2020 |
| 167 | SE 212 (Logic and Computation): |
| 168 | IA in Fall 2019, TA in fall 2018 |
| 169 | SE 463 (Software Requirement Specification and Analysis): |
| 170 | TA in spring 2019 and 2018 |
| 171 | CS 136 (Elementary Algorithm Design and Data Abstraction): |
| 172 | TA in winter 2018 |
| 173 | |
| 174 | [*]: Teaching Assistant (marking exams and assignments), |
| 175 | Instructional Apprentice (holding tutorials and marking), |
| 176 | Research Assistant (doing research for/with supervisor) |
| 177 | |
| 178 | Department of Electrical Engineering & Computer Science, York |
| 179 | University |
| 180 | |
| 181 | fall 2017 | Teaching Assistant |
| 182 | |
| 183 | EECS 1012 (Net-Centric Introduction to Computing): |
| 184 | TA in fall 2017, running labs and marking labs and exams |
| 185 | |
| 186 | Software Engineering Lab, York University |
| 187 | |
| 188 | summer 2017 | Research Assistant |
| 189 | |
| 190 | Worked on an implementation of Lampsort in Eiffel. |
| 191 | Extended the mathmodels library, implementing a rational |
| 192 | class for working with arbitrarily large rational numbers. |
| 193 | |
| 194 | summer 2016 | Research Student |
| 195 | |
| 196 | Worked on Literate Unit-B, the verifier for Unit-B, a new formal |
| 197 | method focused on formal verification of reactive, concurrent |
| 198 | and distributed systems. From the Literate Unit-B codebase |
| 199 | (written in Haskell), decoupled the logic module and used it to |
| 200 | build Unit-B Web, a web interface using Literate Unit-B to do |
| 201 | predicate calculus proofs. Unit-B Web, also written in Haskell, |
| 202 | supports the LaTeX syntax of the Unit-B logic, renders user |
| 203 | input on the page, and calls the sequent prover of the logic |
| 204 | module, which uses the Z3 SMT solver to check the validity of |
| 205 | user input. |
| 206 | |
| 207 | Separated Literate Unit-B's type checker from its parser in a |
| 208 | large refactoring, allowing easier substitution of other type |
| 209 | checking algorithms, and in preparation for implementing |
| 210 | subtyping. |
| 211 | |
| 212 | Lotek Wireless Inc. |
| 213 | |
| 214 | summer 2016 | Software Developer |
| 215 | |
| 216 | Designed and developed an Employee Portal web application in C# |
| 217 | and the MVC framework, used by employees for accessing various |
| 218 | data catalogs and archives. |
| 219 | |
| 220 | summer 2015 | Computer Programmer |
| 221 | |
| 222 | Designed and implemented various applications in C# and C for |
| 223 | analyzing and testing a satellite pass prediction algorithm for |
| 224 | predicting the pass windows of Argos satellites, for scheduling |
| 225 | send times of data collected by the company's wildlife tracking |
| 226 | products. |
| 227 | |
| 228 | Athlete Builder |
| 229 | |
| 230 | 2013-2014 | Software Developer |
| 231 | |
| 232 | Developed the Backend of Athlete Builder platform in C# and MVC. |
| 233 | |
| 234 | Key role in development of the platform core. |
| 235 | |
| 236 | Developed the alpha version of Athlete Builder Android |
| 237 | application in Java. |
| 238 | |
| 239 | |
| 240 | SKILLS |
| 241 | |
| 242 | Programming languages |
| 243 | C, C++, Haskell, Emacs Lisp, Guile Scheme, Python, Eiffel, Bash, |
| 244 | C#, Java, JavaScript |
| 245 | |
| 246 | Tools |
| 247 | GNU Emacs, Git, Alloy, TLA+, ProB, LaTeX, continuous integration |
| 248 | systems |
| 249 | |
| 250 | Platforms |
| 251 | GNU/Linux distributions, including Trisquel, GNU Guix, Debian |
| 252 | |
| 253 | Languages |
| 254 | Persian (mother tongue), English (native proficiency; IELTS: 9.0), |
| 255 | French (beginner) |
| 256 | |
| 257 | |
| 258 | COMMUNITY SERVICE |
| 259 | |
| 260 | EmacsConf conference |
| 261 | |
| 262 | 2019-present |
| 263 | |
| 264 | Chief organizer and maintainer of conference infrastructure, |
| 265 | including the streaming servers. |
| 266 | |
| 267 | 2015 |
| 268 | |
| 269 | One of the organizers and in charge of setting up |
| 270 | and maintaining vital pieces of infrastructure. |
| 271 | |
| 272 | Computer Science Club (CSC) of the University of Waterloo |
| 273 | |
| 274 | Served as the CSC System Administrator in Winter and Spring 2020. |
| 275 | Present member of the CSC Systems Committee, overseeing and |
| 276 | maintaining a large fleet of GNU/Linux servers for CSC members, |
| 277 | as well as running the CSC mirror for free software projects. |
| 278 | |
| 279 | Notable projects include launching the CSC web IRC client |
| 280 | as part of an effort in bringing modern user freedom- and |
| 281 | privacy-respecting communication tools to club members. |
| 282 | |
| 283 | Free/libre software contributions |
| 284 | |
| 285 | Co-maintainer of GNUzilla and IceCat, the GNU version of |
| 286 | the Mozilla suite and the Firefox browser respectively. |
| 287 | |
| 288 | Maintainer of ERC, the powerful, modular, and extensible |
| 289 | IRC client distributed with GNU Emacs. |
| 290 | |
| 291 | Committer and regular contributor to GNU Emacs and GNU Guix. |
| 292 | |
| 293 | GNU webmaster and GNU Savannah hacker. |
| 294 | |
| 295 | Volunteer work |
| 296 | |
| 297 | spring 2013 | Application Developer for VONICAL Inc. |
| 298 | |
| 299 | Worked on development of the Employment Accessibility Resource |
| 300 | Network (EARN) portal using the Anahita social networking |
| 301 | platform, written in PHP and running on GNU/Linux. |
| 302 | |
| 303 | winter 2013 | Mobile & Web Developer for Hire Works Inc. |
| 304 | |
| 305 | Worked on a variety of web and mobile development projects for |
| 306 | Hire Works. |
| 307 | |
| 308 | summer 2012 | Web Developer for St. Brigid's Summer Camp |
| 309 | |
| 310 | Redesigned and revamped the codebase for the photo gallery |
| 311 | section of the camp's website in PHP and JavaScript. |