Abstract logical model checking of infinite-state systems using narrowing K Bae, S Escobar, J Meseguer 24th International Conference on Rewriting Techniques and Applications (RTA …, 2013 | 57 | 2013 |

A rewriting-based model checker for the linear temporal logic of rewriting K Bae, J Meseguer Electronic Notes in Theoretical Computer Science 290, 19-36, 2012 | 42 | 2012 |

Model checking linear temporal logic of rewriting formulas under localized fairness K Bae, J Meseguer Science of Computer Programming 99, 193-234, 2015 | 36 | 2015 |

Synchronous AADL and its formal analysis in Real-Time Maude K Bae, PC Ölveczky, A Al-Nayeem, J Meseguer International Conference on Formal Engineering Methods, 651-667, 2011 | 31 | 2011 |

The linear temporal logic of rewriting Maude model checker K Bae, J Meseguer International Workshop on Rewriting Logic and its Applications, 208-225, 2010 | 28 | 2010 |

Verifying ptolemy ii discrete-event models using real-time maude K Bae, PC Ölveczky, TH Feng, S Tripakis International Conference on Formal Engineering Methods, 717-736, 2009 | 27 | 2009 |

Designing and verifying distributed cyber-physical systems using Multirate PALS: An airplane turning control system case study K Bae, J Krisiloff, J Meseguer, PC Ölveczky Science of computer programming 103, 13-50, 2015 | 26 | 2015 |

Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude K Bae, PC Ölveczky, TH Feng, EA Lee, S Tripakis Science of Computer Programming 77 (12), 1235-1271, 2012 | 24 | 2012 |

Infinite-state model checking of LTLR formulas using narrowing K Bae, J Meseguer International Workshop on Rewriting Logic and its Applications, 113-129, 2014 | 19 | 2014 |

Formal patterns for multirate distributed real-time systems K Bae, J Meseguer, PC Ölveczky Science of Computer Programming 91, 3-44, 2014 | 17 | 2014 |

Model checking LTLR formulas under localized fairness K Bae, J Meseguer International Workshop on Rewriting Logic and its Applications, 99-117, 2012 | 16 | 2012 |

State/event-based LTL model checking under parametric generalized fairness K Bae, J Meseguer International Conference on Computer Aided Verification, 132-148, 2011 | 16 | 2011 |

Definition, semantics, and analysis of Multirate Synchronous AADL K Bae, PC Ölveczky, J Meseguer International Symposium on Formal Methods, 94-109, 2014 | 15 | 2014 |

The synchaadl2maude tool K Bae, PC Ölveczky, J Meseguer, A Al-Nayeem International Conference on Fundamental Approaches to Software Engineering …, 2012 | 15 | 2012 |

PALS-based analysis of an airplane multirate control system in Real-Time Maude K Bae, J Krisiloff, J Meseguer, PC Ölveczky arXiv preprint arXiv:1301.0038, 2013 | 11* | 2013 |

Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models K Bae, PC Ölveczky arXiv preprint arXiv:1009.4261, 2010 | 11 | 2010 |

SMT-based analysis of virtually synchronous distributed hybrid systems K Bae, PC Ölveczky, S Kong, S Gao, EM Clarke Proceedings of the 19th International Conference on Hybrid Systems …, 2016 | 9 | 2016 |

A hybrid architecture for correct-by-construction hybrid planning and control RP Goldman, D Bryce, MJS Pelican, DJ Musliner, K Bae NASA Formal Methods Symposium, 388-394, 2016 | 8 | 2016 |

Guarded terms for rewriting modulo SMT K Bae, C Rocha International Conference on Formal Aspects of Component Software, 78-97, 2017 | 7 | 2017 |

Predicate abstraction of rewrite theories K Bae, J Meseguer Rewriting and Typed Lambda Calculi, 61-76, 2014 | 7 | 2014 |