-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
executable file
·355 lines (334 loc) · 17.1 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
<!doctype html>
<html lang="en">
<head>
<link rel="shortcut icon" type="image/x-icon" href="/favicon.ico">
<meta charset="utf-8">
<title> Ashutosh Trivedi | Computer Science | University of Colorado Boulder</title>
<meta name="MobileOptimized" content="width">
<meta name="HandheldFriendly" content="true">
<meta name="viewport" content="width=device-width">
<meta name="google-site-verification" content="8Y9RWHBEMOdCM4S2aIA_cCzxcvn6jkMzRfzwNA2O48U" />
<link rel="stylesheet" href="css/grid.css">
<link rel="stylesheet" href="css/ucb-styles.css">
<link rel="stylesheet" href="css/styles.css">
<link href="https://fonts.googleapis.com/css?family=Roboto:400,700|Roboto+Condensed:700" rel="stylesheet">
<link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.3.1/css/all.css" integrity="sha384-mzrmE5qonljUremFsqc01SB46JvROS7bZs3IO2EmfFsd15uHvIt+Y8vEf7N7fWAU" crossorigin="anonymous">
<link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.3.1/css/v4-shims.css">
<script src="https://code.jquery.com/jquery-2.2.4.min.js" integrity="sha256-BbhdlvQf/xTY9gja0Dq3HiwQF8LaCRTXxZKRutelT44=" crossorigin="anonymous"></script>
<link href='http://fonts.googleapis.com/css?family=Ultra' rel='stylesheet' type='text/css'>
<link href="https://fonts.googleapis.com/css?family=Shrikhand" rel="stylesheet">
<link href="https://fonts.googleapis.com/css?family=Open+Sans:400,800" rel="stylesheet">
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin="">
<link href="https://fonts.googleapis.com/css2?family=Roboto+Condensed:wght@700&family=Roboto:wght@400;700&display=swap" rel="stylesheet">
</head>
<!-- Body Starts here -->
<body class="headings-bold background-color-white">
<div class="page">
<!-- CU Boulder bar -->
<div class="background-black brand-bar brand-bar-black">
<div class="container">
<script type="text/javascript" src="https://cdn.colorado.edu/static/brand-assets/live/js/brand-bar.js" id="ucb-brand-bar-embed" data-color="black"></script>
</div>
</div>
<!-- CS/CEAS header -->
<header class="ucb light" role="banner">
<div class="container">
<a href="/">Department of Computer Science</a>
<div class="affiliation">
<a href="https://www.colorado.edu/engineering">College of Engineering and Applied Science</a>
</div>
</div>
</header>
<!-- navigation bar -->
<div class="background-color-gray-dark">
<div class="container">
<nav role="navigation" class="ucb-navbar ucb-navbar-dark text-minify">
<label for="show-main-menu" class="show-menu">
<i class="fa fa-bars" aria-hidden="true"></i>
<span class="element-invisible">Menu</span>
</label>
<input type="checkbox" id="show-main-menu" role="button">
<ul>
<li><a href="index.html" class="active"> <i class="fa fa-home"></i>
<span class="display-inline invisible-md invisible-lg">Home</span></a></li>
<li><a href="pubs.html">Publications</a></li>
<li><a href="teaching.html">Teaching</a></li>
<li><a href="ser.html">Service</a></li>
<li><a href="bio.html">Bio</a></li>
</ul>
</nav>
</div>
</div>
<!-- intro bar -->
<div class="background-white padding-large-top padding-large-bottom">
<div class="container">
<div class="row">
<table class="table-noborder" style="width: 100%;">
<tr>
<td style='width:250px;'>
<img class="image-200px circular image-block" src="recent.jpg" alt="placeholder image">
</td>
<td align=left style="max-width: 99%">
<div>
<h2 id="page-title">Ashutosh Trivedi</h2>
Associate Professor of <a href="http://www.cs.colorado.edu">
Computer Science </a> <br>
<p align =left>
<strong> Email</strong>: ashutosh.trivedi @ colorado.edu <br>
<strong> Web</strong>: <a href="http://ashutoshtrivedi.com"> Home </a>,
<a href="https://twitter.com/astrivedi/">Twitter</a>,
<a href="https://scholar.google.com/citations?user=9WDXyy4AAAAJ">
Google Scholar</a>,
<a href="https://dblp.uni-trier.de/pers/hd/t/Trivedi_0001:Ashutosh">
DBLP</a>, <a href="http://www.researcherid.com/rid/B-9196-2017">
ResearchID</a>, <a href="http://orcid.org/0000-0001-9346-0126">
ORCID </a>, and <a href="https://www.researchgate.net/profile/Ashutosh_Trivedi">ResearchGate</a>. <br>
<strong> Research Interests </strong>:
Safety in AI · Reinforcement Learning · Formal
Methods · Software Fairnes · Software Accountability <br>
<strong> Group</strong>: <a href="http://plv.colorado.edu"> Programming
Languages and Verification (CUPLV) </a>
</p>
</div>
</td>
</tr>
</table>
</div>
<div class="content background-gold-light padding margin-bottom ">
<p> <strong>Artificial Intelligence</strong> (AI) assisted software solutions have
made substantial inroads in critical aspects of modern
existence where they routinely make safety-, socio-, and legal-
critical decision with certainty and swift. Instances of such
AI-assisted decisions include: self-driving cars deciding to
stop, implantable pacemakers deciding to pace, or the COMPAS
(Correctional Offender Management Profiling for Alternative
Sanctions) software deciding if individuals are prone to
reoffend. These AI-assisted software are data-driven: they
adapt their behavior based experiences in the form of data: be
it the expertly curated data in <em>supervised learning</em>, surprising
patterns hidden in raw data in <em>unsupervised learning</em>, or the
self-generated data guided by expertly designed reward signals
in <em>reinforcement learning</em>. The focus of my research is on enabling
<em> rigorous system engineering </em> of data-driven system towards
improved
safety, privacy, fairness, and accountability. </p>
<p>While <strong>formal methods</strong> for rigorous system engineering provide principles,
processes, and practices for traditional systems development, data-driven
systems---due to their statistical, inductive, and adaptive nature---demand a
paradigm shift.
My research seeks to understand and to redefine the
role of formal methods in data-driven system development. While I
continue to leverage my expertise in analyzing functional
requirements including safety and privacy, I am actively exploring the applications of
formal methods in analyzing legal and societal implications of data-driven
software systems. Some notable examples from my current research
include:
<ul class="list-style-icon-angle-double">
<li>
the role of formal requirements in <em> reinforcement learning </em>,
<li>
the use of automatic testing and debugging in fairness-aware configuration of
machine learning libraries, and
<li> the role of formal specifications in
expressing correctness requirements for the tax-preparation software.
</ul>
</p>
</div>
<div class="content background-yellow padding margin-bottom ">
<h3>
News.
</h3>
<ul class="list-style-icon-angle-double">
<li> [Jan '25] <b>Job Opportunity: Undergraduate Research Assistant in Neurosymbolic AI</b>
<ul>
<li><strong>Job Title:</strong> Undergraduate Summer Research Assistant</li>
<li><strong>Key Responsibilities:</strong>
<ul>
<li>Training systems using Reinforcement Learning and Hebbian Learning</li>
<li>Deploying SMT solvers to verify system properties</li>
<li>Writing research papers</li>
</ul>
</li>
<li><strong>Qualifications:</strong>
<ul>
<li>Strong background in discrete mathematics</li>
<li>Proficiency in machine learning, particularly Reinforcement Learning and Hebbian Learning</li>
<li>Aptitude for theoretical computer science</li>
</ul>
</li>
<li><strong>Compensation:</strong> $18–$28 per hour (based on prior experience)</li>
<li><strong>Application Process:</strong>
Interested candidates should email their application to
<a href="mailto:[email protected]">[email protected]</a>.
</li>
</ul>
</li>
<li> [May'22] The <a href="https://esweek.org/memocode/"> call
for papers</a> for the 20th ACM/IEEE International Symposium on Formal
Methods and Models for System Design (MEMCODE) is out. Consider submitting your latest work on formal
methods and models.
<li> Our article in the Annual Reviews in Control on <a href ="https://authors.elsevier.com/c/1esEX4syv1upte"> Secure-by-construction synthesis of cyber-physical systems</a>
is available online.
<li> [Apr'22] Congratulations to Mateo Perez on receiving Bell
Foundation Outstanding Research Award 2022.
<li> [Apr'22] Congratulations to Vishnu Murali on receiving
Departmental Outstanding Research Award 2022.
<li> [Feb'22] I look forward to organizing the 8th workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT
<li> [Jan'22] Paper by Murali et al. “k-Inductive Barrier Certificates for Stochastic Systems” accepted to HSCC’22.
<li> [Jan'22] Received the NSF 2022 CAREER Award to
investigate Reinforcement Learning for Recursive Markov Decision Processes and Beyond</em>.
<li> [Jan'22] I am teaching CSCI 2270 (Data Structures) this
spring (Details on Canvas).
<li> [Dec'21] Paper by Velasquez et al. on "Controller Synthesis
for Omega-Regular and Steady-State Specifications" accepted to AAMAS’22.
<li> [Dec'21] Paper by Perez et al. on "Translating Omega-Regular Specifications to Average Objectives for Model-Free Reinforcement Learning” accepted to AAMAS’22.
<li> [Dec'21] Paper by Tizpaz-Niari et al. on "Fairness-aware
Configuration of Machine Learning Libraries" accepted to
ICSE'21.
<li> [Nov'21] Congratulations
to <a href="https://taylordohmen.github.io"> Taylor Dohmen </a> on delivering an excellent
presentation on "Regularity in Transducers and Applications in Reinforcement
Learning" for his area exam.
<li> [Oct'21] <a href="https://plv.colorado.edu/tianhan/"> Tianhan Lu</a> wins the Radhia Cousot Young Researcher Best Paper Award
at <a href="https://conf.researchr.org/home/sas-2021">SAS
2021</a>.
<li> [Aug'21] Congratulations
to <a href="https://plv.colorado.edu/tianhan/"> Tianhan Lu</a> on successfully defending his thesis
proposal.
<li> [Aug'21] Paper by Komp et al. on “Event-Triggered and
Time-Triggered Duration Calculus for Model-Free Reinforcement
Learning” accepted to RTSS'21.
<li> [July'21] Paper by Perez et al. “Model-Free Reinforcement
Learning for Lexicographic Omega-Regular Objectives” accepted
to Formal Methods (FM'21).
<li> [July'21] Paper by Murali et al. on “Safety Verification of
Dynamical Systems via k-Inductive Barrier Certificates” accepted to CDC'21.
<li> [July'21] Paper by Dohmen et al. on <a href="https://link.springer.com/chapter/10.1007/978-3-030-86593-1_13">“Regular Model
Checking with Regular Relations”</a> accepted to <a href="http://www.corelab.ntua.gr/fct2021/">Fundamentals of Computation Theory (FCT'21)</a>.
<li> [July'21] Paper
by <a href="https://plv.colorado.edu/papers/brbo-sas21.html">Lu
et al.</a> accepted to<a href="https://conf.researchr.org/home/sas-2021"> SAS 2021</a>.
<li> [June'21] <a href="https://plv.colorado.edu/wwwmungojerrie/"> Mungojerrie
(beta release) </a> is available for download.
<li> [April'21] Paper by Perez et al. on <em> <a href="https://doi.org/10.1007/978-3-030-81688-9_30"> Model-Free Reinforcement Learning for
Branching Markov Decision Processes </a></em> accepted
to <a href="http://i-cav.org/2021/program/">CAV'21 </a>.
</ul>
</div>
<div class="padding background-color-gray-light">
<h3> Current PhD Students. </h3>
<div class="row equal-height">
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="dohmen.jpg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://taylordohmen.github.io"
class="button button-blue
margin-top-auto"> Taylor
Dohmen</a></p>
<p class="card-text"><strong>Interests.</strong> <em>Regular Relations and
Reinforcement Learning</em></p>
</div>
</div>
</div>
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="joko.jpeg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://dblp.org/pid/174/1975.html"
class="button button-blue margin-top-auto">John Komp</a></p>
<p class="card-text"><strong>Interests.</strong> <em> Duration Calculus and
Reinforcement Learning</em></p>
</div>
</div>
</div>
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="tilu.jpg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://dblp.org/pid/228/8429.html"
class="button button-blue
margin-top-auto">Tianhan Lu</a></p>
<p class="card-text"><strong>Interests.</strong> <em> Static
Analysis for Resource and Cost Bounding <br></em></p>
</div>
</div>
</div>
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="vishnu.jpg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://dblp.org/pid/292/7538.html"
class="button button-blue margin-top-auto">Vishnu Murali</a></p>
<p class="card-text"><strong>Interests.</strong> <em>
Foundations of Cyber-Physical Systems Verification and Synthesis</em></p>
</div>
</div>
</div>
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="mape.jpeg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://dblp.org/pid/228/6991.html"
class="button button-blue margin-top-auto">Mateo Perez</a></p>
<p class="card-text"><strong>Interests.</strong> <em>
Automata-Theoretic Reinforcement Learning</em></p>
</div>
</div>
</div>
</div>
</div>
<div class="padding margin-bottom content background-gray-100">
<h3> Graduated PhD Students </h3>
<div class="row equal-height">
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="saeid.jpeg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://sites.google.com/a/colorado.edu/saeid-tizpaz-niari/"
class="button button-blue
margin-top-auto">Saeid Tizpaz-Niari</a></p>
<p class="card-text"><strong>Thesis.</strong> <em>
Differential Performance Debugging and its
application to side-channel analysis (2020)</em></p>
<p class="card-text"><strong>First Employment.</strong> <em>
Assistant Professor at UT El Paso</em></p>
</div>
</div>
</div>
<div class="col-sm-2">
<div class="card margin-bottom">
<img class="card-image-top" src="debh.jpeg" alt="placeholder image">
<div class="card-body last-margin-none">
<p class="margin-top-auto"><a href="https://www.linkedin.com/in/devendra-bhave-0101a48a/?originalSubdomain=in"
class="button button-blue margin-top-auto">Devendra Bhave</a></p>
<p class="card-text"><strong>Thesis.</strong> <em>
Perfect Subclasses of Real-timed Recursive Systems (2020) </em></p>
<p class="card-text"><strong>First Employment.</strong> <em>
Senior Software Engineer, Mathworks
</em></p>
</div>
</div>
</div>
</div>
</div>
</div>
<footer class="background-black padding-top padding-bottom">
<div class="container">
<div class="row">
<div class="col-lg-4 col-md-4 col-sm-6 col-xs-12">
This HTML template is a resource provided by <a href="https://www.colorado.edu/strategicrelations">Strategic Relations and Communications</a>.
</div>
<div class="col-log-4 col-md-4 col-sm-6 col-xs-12 offset-lg-4 offset-md-4">
<script type="text/javascript"
src="https://cdn.colorado.edu/static/brand-assets/live/js/footer.js"
id="ucb-footer-embed" data-color="white"></script>
</div>
</div>
</div>
</footer>
</div>
</div>
</body>
</html>