| 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 | <meta name="description" content="Amin Bandali is a graduate |
| 7 | student at WatForm, the co-host of the Emacs.el |
| 8 | podcast, a free software advocate, and a volunteer |
| 9 | webmaster for the GNU project."/> |
| 10 | <title>Amin Bandali</title> |
| 11 | <link rel="stylesheet" href="/style.css" /> |
| 12 | </head> |
| 13 | <body> |
| 14 | <header> |
| 15 | <h1><a href="images/amin.png">Amin Bandali</a>’s personal site</h1> |
| 16 | <span id="sub"> |
| 17 | Graduate student at University of Waterloo supervised by |
| 18 | <a href="https://cs.uwaterloo.ca/~nday/">Nancy Day</a> |
| 19 | </span> |
| 20 | </header> |
| 21 | |
| 22 | <main> |
| 23 | <section> |
| 24 | <h2 id="contact">Contact</h2> |
| 25 | <table class="btable"> |
| 26 | <tbody> |
| 27 | <tr> |
| 28 | <th></th> |
| 29 | <th>academic</th> |
| 30 | <th>personal</th> |
| 31 | </tr> |
| 32 | <tr> |
| 33 | <td>email</td> |
| 34 | <td><a href="mailto:abandali@uwaterloo.ca">abandali@uwaterloo.ca</a></td> |
| 35 | <td><a href="mailto:bandali@gnu.org">bandali@gnu.org</a> |
| 36 | (<a href="gpg">gpg</a>)</td> |
| 37 | </tr> |
| 38 | <tr> |
| 39 | <td>git repos</td> |
| 40 | <td><a href="https://git.uwaterloo.ca/abandali">git.uwaterloo.ca/abandali</a></td> |
| 41 | <td><a href="https://git.sr.ht/~bandali">git.sr.ht/~bandali</a></td> |
| 42 | </tr> |
| 43 | <tr> |
| 44 | <td>other means</td> |
| 45 | <td>see <a href="contact">contact</a> page</td> |
| 46 | </tr> |
| 47 | </tbody> |
| 48 | </table> |
| 49 | </section> |
| 50 | |
| 51 | <section> |
| 52 | <h2 id="research-interests">Research interests</h2> |
| 53 | <p> |
| 54 | The main goal of my research is improving |
| 55 | <strong>software reliability</strong> |
| 56 | through application of <em>formal methods</em>. |
| 57 | </p> |
| 58 | |
| 59 | <p> |
| 60 | My current research at <a href="https://watform.uwaterloo.ca">WatForm</a> |
| 61 | focuses on formal logic, model checking, and verification. |
| 62 | Specifically, I am working on various optimizations aiming to |
| 63 | improve the analysis performance of the Alloy Analyzer on |
| 64 | models. |
| 65 | </p> |
| 66 | |
| 67 | <p> |
| 68 | I am also interested in programming languages, type systems, and |
| 69 | interactive theorem proving. |
| 70 | </p> |
| 71 | |
| 72 | <p> |
| 73 | On the side, I dabble in <a href="https://leanprover.github.io">Lean</a> |
| 74 | and <a href="https://www.rust-lang.org">Rust</a>, and enjoy |
| 75 | <a href="https://stallman.org/articles/on-hacking.html">hacking</a> on |
| 76 | <a href="https://www.gnu.org/software/emacs/manual/elisp.html">Emacs Lisp</a>. |
| 77 | I’m also a <a href="https://www.gnu.org/philosophy/free-sw.en.html">free software</a> |
| 78 | and <a href="https://www.gnu.org/licenses/copyleft.en.html">copyleft</a> |
| 79 | advocate, and a volunteer webmaster for the GNU project. |
| 80 | </p> |
| 81 | |
| 82 | <p> |
| 83 | You may wish to view my academic <a href="bandali-cv.pdf">curriculum vitae</a>. |
| 84 | </p> |
| 85 | </section> |
| 86 | |
| 87 | <section> |
| 88 | <h2 id="publications">Publications</h2> |
| 89 | <dl> |
| 90 | <dt> |
| 91 | <strong>A Comparison of the Declarative Modelling |
| 92 | Languages B, Dash, and TLA<sup>+</sup></strong> |
| 93 | (<a href="papers/2018-AbBaDaSe-modre.pdf">pdf</a>, |
| 94 | <a href="papers/2018-AbBaDaSe-modre.bib">bib</a>, |
| 95 | <a href="https://doi.org/10.1109/MoDRE.2018.00008">doi</a>, |
| 96 | <a href="https://cs.uwaterloo.ca/~nday/models/2018-modre">models</a>) |
| 97 | </dt> |
| 98 | <dd> |
| 99 | Ali Abbassi, <strong>Amin Bandali</strong>, Nancy A. Day, |
| 100 | and Jose Serna |
| 101 | </dd> |
| 102 | <dd> |
| 103 | <em>2018 IEEE 8th International Model-Driven Requirements |
| 104 | Engineering Workshop (MoDRE)</em> |
| 105 | </dd> |
| 106 | </dl> |
| 107 | <!-- <h3 id="theses">Theses</h3> --> |
| 108 | </section> |
| 109 | |
| 110 | <section> |
| 111 | <h2 id="presentations">Presentations</h2> |
| 112 | <dl> |
| 113 | <dt> |
| 114 | <strong>The Magic of Specifications and Type |
| 115 | Systems</strong> |
| 116 | </dt> |
| 117 | <dd><strong>Amin Bandali</strong>, Simon Hudon, |
| 118 | Jonathan Ostroff |
| 119 | </dd> |
| 120 | <dd><a href="presentations/cucsc-2017-slides.pdf">Slides</a> |
| 121 | presented at |
| 122 | <abbr title="Canadian Undergraduate Computer Science Conference"> |
| 123 | CUCSC 2017</abbr>, University of Toronto, Canada, June |
| 124 | 15-17, 2017. |
| 125 | </dd> |
| 126 | <dd><a href="presentations/eecs4080-poster.pdf">Poster</a> |
| 127 | presented at |
| 128 | <abbr title="Lassonde Undergraduate Summer Student Research Conference"> |
| 129 | Lassonde USSR Conference</abbr>, York University, Toronto, Canada, |
| 130 | August 15, 2017.</dd> |
| 131 | </dl> |
| 132 | </section> |
| 133 | |
| 134 | <section> |
| 135 | <h2 id="writings">Writings</h2> |
| 136 | <dl> |
| 137 | <dt>Will be added soon.</dt> |
| 138 | <!-- <dd></dd> --> |
| 139 | </dl> |
| 140 | </section> |
| 141 | </main> |
| 142 | <footer> |
| 143 | <p> |
| 144 | Copyright (c) 2016–2019 Amin Bandali<br> |
| 145 | Verbatim copying and redistribution of this entire page are |
| 146 | permitted provided this notice is preserved.<br> |
| 147 | The <a href="https://www.gnu.org/graphics/gnu-inside.html"> |
| 148 | GNU Inside</a> banner is available under the |
| 149 | <a href="https://creativecommons.org/licenses/by-sa/2.0/"> |
| 150 | Creative Commons Attribution-ShareAlike 2.0 License</a>. |
| 151 | </p> |
| 152 | <div id="gnu-inside"> |
| 153 | <a href="https://www.gnu.org"> |
| 154 | <img src="images/gnu-inside.png" |
| 155 | alt="GNU Inside!" title="GNU Inside!"/> |
| 156 | </a> |
| 157 | </div> |
| 158 | </footer> |
| 159 | </body> |
| 160 | </html> |