+<head>
+<meta charset="utf-8" />
+<meta name="author" content="bandali" />
+<meta name="viewport" content="width=device-width, initial-scale=1" />
+<title>curriculum vitae — bandali</title>
+<link rel="canonical" href="https://bndl.org/cv.html" />
+<link rel="alternate" href="bandali-cv.txt" title="plain text" type="text/plain" />
+<link rel="alternate" href="https://p.bndl.org/bandali-cv.pdf" title="pdf" type="application/pdf" />
+<style>
+body {
+ line-height: 1.6;
+ max-width: 37.5em;
+ margin: 0 auto;
+ padding: 0 1em;
+}
+.tex {
+ font-family: "Tex Gyre Termes", serif;
+ text-transform: uppercase;
+}
+.tex span {
+ font-size: 0.75em;
+ margin-left: -0.05em;
+ margin-right: -0.20em;
+}
+.tex sub {
+ font-size: 1em;
+ margin-left: -0.1667em;
+ margin-right: -0.125em;
+ vertical-align: -0.5ex;
+}
+.tex sup {
+ font-size: 0.85em;
+ margin-left: -0.36em;
+ margin-right: -0.15em;
+ vertical-align: 0.15em;
+}
+.box {
+ background: #f8f8f8;
+ border: 1px solid #e6e6e6;
+ border-radius: 4px;
+ font-size: 0.95em;
+ padding: 0.6em 0.9em;
+}
+#link-grid {
+ display: grid;
+ grid: none / auto 1fr;
+ gap: 0.2em 1em;
+}
+#link-grid dd { margin-left: 0; }
+@media (prefers-color-scheme: dark) {
+ body { background: #1c1c1c; color: white; }
+ a:link { color: #acdeff; }
+ a:visited { color: #f8f; }
+ a:active { color: #e00; }
+ .box { background: #1b1d1e; border-color: #373c34; }
+}
+</style>
+</head>
+<body>
+<h1><a href=".">bandali</a>'s curriculum vitae</h1>
+
+<p class="box">also available in plain text
+as <a href="bandali-cv.txt">bandali-cv.txt</a></p>
+
+<dl id="link-grid">
+<dt>Site</dt>
+<dd><a href="https://bndl.org">bndl.org</a></dd>
+<dt>Email</dt>
+<dd>bandali@gnu.org</dd>
+<dt>Phone</dt>
+<dd>available upon request via email</dd>
+</dl>
+
+<h2>Summary of Qualifications</h2>
+
+<ul>
+<li>Experience in building software for diverse areas and platforms in
+various programming languages such as C, Python, and Haskell.</li>
+<li>Passionate about applying scientific and engineering methods while
+designing and building software systems.</li>
+<li>Using formal specification techniques to find specification-level
+bugs early in the design stage rather than implementation.</li>
+<li>GNU/Linux system administration on both the client and the server
+side.</li>
+<li>Problem-solving and communication skills, honed through research
+and teaching roles held in graduate school, as well as holding
+tutorials discussing complex concepts with fellow students and peers
+throughout undergraduate studies and high school.</li>
+<li>Organizational and teamwork skills, strengthened thanks to
+community service in form of volunteer activities including organizing
+the EmacsConf conference and volunteer work for charities such as the
+Free Software Foundation and St. Brigid's Summer Camp.</li>
+</ul>
+
+<h2>Education</h2>
+
+<dl>
+<dt>Master of Mathematics in Computer Science, University of Waterloo,
+2020</dt>
+<dd>Research focus: formal logic, model checking, verification</dd>
+<dd>Thesis: <a href="#mmath">A Comprehensive Study of Declarative
+Modelling Languages</a></dd>
+<dd>Supervisor: <a href="https://cs.uwaterloo.ca/~nday/">Prof. Nancy
+A. Day</a></dd>
+<dd>GPA: 3.7/4.0</dd>
+
+<dt>Bachelor of Science with Honours in Computer Science, York
+University, 2017</dt>
+<dd>Favourite courses: System Specification & Refinement, Software
+Requirements Engineering, Software Design, Operating Systems,
+Computational Complexity, Design & Analysis of Algorithms</dd>
+<dd>GPA: 7.84/9.0</dd>
+</dl>
+
+<h2 id="research">Research Interests</h2>
+
+formal logic, model checking, theorem proving, verification
+
+<h2 id="publications">Publications & Presentations</h2>
+
+<p>The complete bibliography of my publications is available as
+a <a href="bandali.bib">bandali.bib</a>
+<span class="tex">B<span>ib</span>T<sub>e</sub>X</span> bibliography
+file.</p>
+
+<h3>Papers</h3>
+
+<dl>
+<dt>A Comparison of the Declarative Modelling Languages B, DASH, and
+TLA<sup>+</sup>
+<small>
+[ <a href="https://p.bndl.org/modre2018-declarative.pdf">pdf</a>
+| <a href="https://cs.uwaterloo.ca/~nday/artifacts/2018-modre/">models</a>
+]
+</small>
+</dt>
+<dd>
+Ali Abbassi, <a href="https://bndl.org">Amin Bandali</a>,
+<a href="https://cs.uwaterloo.ca/~nday/">Nancy A. Day</a>, Jose Serna<br />
+<em>8th IEEE International Model-Driven Requirements Engineering Workshop, MoDRE@RE 2018</em><br />
+Copyright © 2018 IEEE. All Rights Reserved. Sadly.
+</dd>
+</dl>
+
+<h3>Theses</h3>
+
+<dl>
+<dt id="mmath">A Comprehensive Study of Declarative Modelling
+Languages
+<small>
+[ <a href="https://p.bndl.org/bandali-mmath-thesis.pdf">pdf</a>
+| <a href="https://hdl.handle.net/10012/16059">hdl</a>
+| <a href="https://bndl.org/mmath.html">http</a>
+]
+</small>
+</dt>
+<dd>
+<a href="https://bndl.org">Amin Bandali</a><br />
+<em><abbr title="Master of Mathematics">MMath</abbr> Thesis,
+University of Waterloo, David R. Cheriton School of Computer Science,
+July 2020.</em>
+</dd>
+</dl>
+
+<h3>Talks</h3>
+
+<dl>
+<dt>Jami and how it empowers users
+<small>
+[ <a href="https://p.bndl.org/bandali-jami-libreplanet-2021.pdf">pdf</a>
+(<a href="https://p.bndl.org/bandali-jami-libreplanet-2021-with-notes.pdf">with
+notes</a>)
+| <a href="https://bndl.org/libreplanet-2021.html">http</a>
+]
+</small>
+</dt>
+<dd>
+<a href="https://bndl.org">Amin Bandali</a><br />
+<em>Presented at the LibrePlanet 2021 Conference, March 20, 2021.</em>
+</dd>
+
+<dt>The Magic of Specifications and Type Systems
+<small>
+[ <a href="https://p.bndl.org/cucsc-2017-slides.pdf">slides</a>
+| <a href="https://p.bndl.org/eecs4080-poster.pdf">poster</a>
+]
+</small>
+</dt>
+<dd>
+<a href="https://bndl.org">Amin Bandali</a>,
+<a href="https://github.com/cipher1024">Simon Hudon</a>,
+<a href="https://www.eecs.yorku.ca/~jonathan/">Jonathan S. Ostroff</a><br />
+<em>Slides presented at the Canadian Undergraduate Computer Science
+Conference 2017, University of Toronto, Canada, June 15–17, 2017.<br />
+Poster presented at the Lassonde Undergraduate Summer Student Research
+Conference, York University, Toronto, Canada, August 15, 2017.</em>
+</dd>
+
+<dt>Introducing YULUG</dt>
+<dd>
+<a href="https://bndl.org">Amin Bandali</a><br />
+<em>Slides introducing YULUG — (GNU/)Linux User Group at York
+University — presented at a Computing Students Hub (CSHub) tech
+talk at York University, Toronto, Canada, February 12, 2015.</em>
+</dd>
+</dl>
+
+<h2>Work & Research Experience</h2>
+
+<dl>
+<dt>Savoir-faire Linux</dt>
+<dd>fall 2020–present | Free Software Consultant | Consultant en
+logiciel libre</dd>
+<dd>
+<dl>
+<dd>I am part of the Jami core development team at Savoir-faire Linux,
+where I work on various parts of Jami as a Free Software Consultant.
+These include working on and maintaining the GTK+-based jami-gnome
+client application written in C++ and C, and packaging Jami for
+various GNU/Linux distributions and other platforms. I also serve as
+a community liaison between the Jami core team and the wider free
+software community around Jami, with the goal of helping facilitate
+the communications and relations between the two.</dd>
+</dl>
+</dd>
+
+<dt>Free Software Foundation (FSF)</dt>
+<dd>spring 2020 | Intern</dd>
+<dd>
+<dl>
+<dd>Working with the FSF tech team in a sysadmin role on a variety of
+tasks including installation of the Sourcehut free software forge on
+the FSF infrastructure for evaluation for the FSF forge project, as
+well as a series of enhancements
+for <a href="https://www.gnu.org">www.gnu.org</a>.</dd>
+</dl>
+</dd>
+
+<dt>Cheriton School of Science, University of Waterloo</dt>
+<dd>winter 2018–spring 2020 | TA, IA, RA <sup>[*]</sup></dd>
+<dd>
+<dl>
+<dd>SE 465 (Software Testing and Quality Assurance): TA in winter
+2020</dd>
+<dd>SE 212 (Logic and Computation): <a href="se212-f19.html">IA in
+Fall 2019</a>, TA in fall 2018</dd>
+<dd>SE 463 (Software Requirement Specification and Analysis): TA in
+spring 2019 and 2018</dd>
+<dd>CS 136 (Elementary Algorithm Design and Data Abstraction): TA in
+winter 2018</dd>
+</dl>
+</dd>
+<dd><small>[*]: Teaching Assistant (marking exams and assignments),
+Instructional Apprentice (holding tutorials and marking), Research
+Assistant (doing research for/with supervisor)</small></dd>
+
+<dt>Department of Electrical Engineering & Computer Science, York
+University</dt>
+<dd>fall 2017 | Teaching Assistant</dd>
+<dd>
+<dl>
+<dd>EECS 1012 (Net-Centric Introduction to Computing): TA in fall
+2017, running labs and marking labs and exams</dd>
+</dl>
+</dd>
+
+<dt>Software Engineering Lab, York University</dt>
+<dd>
+<dl>
+<dt>summer 2017 | Research Assistant</dt>
+<dd>Worked on an implementation
+of <a href="https://bertrandmeyer.com/2014/12/07/lampsort/">Lampsort</a>
+in Eiffel. Extended
+the <a href="https://svn.eecs.yorku.ca/repos/sel-open/mathmodels/">mathmodels</a>
+library, implementing a <code>rational</code> class for working with
+arbitrarily large rational numbers.</dd>
+</dl>
+</dd>
+<dd>
+<dl>
+<dt>summer 2016 | Research Student</dt>
+<dd>Worked on <em>Literate Unit-B</em>, the verifier for Unit-B, a
+new formal method focused on formal verification of reactive,
+concurrent and distributed systems. From the Literate Unit-B codebase
+(written in Haskell), decoupled the logic module and used it to build
+<em>Unit-B Web</em>, a web interface using Literate Unit-B to do
+predicate calculus proofs. Unit-B Web, also written in Haskell,
+supports the <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span>
+syntax of the Unit-B logic, renders user input on the page, and calls
+the sequent prover of the logic module, which uses the Z3 SMT solver
+to check the validity of user input.</dd>
+<dd>Separated Literate Unit-B's type checker from its parser in a
+large refactoring, allowing easier substitution of other type checking
+algorithms, and in preparation for implementing subtyping.</dd>
+</dl>
+</dd>
+
+<dt>Lotek Wireless Inc.</dt>
+<dd>
+<dl>
+<dt>summer 2016 | Software Developer</dt>
+<dd>Designed and developed an Employee Portal web application in C#
+and the MVC framework, used by employees for accessing various data
+catalogs and archives.</dd>
+</dl>
+</dd>
+<dd>
+<dl>
+<dt>summer 2015 | Software Developer</dt>
+<dd>Designed and implemented various applications in C# and C for
+analyzing and testing a satellite pass prediction algorithm for
+predicting the pass windows of Argos satellites, for scheduling send
+times of data collected by the company's wildlife tracking
+products.</dd>
+</dl>
+</dd>
+
+<dt>Athlete Builder</dt>
+<dd>
+<dl>
+<dt>2013–2014 | Software Developer</dt>
+<dd>Developed the Backend of Athlete Builder platform in C# and
+MVC.</dd>
+<dd>Key role in development of the platform core.</dd>
+<dd>Developed the alpha version of Athlete Builder Android application
+in Java.</dd>
+</dl>
+</dd>
+</dl>
+
+<h2>Skills</h2>
+<dl>
+<dt>Programming languages</dt>
+<dd>C, C++, Haskell, Emacs Lisp, Guile Scheme, Python, Eiffel, Bash,
+C#, Java, JavaScript</dd>
+<dt>Tools</dt>
+<dd>GNU Emacs, Git, Alloy, TLA<sup>+</sup>,
+ProB, <span class="tex">L<sup>a</sup>T<sub>e</sub>X</span>, continuous
+integration systems</dd>
+<dt>Platforms</dt>
+<dd>GNU/Linux distributions, including Trisquel, GNU Guix, Debian</dd>
+<dt>Languages</dt>
+<dd>Persian (mother tongue), English (native proficiency; IELTS: 9.0),
+French (beginner)</dd>
+</dl>
+
+<h2>Community Service</h2>
+<dl>
+<dt>EmacsConf conference</dt>
+<dd>
+<dl>
+<dt>2019–present</dt>
+<dd>Chief organizer and maintainer of conference infrastructure,
+including the streaming servers.</dd>
+<dt>2015</dt>
+<dd>One of the organizers and in charge of setting up and maintaining
+vital pieces of infrastructure.</dd>
+</dl>
+</dd>
+<dt>Computer Science Club (CSC) of the University of Waterloo</dt>
+<dd>Served as the CSC System Administrator in Winter and Spring 2020.
+Present member of the CSC Systems Committee, overseeing and
+maintaining a large fleet of GNU/Linux servers for CSC members, as
+well as running the CSC mirror for free software projects.</dd>
+<dd>Notable projects
+include <a href="https://mailman.csclub.uwaterloo.ca/pipermail/csc-general/2020-July/000837.html">launching
+the CSC web IRC client</a> as part of an effort in bringing modern
+user freedom- and privacy-respecting communication tools to club
+members.</dd>
+<dt>Free/libre software contributions</dt>
+<dd>Co-maintainer
+of <a href="https://www.gnu.org/software/gnuzilla/gnuzilla.html">GNUzilla
+and IceCat</a>, the GNU version of the Mozilla suite and the Firefox
+browser respectively.</dd>
+<dd>Maintainer
+of <a href="https://www.gnu.org/software/emacs/erc.html">ERC</a>, the
+powerful, modular, and extensible IRC client distributed with GNU
+Emacs.</dd>
+<dd>Committer and regular contributor
+to <a href="https://www.gnu.org/software/emacs/emacs.html">GNU
+Emacs</a> and <a href="https://guix.gnu.org">GNU Guix</a>.</dd>
+<dd><a href="https://www.gnu.org/people/webmeisters.html#bandali">GNU
+webmaster</a>
+and <a href="https://savannah.gnu.org/maintenance/SavannahHacker/">GNU
+Savannah hacker</a>.</dd>
+<dt>Volunteer work</dt>
+<dd>
+<dl>
+<dt>spring 2013 | Application Developer for VONICAL Inc.</dt>
+<dd>Worked on development of the Employment Accessibility Resource
+Network (EARN) portal using the Anahita social networking platform,
+written in PHP and running on GNU/Linux.</dd>
+<dt>winter 2013 | Mobile & Web Developer for Hire Works Inc.</dt>
+<dd>Worked on a variety of web and mobile development projects for
+Hire Works.</dd>
+<dt>summer 2012 | Web Developer for St. Brigid's Summer Camp</dt>
+<dd>Redesigned and revamped the codebase for the photo gallery section
+of the camp's website in PHP and JavaScript.</dd>
+</dl>
+</dd>
+</dl>
+</body>
projects / ~bandali / bndl.org / blobdiff