Commit | Line | Data |
---|---|---|
cb742bb6 AB |
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> | |
8b2bd489 AB |
90 | <dt> |
91 | <strong>A Comparison of the Declarative Modelling | |
92 | Languages B, Dash, and TLA<sup>+</sup></strong> | |
cb742bb6 AB |
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> | |
8b2bd489 AB |
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> | |
cb742bb6 AB |
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> |