-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
529 lines (499 loc) · 34 KB
/
index.html
File metadata and controls
529 lines (499 loc) · 34 KB
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
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
<!doctype html>
<html class="no-js" lang="en">
<head>
<meta charset="utf-8">
<meta http-equiv="x-ua-compatible" content="ie=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>Kyungmin Bae</title>
<link rel="stylesheet" href="css/app.css">
<link rel="stylesheet" href="css/my.css">
</head>
<body>
<section id="contact" data-magellan-target="contact">
<div class="row">
<div class="medium-3 columns">
<img class="thumbnail" id="mypic" width="250px" src="image/bae.png">
</div>
<div class="medium-9 columns end">
<h1 id="name">Kyungmin Bae</h1>
<p>
<span>Associate Professor</span>
<br/>
<span><a href="http://cse.postech.ac.kr/">Department of Computer Science and Engineering</a></span>
<br/>
<span><a href="http://www.postech.ac.kr/">POSTECH</a> (Pohang University of Science and Technology)</span>
</p>
<dl id="contact">
<dt>Email</dt>
<dd>kmbae at postech.ac.kr</dd>
<dt>Office</dt>
<dd>B2 219</dd>
<dt>Phone</dt>
<dd>+82-54-279-2256</dd>
<dt>Address</dt>
<dd>77 Cheongam-Ro, Nam-Gu, Pohang, Gyeongbuk, Korea 37673</dd>
</dl>
</div>
</div>
<div id="top-menu" >
<div class="title-bar" data-responsive-toggle="menu-items" data-hide-for="medium">
<button class="menu-icon" type="button" data-toggle></button>
<div class="title-bar-title">Menu</div>
</div>
<div id="menu-container" data-sticky-container>
<div class="sticky" id="menu-items" data-sticky data-margin-top="0" style="width:100%;" data-margin-bottom="0" data-top-anchor="pgbegin:top" data-btm-anchor="pgend:bottom">
<nav data-magellan class="sticky-mag" data-bar-offset="20">
<ul class="top-bar vertical medium-horizontal menu expanded" >
<li><a href="#contact">Contact</a></li>
<li><a href="#about">About</a></li>
<li><a href="#papers">Publication</a></li>
<li><a href="#bio">Biography</a></li>
</ul>
</nav>
</div>
</div>
</div>
<div id="pgbegin"></div>
</section>
<section id="about" data-magellan-target="about">
<div class="column row">
<h2>About</h2>
<p>
I am an associate professor in the <a href="http://cse.postech.ac.kr/">Department of Computer Science and Engineering</a> at <a href="http://www.postech.ac.kr/">POSTECH</a>, and lead the <a href="http://sv.postech.ac.kr">Software Verification Laboratory</a>.
I study automatic formal analysis and software engineering methods to develop safe and reliable computer systems.
</p>
</div>
<div class="column row">
<h2>Research Interests</h2>
<ul>
<li>Formal methods to develop safe, reliable, and secure software, cyber-physical, and AI-based systems</li>
<li>Scalable yet precise automatic analysis techniques, based on model checking, automated reasoning, and computational logic</li>
</ul>
</div>
<div class="column row">
<h2>Professional Activities</h2>
<ul>
<li> Program committee (co-)chair </li>
<ul>
<li>
<a href="http://sv.postech.ac.kr/wrla2022"> WRLA 2022</a>,
<a href="https://www.formalise.org/content/formalise-2020">FormaliSE 2020</a>,
<a href="http://sevlab.postech.ac.kr/facs18/">FACS 2018</a>
</li>
</ul>
<li> Program committee member </li>
<ul>
<li>
ATVA (<a href="https://atva-conference.org/2023">2023</a>),
CAV (<a href="http://www.i-cav.org/2023">2023</a>),
ICTAC (<a href="https://ictac2024.cs.ait.ac.th">2024</a>,<a href="https://ictac2023.compsust.utec.edu.pe">2023</a>,<a href="https://ictac2021.github.io/">2021</a>),
SPIN (<a href="https://spin-web.github.io/SPIN2023/">2023</a>, <a href="https://spin2022chi.web.illinois.edu/">2022</a>),
APSEC (<a href="https://conf.researchr.org/home/apsec-2023">2023</a>, <a href="https://conf.researchr.org/home/apsec-2022">2022</a>, <a href="https://apsec2021.seat.org.tw/">2021</a>),
FormaliSE (<a href="https://conf.researchr.org/home/Formalise-2024">2024</a>, <a href="https://conf.researchr.org/home/Formalise-2023">2023</a>, <a href="https://conf.researchr.org/home/icse-2022/Formalise-2022">2022</a>, <a href="https://conf.researchr.org/home/Formalise-2021">2021</a>),
FACS (<a href="https://facs-conference.github.io/2024/">2024</a>, <a href="https://facs-conference.github.io/2023/">2023</a>, <a href="https://facs-conference.github.io/2022/">2022</a>, <a href="https://facs2021.inria.fr/">2021</a>, <a href="http://facs2019.org/">2019</a>, <a href="http://facs2017.di.uminho.pt/">2017</a>, <a href="http://events.femto-st.fr/facs2016/">2016</a>, <a href="http://facs2015.ic.uff.br/">2015</a>),
SEKE (<a href="https://ksiresearch.org/seke/seke24.html">2024</a>, <a href="http://ksiresearch.org/seke/seke23.html">2023</a>, <a href="http://ksiresearch.org/seke/seke22.html">2022</a>, <a href="http://ksiresearch.org/seke/seke21.html">2021</a>, <a href="https://ksiresearch.org/seke/seke20.html">2020</a>, <a href="https://ksiresearchorg.ipage.com/seke/seke17.html">2017</a>),
APLAS (<a href="https://conf.researchr.org/home/aplas-2021">2021</a>),
ICSE-SEIP (<a href="https://conf.researchr.org/track/icse-2020/icse-2020-Software-Engineering-in-Practice?track=ICSE%20Software%20Engineering%20in%20Practice">2020</a>),
TASE (<a href="https://sei.ecnu.edu.cn/tase2020/">2020</a>),
SEFM (<a href="https://sefm2019.inria.fr/">2019</a>),
WRLA (<a href="https://wrla2024.gitlab.io/">2024</a>, <a href="http://wrla2020.webs.upv.es/">2020</a>, <a href="https://project.inria.fr/wrla18/">2018</a>, <a href="https://fmse.info.uaic.ro/event/wrla2016/">2016</a>),
FTSCS (<a href="https://2023.splashcon.org/home/ftscs-2023">2023</a>, <a href="https://2022.splashcon.org/home/ftscs-2022">2022</a>, <a href="https://old.ftscs.org/2019/">2019</a>, <a href="https://old.ftscs.org/2018/">2018</a>, <a href="https://old.ftscs.org/2016/">2016</a>, <a href="http://old.ftscs.org/2015">2015</a>, <a href="http://www.ftscs.org/2014">2014</a>),
TTCS (<a href="http://cs.ipm.ac.ir/ttcs/2020/">2020</a>)
<!--FMi 2015--></li>
</ul>
<!--li> External reviewer</li>
<ul>
<li><a href="http://hscc2017.ece.illinois.edu/">HSCC 2017</a>, <a href="https://www.etaps.org/2016/tacas">TACAS 2016</a>, <a href="http://rdp15.mimuw.edu.pl/index.php?site=rta">RTA 2015</a>, <a href="https://www.etaps.org/2015/fase">FASE 2015</a></li>
</ul-->
<li> Invited speaker and lecturer</li>
<ul>
<li>
<a href="https://2023.splashcon.org/home/ftscs-2023">FTSCS 2023</a>,
<a href="https://ifip-wg-rewriting.cs.ru.nl/summerschool.html">ISR 2018</a>
</li>
</ul>
</ul>
</div>
<div class="column row">
<h2>Software</h2>
<ul>
<li> <a href="https://hybridsynchaadl.github.io/">HybridSynchAADL tool</a> </li>
<li> <a href="https://stlmc.github.io/">stlMC: a bounded model checker for hybrid systems</a> </li>
<li> <a href="https://maude-se.github.io/">Maude-SE: RW/SMT extension of Maude</a> </li>
<li> <a href="http://maude.cs.illinois.edu/tools/tlr/">Maude LTLR Model Checker</a> </li>
<li> <a href="http://maude.cs.illinois.edu/tools/lmc/">Maude LTL LMC Model Checker</a> </li>
<!--li> <a href="http://maude.cs.illinois.edu/tools/synchaadl">SynchAADL2Maude tool</a> </li-->
</ul>
</div>
<div class="column row">
<h2>Teaching</h2>
<ul>
<li> CSED502: Theory of Computation (2024 Fall) </li>
<li> CSED490H: Programming Studio (2024 Spring) </li>
<li> CSED332: Software Design Methods (2016-2021 Fall, 2023 Fall) </li>
<li> CSED420: Software Verification (2016 Spring, 2020-2022 Spring) </li>
<li> CSED321: Programming Languages (2019 Spring) </li>
<li> CSED433: Logic in Computer Science (2018 Spring)</li>
<li> CSED507: Software Engineering (2017 Spring)</li>
</div>
</section>
<section id="papers" data-magellan-target="papers">
<div class="column row">
<h2>Publications</h2>
<div>
<h3> Conference Papers </h3>
<ol>
<li>
<span class="title">Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption</span>
<span class="author">Jaeseo Lee and Kyungmin Bae</span>
<span class="ref">International Symposium on Formal Methods (FM)</span>
<span class="year">2024</span>
<span class="note">(To appear)</span>
</li>
<li>
<span class="title">Formal Specification of Trusted Execution Environment APIs</span>
<span class="author">Geunyeol Yu, Seunghyun Chae, Kyungmin Bae, and Sungkun Moon</span>
<span class="ref">International Conference on Fundamental Approaches to Software Engineering (FASE)</span>
<span class="year">2024</span>
</li>
<li>
<span class="title">Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving</span>
<span class="author">Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, and Fredrik Romming</span>
<span class="ref">International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets)</span>
<span class="year">2023</span>
</li>
<li>
<span class="title">Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL</span>
<span class="author">Kyungmin Bae and Peter Olveczky</span>
<span class="ref">International Conference on Formal Aspects of Component Software (FACS)</span>
<span class="year">2023</span>
</li>
<li>
<span class="title">An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs</span>
<span class="author">Jaehun Lee, Kyungmin Bae and Peter Olveczky</span>
<span class="ref">International Symposium on Leveraging Applications of Formal Methods (ISoLA)</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">STLmc: Robust STL Model Checking of Hybrid Systems using SMT</span>
<span class="author">Geunyeol Yu, Jia Lee, and Kyungmin Bae</span>
<span class="ref"> International Conference on Computer Aided Verification (CAV)</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">Efficient SMT-Based Model Checking for Signal Temporal Logic</span>
<span class="author">Jia Lee, Geunyeol Yu, and Kyungmin Bae</span>
<span class="ref">IEEE/ACM International Conference on Automated Software Engineering (ASE)</span>
<span class="year">2021</span>
</li>
<li>
<span class="title">MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-Physical Systems</span>
<span class="author">Kyungmin Bae and Peter Olveczky</span>
<span class="ref">International Conference on Embedded Software (EMSOFT)</span>
<span class="year">2021</span>
</li>
<li>
<span class="title">HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL</span>
<span class="author">Jaehun Lee, Sharon Kim, Kyungmin Bae and Peter Olveczky</span>
<span class="ref"> International Conference on Computer Aided Verification (CAV)</span>
<span class="year">2021</span>
</li>
<li>
<span class="title">Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation</span>
<span class="author">Kyungmin Bae and Jia Lee</span>
<span class="ref">ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)</span>
<span class="year">2019</span>
</li>
<li>
<span class="title">Modular SMT-Based Analysis of Nonlinear Hybrid Systems</span>
<span class="author">Kyungmin Bae and Sicun Gao</span>
<span class="ref">International Conference on
Formal Methods in Computer-Aided Design (FMCAD)</span>
<span class="year">2017</span>
</li>
<li>
<span class="title">Guarded Terms for Rewriting modulo SMT</span>
<span class="author">Kyungmin Bae and Camilo Rocha</span>
<span class="ref">International Conference on Formal Aspects of Component Software (FACS)</span>
<span class="year">2017</span>
<!--span style="color:blue; font-weight:bold;">(Best Paper Award)</span-->
</li>
<li>
<span class="title">SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems</span>
<span class="author">Kyungmin Bae, Peter Olveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke</span>
<span class="ref">ACM International Conference on Hybrid Systems: Computation and Control (HSCC)</span>
<span class="year">2016</span>
</li>
<li>
<span class="title">A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control</span>
<span class="author">Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae</span>
<span class="ref"> International Symposium on NASA Formal Methods (NFM)</span>
<span class="year">2016</span>
</li>
<li>
<span class="title">A Term Rewriting Approach to Analyze High Level Petri Nets</span>
<span class="author">Xudong He, Reng Zeng, Su Liu, Zhuo Sun, Kyungmin Bae</span>
<span class="ref"> International Symposium on Theoretical Aspects of Software Engineering (TASE)</span>
<span class="year">2016</span>
</li>
<li>
<span class="title">Predicate Abstraction of Rewrite Theories</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref"> Joint International Conference on Rewriting and Typed Lambda Calculi (RTA-TLCA)</span>
<span class="year">2014</span>
</li>
<li>
<span class="title">Definition, Semantics, and Analysis of Multirate Synchronous AADL</span>
<span class="author">Kyungmin Bae, Peter Olveczky, and José Meseguer</span>
<span class="ref">International Symposium on Formal Methods (FM)</span>
<span class="year">2014</span>
</li>
<li>
<span class="title">Abstract Logical Model Checking of Infinite-State Systems Using Narrowing</span>
<span class="author">Kyungmin Bae, Santiago Escobar and José Meseguer</span>
<span class="ref">International Conference on Rewriting Techniques and Applications (RTA)</span>
<span class="year">2013</span>
</li>
<li>
<span class="title">The SynchAADL2Maude Tool</span>
<span class="author">Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem</span>
<span class="ref">International Conference on Fundamental Approaches to Software Engineering (FASE)</span>
<span class="year">2012</span>
</li>
<li>
<span class="title">Formal Patterns for Multi-Rate Distributed Real-Time Systems</span>
<span class="author">Kyungmin Bae, José Meseguer, and Peter Olveczky</span>
<span class="ref"> International Symposium on Formal Aspects of Component Software (FACS)</span>
<span class="year">2012</span>
</li>
<li>
<span class="title">State/Event-based LTL Model Checking under Parametric Generalized Fairness</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref"> International Conference on Computer Aided Verification (CAV)</span>
<span class="year">2011</span>
</li>
<li>
<span class="title">Synchronous AADL and its Formal Analysis in Real-Time Maude</span>
<span class="author">Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and José Meseguer</span>
<span class="ref">International Conference on Formal Engineering Methods (ICFEM)</span>
<span class="year">2011</span>
</li>
<li>
<span class="title">Verifying Ptolemy II Discrete-Event Models using Real-Time Maude</span>
<span class="author">Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng and Stavros Tripakis</span>
<span class="ref">International Conference on Formal Engineering Methods (ICFEM)</span>
<span class="year">2009</span>
<!--span>Invited to Science of Computer Programming as the best ICFEM 2009 papers</span-->
</li>
</ol>
</div>
<div>
<h3> Journal Articles </h3>
<ol>
<li>
<span class="title">Narrowing and heuristic search for symbolic reachability analysis of concurrent object-oriented systems</span>
<span class="author">Byeongjee Kang and Kyungmin Bae</span>
<span class="ref">Science of Computer Programming 235: 103097</span>
<span class="year">2024</span>
</li>
<li>
<span class="title">Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving</span>
<span class="author">Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Olveczky, Laure Petrucci, and Fredrik Romming</span>
<span class="ref">Science of Computer Programming 233: 103074</span>
<span class="year">2024</span>
</li>
<li>
<span class="title">Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL</span>
<span class="author">Jaehun Lee, Kyungmin Bae, Peter Olveczky, Sharon Kim, and Minseok Kang</span>
<span class="ref">Software Tools for Technology Transfer 24: 911–948</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">Symbolic State Space Reduction with Guarded Terms for Rewriting Modulo SMT</span>
<span class="author">Kyungmin Bae and Camilo Rocha</span>
<span class="ref">Science of Computer Programming 178: 20-42 </span>
<span class="year">2019</span>
</li>
<li>
<span class="title">Designing and Verifying Distributed Cyber-Physical Systems using Multirate PALS: An Airplane Turning Control System Case Study</span>
<span class="author">Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky</span>
<span class="ref">Science of Computer Programming 103:13-50 </span>
<span class="year">2015</span>
</li>
<li>
<span class="title">Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness</span>
<span class="author">Kyungmin Bae, and José Meseguer</span>
<span class="ref">Science of Computer Programming 99</span>
<span class="year">2015</span>
</li>
<li>
<span class="title">Formal Patterns for Multirate Distributed Real-Time Systems (extended version)</span>
<span class="author">Kyungmin Bae, José Meseguer, and Peter Olveczky</span>
<span class="ref">Science of Computer Programming 91, Part A</span>
<span class="year">2014</span>
</li>
<li>
<span class="title">Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude</span>
<span class="author">Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis,</span>
<span class="ref"> Science of Computer Programming 77(12)</span>
<span class="year">2012</span>
</li>
</ol>
</div>
<div>
<h3> Workshop Papers </h3>
<ol>
<li>
<span class="title">Formal Model Engineering of Synchronous CPS Designs in AADL</span>
<span class="author">Kyungmin Bae and Peter Olveczky</span>
<span class="ref">2nd ADEPT workshop: AADL by its practitioners (ADEPT)</span>
<span class="year">2023</span>
</li>
<li>
<span class="title">Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata</span>
<span class="author">Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, Fredrik Rømming</span>
<span class="ref">ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search</span>
<span class="author">Byeongjee Kang, Kyungmin Bae</span>
<span class="ref">ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">Bounded Model Checking of PLC ST Programs using Rewriting Modulo SMT</span>
<span class="author">Jaeseo Lee, Sangki Kim, Kyungmin Bae</span>
<span class="ref">ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">Maude-SE: a Tight Integration of Maude and SMT Solvers</span>
<span class="author">Geunyeol Yu and Kyungmin Bae</span>
<span class="ref">International Workshop on Rewriting Logic and its Applications (WRLA)</span>
<span class="year">2020</span>
</li>
<li>
<span class="title">An Architecture for Hybrid Planning and Execution</span>
<span class="author">Robert P. Goldman, Dan Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae</span>
<span class="ref">AAAI-16 Workshop on Planning for Hybrid Systems</span>
<span class="year">2016</span>
</li>
<li>
<span class="title">SMT Encoding of Hybrid Systems in dReal</span>
<span class="author">Kyungmin Bae, Soonho Kong, and Sicun Gao</span>
<span class="ref">International Workshop on Applied veRification for Continuous and Hybrid Systems</span>
<span class="year">2015</span>
</li>
<li>
<span class="title">Hybrid Multirate PALS</span>
<span class="author">Kyungmin Bae and Peter C. Olveczky</span>
<span class="ref">Logic, Rewriting, and Concurrency</span>
<span class="year">2015</span>
</li>
<li>
<span class="title">Infinite-State Model Checking of LTLR Formulas Unsing Narrowing</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref">International Workshop on Rewriting Logic and its Applications (WRLA)</span>
<span class="year">2014</span>
</li>
<li>
<span class="title">PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude</span>
<span class="author">Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Olveczky</span>
<span class="ref">International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)</span>
<span class="year">2012</span>
</li>
<li>
<span class="title">Model Checking LTLR Formulas under Localized Fairness</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref">International Workshop on Rewriting Logic and its Applications (WRLA)</span>
<span class="year">2012</span>
</li>
<li>
<span class="title">Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models</span>
<span class="author">Kyungmin Bae and Peter C. Olveczky</span>
<span class="ref">International Workshop on Rewriting Techniques for Real-Time Systems</span>
<span class="year">2010</span>
</li>
<li>
<span class="title">The Linear Temporal Logic of Rewriting Maude Model Checker</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref">International Workshop on Rewriting Logic and its Applications (WRLA)</span>
<span class="year">2010</span>
</li>
<li>
<span class="title">A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting</span>
<span class="author">Kyungmin Bae and José Meseguer</span>
<span class="ref">International Workshop on Rule-Based Programming</span>
<span class="year">2008</span>
</li>
</ol>
</div>
<div class="column row">
<h3>Books</h3>
<ul>
<li>
<span class="title">Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022, Revised Selected Papers</span>
<span class="author">Kyungmin Bae</span>
<span class="ref">Lecture Notes in Computer Science 13252, Springer</span>
<span class="year">2022</span>
</li>
<li>
<span class="title">FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020</span>
<span class="author">Kyungmin Bae, Domenico Bianculli, Stefania Gnesi, and Nico Plat</span>
<span class="ref">ACM</span>
<span class="year">2020</span>
</li>
<li>
<span class="title">Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings</span>
<span class="author">Kyungmin Bae and Peter Olveczky</span>
<span class="ref">Lecture Notes in Computer Science 11222, Springer</span>
<span class="year">2018</span>
</li>
<li>
<span class="title">Rewriting-based model checking methods</span>
<span class="ref">Kyungmin Bae, PhD Dissertation, Department of Computer Science, University of Illinois at Urbana-Champaign, USA</span>
<span class="year">2014</span>
<span>(<a href="http://hdl.handle.net/2142/50553">link</a>)</span>
</li>
</ul>
</div>
</div>
</section>
<section id="bio" data-magellan-target="bio">
<div class="column row">
<h2>Education</h2>
<ul>
<li> 2007.08 ~ 2014.08 : Ph.D. in Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL (Advisor: José Meseguer).
<li> 2000.03 ~ 2004.03 : B.S. in Computer Science and Mathematics (double major), KAIST (summa cum laude).
</ul>
</div>
<div class="column row">
<h2>Employment</h2>
<ul>
<li> 2016.02 ~ present : Assistant/Associate professor at POSTECH </li>
<li> 2015.07 ~ 2016.01 : Postdoctoral researcher in the Computer Science Laboratory at SRI International </li>
<li> 2014.09 ~ 2015.07 : Postdoctoral researcher in Edmund Clarke's group at Carnegie Mellon University </li>
<li> 2010.05 ~ 2010.08 : International Fellow in the Computer Science Laboratory at SRI International </li>
<li> 2009.05 ~ 2009.08 : International Fellow in the Computer Science Laboratory at SRI International </li>
<li> 2004.03 ~ 2007.06 : Lieutenant, Republic of Korea Air force (mandatory military service) </li>
</ul>
</div>
<div class="column row">
<h2>Honors and Awards</h2>
<ul>
<li>Best Paper Award, FACS, 2017</li>
<li>Feng Chen Memorial Award, UIUC, 2013</li>
<li>Chirag Foundation Fellowship, UIUC, 2007 ~ 2008</li>
<li>Doctoral Study Scholarship, Korea Foundation for Advanced Studies, 2007</li>
<!--li>Merit-based Scholarship, KAIST, 2000 ~ 2003</li-->
</ul>
</div>
</section>
<div id="pgend"></div>
<script src="js/jquery.min.js"></script>
<script src="js/what-input.min.js"></script>
<script src="js/foundation.min.js"></script>
<script>$(document).foundation();</script>
</body>
</html>