| 1 | <!doctype html> |
| 2 | <html lang="en"> |
| 3 | <head> |
| 4 | <meta charset="utf-8" /> |
| 5 | <meta name=viewport content="width=device-width, initial-scale=1" /> |
| 6 | <title>Amin Bandali's Personal Site</title> |
| 7 | <meta |
| 8 | name="description" |
| 9 | content="Amin Bandali is a graduate student at WatForm, a free |
| 10 | software activist, and a GNU webmaster and volunteer." /> |
| 11 | <link rel="stylesheet" href="/style.css" /> |
| 12 | </head> |
| 13 | <body> |
| 14 | <nav><span>bandali.eu.org</span></nav> |
| 15 | <main> |
| 16 | <h1 id="hiddentitle">Amin Bandali</h1> |
| 17 | <section> |
| 18 | <p> |
| 19 | Hi, I’m |
| 20 | <a href="images/bandali-with-rms.jpg" |
| 21 | title="photo of bandali with rms wearing a “pay cash don’t be tracked” pin">Amin Bandali</a>. |
| 22 | I’m a graduate student at <a href="https://watform.uwaterloo.ca">WatForm</a> |
| 23 | at University of Waterloo, supervised by |
| 24 | <a href="https://cs.uwaterloo.ca/~nday/">Dr. Nancy Day</a>. |
| 25 | The main goal of my research is improving |
| 26 | <strong>software and systems reliability</strong> |
| 27 | through application of <em>formal methods</em>. |
| 28 | </p> |
| 29 | |
| 30 | <p> |
| 31 | My research at WatForm focuses on formal logic, model |
| 32 | checking, and verification. I’m also interested in |
| 33 | programming languages, theorem provers, and their type |
| 34 | systems. You may wish to view my |
| 35 | academic <a href="bandali-cv.html">curriculum vitae</a>. |
| 36 | </p> |
| 37 | |
| 38 | <p class="notice"> |
| 39 | <strong>SE 212 students:</strong> |
| 40 | see <a href="se212-f19/">here</a> for slides and other |
| 41 | material from the tutorials. |
| 42 | </p> |
| 43 | |
| 44 | <p> |
| 45 | On the side, I dabble in <a href="https://leanprover.github.io">Lean</a> |
| 46 | and enjoy <a href="https://stallman.org/articles/on-hacking.html">hacking</a> on |
| 47 | <a href="https://www.gnu.org/software/emacs/manual/elisp.html">Elisp</a>. |
| 48 | I’m a <a href="https://www.gnu.org/philosophy/free-sw.html">Free Software</a> activist |
| 49 | and FSF <a href="https://www.fsf.org/associate/">supporter</a>, and a GNU maintainer |
| 50 | and <a href="https://www.gnu.org/people/webmeisters.html#bandali">webmaster</a>. |
| 51 | I co-host the <a href="https://emacsel.com">Emacs.el</a> podcast with |
| 52 | <a href="https://www.pygopar.com">Daniel Gopar</a>, and |
| 53 | organize <a href="https://emacsconf.org">EmacsConf</a> with |
| 54 | help from many wonderful people. |
| 55 | |
| 56 | I am also a member of the Systems Committee for the |
| 57 | <a href="https://csclub.uwaterloo.ca">Computer Science Club |
| 58 | of the University of Waterloo</a>. |
| 59 | </p> |
| 60 | |
| 61 | <p> |
| 62 | See my <a href="contact.html">contact</a> page for how to |
| 63 | best reach me. |
| 64 | </p> |
| 65 | </section> |
| 66 | |
| 67 | <h3 id="papers">Papers</h3> |
| 68 | <dl> |
| 69 | <dt> |
| 70 | A Comparison of the Declarative Modelling Languages B, |
| 71 | Dash, and TLA<sup>+</sup> |
| 72 | <span class="plinks"> |
| 73 | [ |
| 74 | <a href="papers/modre2018-declarative.pdf">pdf</a> |
| 75 | | |
| 76 | <a href="papers/modre2018-declarative.bib">bib</a> |
| 77 | ] |
| 78 | </span> |
| 79 | </dt> |
| 80 | <dd> |
| 81 | Ali Abbassi, |
| 82 | <a href="https://bandali.eu.org">Amin Bandali</a>, |
| 83 | <a href="https://cs.uwaterloo.ca/~nday/">Nancy A. Day</a>, |
| 84 | and Jose Serna<br/> |
| 85 | <em>2018 IEEE 8th International Model-Driven Requirements |
| 86 | Engineering Workshop (MoDRE)</em><br/> |
| 87 | Copyright © 2018 IEEE. All Rights Reserved. Sadly. |
| 88 | </dd> |
| 89 | </dl> |
| 90 | |
| 91 | <h3 id="talks">Talks</h3> |
| 92 | <dl> |
| 93 | <dt> |
| 94 | The Magic of Specifications and Type Systems |
| 95 | <span class="plinks"> |
| 96 | [ |
| 97 | <a href="talks/cucsc-2017-slides.pdf" |
| 98 | title="presented at the Canadian Undergraduate Computer Science Conference 2017, |
| 99 | University of Toronto, Canada, June 15-17, 2017">slides</a> |
| 100 | | |
| 101 | <a href="talks/eecs4080-poster.pdf" |
| 102 | title="presented at the Lassonde Undergraduate Summer Student Research Conference, |
| 103 | York University, Toronto, Canada, August 15, 2017">poster</a> |
| 104 | ] |
| 105 | </span> |
| 106 | </dt> |
| 107 | <dd> |
| 108 | <a href="https://bandali.eu.org">Amin Bandali</a>, |
| 109 | <a href="https://github.com/cipher1024">Simon Hudon</a>, |
| 110 | <a href="http://www.cse.yorku.ca/~jonathan/">Jonathan Ostroff</a> |
| 111 | </dd> |
| 112 | </dl> |
| 113 | |
| 114 | <h3>Projects</h3> |
| 115 | <p> |
| 116 | Below are a number of free software projects I have worked on: |
| 117 | </p> |
| 118 | <dl> |
| 119 | <dt><a href="https://git.sr.ht/~bandali/george-mode">george-mode</a></dt> |
| 120 | <dd>Emacs major mode for editing George files</dd> |
| 121 | |
| 122 | <dt><a href="https://git.uwaterloo.ca/bandali/alloy-catalyst">alloy-catalyst</a></dt> |
| 123 | <dd>Framework for performance analysis of Alloy models</dd> |
| 124 | |
| 125 | <dt><a href="https://github.com/unitb/unitb-web">unitb-web</a></dt> |
| 126 | <dd>Web interface for Unit-B</dd> |
| 127 | |
| 128 | <dt><a href="https://github.com/unitb/tex2png-hs">tex2png-hs</a></dt> |
| 129 | <dd>Library and CLI for converting TeX and LaTeX to PNG images</dd> |
| 130 | </dl> |
| 131 | |
| 132 | <h3>Notes</h3> |
| 133 | <ul> |
| 134 | <!-- <li> |
| 135 | <a href="streaming-with-free-software.html">Streaming with |
| 136 | Free Software</a> |
| 137 | </li> --> |
| 138 | <li> |
| 139 | <a href="bandali-computing.html">How I do my computing</a> |
| 140 | </li> |
| 141 | </ul> |
| 142 | </main> |
| 143 | <footer> |
| 144 | <p> |
| 145 | Copyright © 2016–2019 Amin Bandali. |
| 146 | See <a href="/license.html">license.html</a> for license |
| 147 | conditions. Please copy and share. |
| 148 | </p> |
| 149 | </footer> |
| 150 | </body> |
| 151 | </html> |