@ARTICLE{interaspect-journal, @ARTICLE{interaspect-journal, AUTHOR = "J. Seyster and K. Dixit and X. Huang and R. Grosu and K. Havelund and S. A. Smolka and S. D. Stoller and E. Zadok", TITLE = "{InterAspect}: Aspect-Oriented Instrumentation with {GCC}", JOURNAL = "Formal Methods in System Design", MONTH = "August", YEAR = 2012, PUBLISHER = "Springer", URL = "\url{http://link.springer.com/article/10.1007%2Fs10703-012-0171-3}" }

@ARTICLE{stoller11reachability, AUTHOR = "S. D. Stoller and P. Yang and M. Gofman and C. R. Ramakrishnan", TITLE = "Symbolic Reachability Analysis for Parameterized Administrative Role Based Access Control", JOURNAL = "Computers \& Security", VOLUME = 30, NUMBER = "2-3", PAGES = "148-164", MONTH = "March-May", YEAR = 2011, }

@ARTICLE{huang11smco, AUTHOR = "X. Huang and J. Seyster and S. Callanan and K. Dixit and R. Grosu and S. A. Smolka and S. D. Stoller and E. Zadok", TITLE = "Software Monitoring with Controllable Overhead", JOURNAL = "International Journal on Software Tools for Technology Transfer (STTT)", VOLUME = 14, NUMBER = 3, YEAR = 2012, PAGES = "327--347" PUBLISHER = "Springer", }

@ARTICLE{bartocci08bmc, AUTHOR = "E. Bartocci and F. Corradini and E. Entcheva and R. Grosu and S. A. Smolka", TITLE = "{CellExcite}: An Efficient Simulation Environment for Excitable Cells", JOURNAL = "BMC Bioinformatics", YEAR = 2008, PUBLISHER = "BioMed Central", VOLUME = 9, NUMBER = "Suppl. 2", }

@ARTICLE{ye08iet, AUTHOR = "P.Ye, E. Entcheva, S. A. Smolka, and R. Grosu", TITLE = "Modeling Excitable Cells Using Cycle-Linear Hybrid-Automata", JOURNAL = "IET Systems Biology", YEAR = 2008, VOLUME = 2, NUMBER = 1, PAGES = "24--32" }

@ARTICLE{basu07tosem, AUTHOR = "S. Basu and S. A. Smolka", TITLE = "Model checking the Java metalocking algorithm", JOURNAL = "ACM Trans. Softw. Eng. Methodol.", VOLUME = 16, ISSUE = 3, MONTH = "July", YEAR = 2007, ISSN = "1049-331X", ARTICLENO = "12", URL = "http://doi.acm.org/10.1145/1243987.1243990", DOI = "http://doi.acm.org/10.1145/1243987.1243990", ACMID = "1243990", PUBLISHER = "ACM", ADDRESS = "New York, NY, USA", KEYWORDS = "Java, XMC, metalocking, monitor queues, mutual exclusion, synchronized methods", }

@INPROCEEDINGS{fm2012barringer, AUTHOR = "H. Barringer and Y. Falcone and K. Havelund and G. Reger and D. Rydeheard", TITLE = "Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors", BOOKTITLE = "FM 2012: Formal Methods", YEAR = "2012", MONTH = "August", PAGES = "68-84m", URL = "http://dx.doi.org/10.1007/978-3-642-32759-9_9", }

@INPROCEEDINGS{rv12arv, AUTHOR = "E. Bartocci and R. Grosu and A. Karmarkar and S. A. Smolka and S. D. Stoller and E. Zadok and J. Seyster", TITLE = "Adaptive runtime verification", BOOKTITLE = "Proc.\ 3rd International Conference on Runtime Verification (RV'12)", YEAR = 2012, MONTH = "September", ADDRESS = "Istanbul, Turkey", }

@INPROCEEDINGS{xu12algorithms, AUTHOR = "Z. Xu and S. D. Stoller", TITLE = "Algorithms for Mining Meaningful Roles", BOOKTITLE = "Proceedings of the 17th ACM Symposium on Access Control Models and Technologies (SACMAT)", YEAR = 2012, PUBLISHER = "ACM Press" }

@INPROCEEDINGS{gorbovitski12composing, AUTHOR = "M. Gorbovitski and Y. A. Liu and S. D. Stoller and T. Rothamel", TITLE = "Composing transformations for instrumentation and optimization", YEAR = 2012, MONTH = "January", BOOKTITLE = "Proc.\ 2012 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM)", PUBLISHER = "ACM Press" }

@INPROCEEDINGS{ica3pp11redflag, AUTHOR = "J. Seyster and P. Radhakrishnan and S. Katoch and A. Duggal and S. D. Stoller and E. Zadok", TITLE = "Redflag: A framework for analysis of kernel-level concurrency", BOOKTITLE = "Proc. of the 11th International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP'11)", YEAR = 2011, MONTH = "October", ADDRESS = "Melbourne, Australia", }

@INPROCEEDINGS{rv11stoller, AUTHOR = "S. D. Stoller and E. Bartocci and J. Seyster and R. Grosu and K. Havelund and S. A. Smolka and E. Zadok", TITLE = "Runtime verification with state estimation", BOOKTITLE = "Proc. of the 2nd International Conference on Runtime Verification (RV'11)", YEAR = 2011, MONTH = "September", ADDRESS = "San Fransisco, CA", NOTE = "(Won best paper award)", }

@INPROCEEDINGS{grosu11cardiac, AUTHOR = "R. Grosu and G. Batt and F. H. Fenton and J. Glimm and C. Le Guernic and S. A. Smolka and E. Bartocci", BOOKTITLE = "From Cardiac Cells to Genetic Regulatory Networks", SERIES = "CAV", YEAR = 2011, PAGES = "396-411", ADDRESS = "Snowbird, Utah", }

@INPROCEEDINGS{systor11energy, TITLE = "On the Energy Consumption and Performance of Systems Software", AUTHOR = "Z. Li and R. Grosu and P. Sehgal and S. A. Smolka and S. D. Stoller and E. Zadok", BOOKTITLE = "Proceedings of the 4th Israeli Experimental Systems Conference (ACM SYSTOR '11)", YEAR = 2011, MONTH = "May/June", ADDRESS = "Haifa, Israel", PUBLISHER = "ACM", }

@INPROCEEDINGS{bartocci11repair, AUTHOR = "E. Bartocci and R. Grosu and P. Katsaros and C. R. Ramakrishnan and S. A. Smolka", TITLE = "Model repair for probabilistic systems", BOOKTITLE = "Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems", SERIES = "TACAS'11/ETAPS'11", YEAR = "2011", ISBN = "978-3-642-19834-2", LOCATION = {Saarbr\"{u}cken, Germany}, PAGES = "326--340", NUMPAGES = "15", URL = "http://dl.acm.org/citation.cfm?id=1987389.1987428", ACMID = "1987428", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin, Heidelberg", KEYWORDS = "model repair, nonlinear programming, probabilistic model checking", }

@INPROCEEDINGS{barringer11flightrules, AUTHOR = "H. Barringer and K. Havelund", TITLE = "Checking Flight Rules with {TraceContract}: Application of a {Scala} {DSL} for Trace Analysis", BOOKTITLE = "Proceedings of Scala Days 2011", YEAR = "2011", LOCATION = "Stanford, CA", }

@INPROCEEDINGS{barringer11tracecontract, AUTHOR = "H. Barringer and K. Havelund", TITLE = "{TraceContract}: a {Scala} {DSL} for trace analysis", BOOKTITLE = "Proceedings of the 17th international conference on Formal methods", SERIES = "FM'11", YEAR = "2011", ISBN = "978-3-642-21436-3", LOCATION = "Limerick, Ireland", PAGES = "57--72", NUMPAGES = "16", URL = "http://dl.acm.org/citation.cfm?id=2021296.2021306", ACMID = "2021306", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin, Heidelberg", }

@INPROCEEDINGS{stoller10trust, AUTHOR = "Scott D. Stoller", TITLE = "Trust Management for Web Services", BOOKTITLE = "Proc.\ 6th International Conference on Network and Service Management (CNSM)", MONTH= "October", YEAR= 2010, PUBLISHER = "IEEE Press", PAGES = "262-265" }

@INPROCEEDINGS{interaspect, AUTHOR = "J. Seyster and K. Dixit and X. Huang and R. Grosu and K. Havelund and S. A. Smolka and S. D. Stoller and E. Zadok", TITLE = "Aspect-Oriented Instrumentation with {GCC}", BOOKTITLE = "Proc. of the 1st International Conference on Runtime Verification (RV 2010)", SERIES = "Lecture Notes in Computer Science", PUBLISHER = "Springer", MONTH = "November", YEAR = 2010, }

@INPROCEEDINGS{alexiou10kaminksy, AUTHOR = "N. Alexiou and T. Deshpande and S. Basagiannis and S. A. Smolka and P. Katsaros", TITLE = "Formal Analysis of the {Kaminsky} {DNS} Cache-Poisoning Attack Using Probabilistic Model Checking", BOOKTITLE = "Proceedings of the 2010 IEEE 12th International Symposium on High-Assurance Systems Engineering", SERIES = "HASE '10", YEAR = "2010", ISBN = "978-0-7695-4292-8", PAGES = "94--103", NUMPAGES = "10", URL = "http://dx.doi.org/10.1109/HASE.2010.25", DOI = "http://dx.doi.org/10.1109/HASE.2010.25", ACMID = "1909810", PUBLISHER = "IEEE Computer Society", ADDRESS = "Washington, DC, USA", KEYWORDS = "DNS, Cache Poisoning, Probabilistic Model Checking", }

@INPROCEEDINGS{huang10nfm, AUTHOR = "Xiaowan Huang and Anu Singh and Scott A. Smolka", TITLE = "Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol", BOOKTITLE = "Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215", EDITOR = "C{\'e}sar Mu{\~{n}}oz", ORGANIZATION = "NASA", ADDRESS = "Langley Research Center, Hampton VA 23681-2199, USA", PAGES = "77--86", MONTH = "April", YEAR = "2010" }

@INPROCEEDINGS{yang09ifm, AUTHOR = "Z. Yang and B. Al-Rawi and K. Sakallah and X. Huang and S. Smolka and R. Grosu", TITLE = "Dynamic Path Reduction for Software Model Checking", BOOKTITLE = "Proceedings of the 7th International Conference on Integrated Formal Methods", SERIES = "IFM '09", YEAR = 2009, ISBN = "978-3-642-00254-0", LOCATION = "D\"{u}sseldorf, Germany", PAGES = "322--336", NUMPAGES = "15", URL = "http://dx.doi.org/10.1007/978-3-642-00255-7_22", DOI = "http://dx.doi.org/10.1007/978-3-642-00255-7_22", ACMID = "1506960", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin, Heidelberg", }

@INPROCEEDINGS{unnikrishnan09parametric, AUTHOR = "Leena Unnikrishnan and Scott D. Stoller", TITLE = "Parametric Heap Usage Analysis for Functional Programs", BOOKTITLE = "Proceedings of the 8th International Symposium on Memory Management (ISMM)", YEAR = 2009, PUBLISHER = "ACM Press" }

@INPROCEEDINGS{chen09have, AUTHOR = "Qichang Chen and Liqiang Wang and Zijiang Yang and Scott D. Stoller", TITLE = "{HAVE}: Integrated Dynamic and Static Analysis for Atomicity Violations", BOOKTITLE = "Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering (FASE)", YEAR = 2009, PUBLISHER = "Springer-Verlag", SERIES = "Lecture Notes in Computer Science", VOLUME = "5503", PAGES = "425-439" }

@INPROCEEDINGS{grosu09hscc, AUTHOR = "R. Grosu", TITLE = "Finite Automata as Time-Inv Linear Systems Observability, Reachability and More", BOOKTITLE = "Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control", SERIES = "HSCC '09", YEAR = 2009, ISBN = "978-3-642-00601-2", LOCATION = "San Francisco, CA", PAGES = "194--208", NUMPAGES = "15", URL = "http://dx.doi.org/10.1007/978-3-642-00602-9_14", DOI = "http://dx.doi.org/10.1007/978-3-642-00602-9_14", ACMID = "1538203", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin, Heidelberg", }

@INPROCEEDINGS{gorbovitski08efficient, AUTHOR = "Michael Gorbovitski and Tom Rothamel and Yanhong A. Liu and Scott D. Stoller", TITLE = "Efficient Runtime Invariant Checking: A Framework and Case Study", BOOKTITLE = "Proceedings of the 6th International Workshop on Dynamic Analysis (WODA 2008)", PUBLISHER = "ACM Press", YEAR = 2008 }

@INPROCEEDINGS{callanan08ngs, AUTHOR = "S. Callanan and D. J. Dean and M. Gorbovitski and R. Grosu and J. Seyster and S. A. Smolka and S. D. Stoller and E. Zadok", TITLE = "Software Monitoring with Bounded Overhead", BOOKTITLE = "Proceedings of the 2008 NSF Next Generation Software Workshop, in conjunction with the 2008 International Parallel and Distributed Processing Symposium (IPDPS 2008)", YEAR = 2008, MONTH = "April", ADDRESS = "Miami, FL", }

@INPROCEEDINGS{grosu08hscc, AUTHOR = "R. Grosu and E. Bartocci and F. Corradini and E. Entcheva and S. A. Smolka and A. Wasilewska", TITLE = "Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes", BOOKTITLE = "Proceedings of the 11th international workshop on Hybrid Systems: Computation and Control", SERIES = "HSCC '08", YEAR = 2008, ISBN = "978-3-540-78928-4", LOCATION = "St. Louis, MO, USA", PAGES = "229--243", NUMPAGES = "15", URL = "http://dx.doi.org/10.1007/978-3-540-78929-1_17", DOI = "http://dx.doi.org/10.1007/978-3-540-78929-1_17", ACMID = "1423051", PUBLISHER = "Springer-Verlag", ADDRESS = "Berlin, Heidelberg", }

@INPROCEEDINGS{traeger08darc, AUTHOR = "A. Traeger and I. Deras and E. Zadok", TITLE = "{DARC}: Dynamic Analysis of Root Causes of Latency Distributions", PAGES = "277--288", BOOKTITLE = "Proceedings of the 2008 International Conference on Measurement and Modeling of Computer Systems (SIGMETRICS 2008)", ADDRESS = "Annapolis, MD", MONTH = "June", YEAR = 2008, PUBLISHER = "ACM", }

@INPROCEEDINGS{callanan07gccsummit, AUTHOR = "S. Callanan and D. J. Dean and E. Zadok", TITLE = "Extending {GCC} with Modular {GIMPLE} Optimizations", BOOKTITLE = "Proceedings of the 2007 GCC Developers' Summit", ADDRESS = "Ottawa, Canada", MONTH = "July", YEAR = 2007, }

@INPROCEEDINGS{callanan07memcov, AUTHOR = "S. Callanan and R. Grosu and J. Seyster and S.\ A.\ Smolka and E. Zadok", TITLE = "Model Predictive Control for Memory Profiling", BOOKTITLE = "Proceedings of the 2007 NSF Next Generation Software Workshop, in conjunction with the 2007 International Parallel and Distributed Processing Symposium (IPDPS 2007)", YEAR = 2007, MONTH = "March", ADDRESS = "Long beach, CA", }

@PHDTHESIS{redflag-dissertation, AUTHOR = "J. Seyster", TITLE = "Runtime Verification of Kernel-Level Concurrency Using Compiler-Based Instrumentation", SCHOOL = "Computer Science Department, Stony Brook University", YEAR = "2012", MONTH = "December", NOTE = "Technical Report FSL-12-05, \url{www.fsl.cs.sunysb.edu/docs/jseyster-dissertation/redflag.pdf}", }

@PHDTHESIS{xiaowan-dissertation, AUTHOR = "X. Huang", TITLE = "Compiler-Assisted Software Model Checking and Monitoring", SCHOOL = "Computer Science Department, Stony Brook University", YEAR = 2010, MONTH = "December", }

@PHDTHESIS{callanan09phdthesis, AUTHOR = "S. Callanan", TITLE = "Flexible Debugging with Controllable Overhead", YEAR = "2009", MONTH = "August", NOTE = "Technical Report FSL-09-01, \url{http://www.fsl.cs.sunysb.edu/docs/callanan09phdthesis/callanan09phdthesis.pdf}", SCHOOL = "Computer Science Department, Stony Brook University", }