curriculum vitae

                             Amin Bandali

              phone: available upon request via email

              this file:
              last update: 2021-08-31


  - Experience in building software for diverse areas and platforms
    in various programming languages such as C, Python, and Haskell.

  - Passionate about applying scientific and engineering methods
    while designing and building software systems.

  - Using formal specification techniques to find specification-level
    bugs early in the design stage rather than implementation.

  - GNU/Linux system administration on both the client and the server

  - 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.

  - 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.


  Master of Mathematics in Computer Science, University of Waterloo,

    Research focus:
      formal logic, model checking, verification
      A Comprehensive Study of Declarative Modelling Languages
      Prof. Nancy A. Day

  Bachelor of Science with Honours in Computer Science, York
  University, 2017

    Favourite courses:
      System Specification & Refinement, Software Requirements
      Engineering, Software Design, Operating Systems, Computational
      Complexity, Design & Analysis of Algorithms


  formal logic, model checking, theorem proving, verification


  The complete bibliography of my publications is available as
  a BibTeX bibliography file from


    A Comparison of the Declarative Modelling Languages B, DASH,
    and TLA+

      Ali Abbassi, Amin Bandali, Nancy A. Day, Jose Serna
      8th IEEE International Model-Driven Requirements
      Engineering Workshop, MoDRE@RE 2018
      Copyright (c) 2018 IEEE.  All Rights Reserved.  Sadly.



    A Comprehensive Study of Declarative Modelling Languages

      Amin Bandali
      MMath Thesis, University of Waterloo, David R. Cheriton
      School of Computer Science, July 2020.



    Jami and how it empowers users

      Amin Bandali
      Presented at the LibrePlanet 2021 Conference, March 20, 2021.

      slides with notes:

    The Magic of Specifications and Type Systems

      Amin Bandali, Simon Hudon, Jonathan S. Ostroff
      Slides presented at the Canadian Undergraduate Computer Science
      Conference 2017, University of Toronto, Canada, June 15-17,
      Poster presented at the Lassonde Undergraduate Summer Student
      Research Conference, York University, Toronto, Canada,
      August 15, 2017.


    Introducing YULUG

      Amin Bandali
      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.


  Savoir-faire Linux

    fall 2020-present | Free Software Consultant
                      | Consultant en logiciel libre

      I am part of the Jami core development team at Savoir-faire
      Linux, where I get to 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.

  Free Software Foundation (FSF)

    spring 2020 | Intern

      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

  Cheriton School of Science, University of Waterloo

    winter 2018-spring 2020 | TA, IA, RA [*]

      SE 465 (Software Testing and Quality Assurance):
        TA in winter 2020
      SE 212 (Logic and Computation):
        IA in Fall 2019, TA in fall 2018
      SE 463 (Software Requirement Specification and Analysis):
        TA in spring 2019 and 2018
      CS 136 (Elementary Algorithm Design and Data Abstraction):
        TA in winter 2018

    [*]: Teaching Assistant (marking exams and assignments),
    Instructional Apprentice (holding tutorials and marking),
    Research Assistant (doing research for/with supervisor)

  Department of Electrical Engineering & Computer Science, York

    fall 2017 | Teaching Assistant

      EECS 1012 (Net-Centric Introduction to Computing):
        TA in fall 2017, running labs and marking labs and exams

  Software Engineering Lab, York University

    summer 2017 | Research Assistant

      Worked on an implementation of Lampsort in Eiffel.
      Extended the mathmodels library, implementing a rational
      class for working with arbitrarily large rational numbers.

    summer 2016 | Research Student

      Worked on Literate Unit-B, 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 Unit-B Web, a web interface using Literate Unit-B to do
      predicate calculus proofs.  Unit-B Web, also written in Haskell,
      supports the LaTeX 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.

      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

  Lotek Wireless Inc.

    summer 2016 | Software Developer

      Designed and developed an Employee Portal web application in C#
      and the MVC framework, used by employees for accessing various
      data catalogs and archives.

    summer 2015 | Computer Programmer

      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

  Athlete Builder

    2013-2014 | Software Developer

      Developed the Backend of Athlete Builder platform in C# and MVC.

      Key role in development of the platform core.

      Developed the alpha version of Athlete Builder Android
      application in Java.


  Programming languages
    C, C++, Haskell, Emacs Lisp, Guile Scheme, Python, Eiffel, Bash,
    C#, Java, JavaScript

    GNU Emacs, Git, Alloy, TLA+, ProB, LaTeX, continuous integration

    GNU/Linux distributions, including Trisquel, GNU Guix, Debian

    Persian (mother tongue), English (native proficiency; IELTS: 9.0),
    French (beginner)


  EmacsConf conference


      Chief organizer and maintainer of conference infrastructure,
      including the streaming servers.


      One of the organizers and in charge of setting up
      and maintaining vital pieces of infrastructure.

  Computer Science Club (CSC) of the University of Waterloo

    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.

    Notable projects include launching the CSC web IRC client
    as part of an effort in bringing modern user freedom- and
    privacy-respecting communication tools to club members.

  Free/libre software contributions

    Co-maintainer of GNUzilla and IceCat, the GNU version of
    the Mozilla suite and the Firefox browser respectively.

    Maintainer of ERC, the powerful, modular, and extensible
    IRC client distributed with GNU Emacs.

    Committer and regular contributor to GNU Emacs and GNU Guix.

    GNU webmaster and GNU Savannah hacker.

  Volunteer work

    spring 2013 | Application Developer for VONICAL Inc.

      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.

    winter 2013 | Mobile & Web Developer for Hire Works Inc.

      Worked on a variety of web and mobile development projects for
      Hire Works.

    summer 2012 | Web Developer for St. Brigid's Summer Camp

      Redesigned and revamped the codebase for the photo gallery
      section of the camp's website in PHP and JavaScript.