Commit | Line | Data |
---|---|---|
d3adcff4 | 1 | curriculum vitae |
7b376474 | 2 | |
d3adcff4 | 3 | Amin Bandali |
7b376474 | 4 | |
d3adcff4 AB |
5 | ------------------------------------------ |
6 | site: https://bndl.org | |
7 | email: bandali@gnu.org | |
8 | bandali@uwaterloo.ca | |
9 | phone: available upon request via email | |
7b376474 | 10 | |
d3adcff4 AB |
11 | this file: https://bndl.org/bandali-cv.txt |
12 | last update: 2021-08-31 | |
13 | ------------------------------------------ | |
7b376474 AB |
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 | ||
7909a222 | 220 | summer 2015 | Computer Programmer |
7b376474 AB |
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 | |
47fc2c71 AB |
254 | Persian (mother tongue), English (native proficiency; IELTS: 9.0), |
255 | French (beginner) | |
7b376474 AB |
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. |