| 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 | 69 | 2013 |
| Model checking linear temporal logic of rewriting formulas under localized fairness K Bae, J Meseguer Science of Computer Programming 99, 193-234, 2015 | 45 | 2015 |
| 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 | 43 | 2012 |
| 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 | 31 | 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 |
| 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 | 28 | 2009 |
| 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 | 26 | 2012 |
| The linear temporal logic of rewriting Maude model checker K Bae, J Meseguer International Workshop on Rewriting Logic and its Applications, 208-225, 2010 | 26 | 2010 |
| Infinite-state model checking of LTLR formulas using narrowing K Bae, J Meseguer International Workshop on Rewriting Logic and its Applications, 113-129, 2014 | 22 | 2014 |
| Formal patterns for multirate distributed real-time systems K Bae, J Meseguer, PC Ölveczky Science of Computer Programming 91, 3-44, 2014 | 18 | 2014 |
| Definition, semantics, and analysis of multirate synchronous AADL K Bae, PC Ölveczky, J Meseguer International Symposium on Formal Methods, 94-109, 2014 | 17 | 2014 |
| The synchaadl2maude tool K Bae, PC Ölveczky, J Meseguer, A Al-Nayeem International Conference on Fundamental Approaches to Software Engineering …, 2012 | 17 | 2012 |
| 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 | 15 | 2011 |
| 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 | 12 | 2016 |
| Bounded model checking of signal temporal logic properties using syntactic separation K Bae, J Lee Proceedings of the ACM on Programming Languages 3 (POPL), 1-30, 2019 | 11 | 2019 |
| 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 | 11 | 2016 |
| Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models K Bae, PC Ölveczky arXiv preprint arXiv:1009.4261, 2010 | 11 | 2010 |
| 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 | 10* | 2013 |
| Guarded terms for rewriting modulo SMT K Bae, C Rocha International Conference on Formal Aspects of Component Software, 78-97, 2017 | 8 | 2017 |
