• Medical Cyber-Physical Systems
• Safe AI and Autonomy
• Security, Trust Management, and Policy Modeling
• Real-Time Resource Management: Compositional Scheduling, Virtualization, Communication
• Real-Time Embedded Systems: Model-Based Development, Programming, Testing
• Formal Methods in Safety-Critical Systems (Real-Time, Hybrid, and Probabilistic Systems)
• Runtime Monitoring and Checking (a la Runtime Verification)
• Position and Workshop Summary Papers

Medical Cyber-Physical Systems

• Raproto: An Open Source Platform for Rapid Prototyping of Wearable Medical Devices. Amanda Watson, Hyonyoung Choi, Insup Lee, and James Weimer. Proceedings of the 12th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Nashville, TN, May 2021.
• Characterizing Glycemic Control and Sleep in Adults with Long-Standing Type 1 Diabetes and Hypoglycemia Unawareness Initiating Hybrid Closed Loop Insulin Delivery. Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. Journal of Diabetes Research, Vol 2021, Num 6611064, February 2021.
• Methods, systems, and computer readable media for physiology parameter-invariant meal detection. Sanjian Chen, James Erich Weimer, and Insup Lee, U.S. Patent No. 10,792,423, October 6, 2020.
• Reducing Pulse Oximetry False Alarms Without Missing Life-Threatening Events. Hung Nguyen, Sooyong Jang, Radoslav Ivanov, Christopher P. Bonafide, James Weimer, and Insup Lee. In Proceedings of IEEE/ACM Conference on Connected Health: Applications, Systems and Engineering Technologies (CHASE 2018), Washington, D.C., USA, September 2018.
• OpenICE-lite: Towards a Connectivity Platform for the Internet of Medical Things. Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, and Insup Lee. In Proceedings of IEEE ISORC 2018, Singapore, May 2018.
• Context-Aware Detection in Medical Cyber-Physical Systems. Radoslav Ivanov, James Weimer, and Insup Lee. In Proceedings of 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2018), Porto, Portugal, April 2018.
• Continuous Glucose Monitoring for Hypoglycemia Avoidance and Glucose Counterregulation in Long-Standing Type 1 Diabetes. Michael R. Rickels, Amy J. Peleckis, Cornelia Dalton-Bakes, Joseph R. Naji, Nina Ran, Huong-Lan Nguyen, Shannon O'Brien, Sanjian Chen,Insup Lee, and Mark H. Schutta. In The Journal of Clinical Endocrinology & Metabolism, Volume 103, Issue 1, pp. 105-114, January 2018, published November 2017.
• Parameter-Invariant Monitor Design for Cyber Physical Systems. James Weimer, Radoslav Ivanov, Sanjian Chen, Alexander Roederer, Oleg Sokolsky, and Insup Lee. In Proceedings of the IEEE, Volume 106, Issue 1 pp.71-92, January 2018, published September 2017.
• Modeling Opportunities in mHealth Cyber-Physical Systems. Wendy Nilsen, Emre Ertin, Eric B. Hekler, Santosh Kumar, Insup Lee, Rahul Mangharam, Misha Pavel, James M. Rehg, William T. Riley, Daniel E. Rivera, Donna Spruijt-Metz. In Mobile Health - Sensors, Analytic Methods, and Applications. 2017. pp 443-453
• Transmission delay performance in telemedicine: A case study. Gang Wang, Shan Lin, Margaret Mullen-Fortino, Oleg Sokolsky, Insup Lee. In Proceedings of 39th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC 2017), Jeju Island, Korea from, July 2017.
• Data-driven Adaptive Safety Monitoring using Virtual Subjects in Medical Cyber-Physical Systems: A Glucose Control Case Study. Sanjian Chen, Oleg Sokolsky, James Weimer, and Insup Lee. In Journal of Computer Science and Engineering, Volume 10, Num.3, pp.75-84, September 2016 (Open Access).
• Clinician-in-the-Loop Annotation of ICU Bedside Alarm Data. Alexander Roederer, Joseph Dimartino, Jacob Gutsche, Margaret Mullen-Fortino, Sachin Shah, C. William Hanson III, and Insup Lee. In Proceedings of First IEEE Conference on Connected Health Applications, Systems and Engineering Technologies (IEEE CHASE 2016), Washington, DC, June 2016.
• Cloud-Based Secure Logger for Medical Devices. Hung Nguyen, Bipeen Acharya, Radoslav Ivanov, Andreas Haeberlen, Linh T.X. Phan, Oleg Sokolsky, Jesse Walker, James Weimer, C. William Hanson III, and Insup Lee. In Proceedings of IEEE First International Conference on Connected Health: Applications, Systems and Engineering Technologies (CHASE 2016), Washington, DC, USA, June 2016.
• Estimation of Blood Oxygen Content Using Context-Aware Filtering. Radoslav Ivanov, Nikolay Atanasov, James Weimer, Miroslav Pajic, Allan Simpao, Mohamed Rehman, George Pappas and Insup Lee. In Proceedings of 7th International Conference on Cyber-Physical Systems (ICCPS 2016), Vienna, Austria, April 2016.
• Protecting interoperable clinical environment with authentication. Liang Cheng, Zhangtan Li, Yi Zhang, Yang Zhang, Insup Lee. In Proceedings of Medical CPS workshop 2016, Vienna, Austria, April 2016. Also published in SIGBED Review Vol. 14, Num. 2, February 2017
• Representation of Confidence in Assurance Cases using the Beta Distribution. Lian Duan, Sanjai Rayadurgam, Mats Heimdahl, Oleg Sokolsky, and Insup Lee. In Proceedings of IEEE High Assurance Systems Engineering Symposium (HASE 2016), Orlando, Florida, USA, January 2016.
• Platform-Specific Code Generation from Platform-Independent Timed Models. BaekGyu Kim, Lu Feng, Oleg Sokolsky and Insup Lee. In IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
• Parameter-Invariant Design of Medical Alarms. James Weimer, Radoslav Ivanov, Alexander Roederer, Sanjian Chen, and Insup Lee. In IEEE Design & Test , Volume 32, Issue 5, pp 9-16, October 2015.
• A Data-Driven Behavior Modeling and Analysis Framework for Diabetic Patients on Insulin Pumps. Sanjian Chen, Lu Feng, Michael R. Rickels, Amy Peleckis, Oleg Sokolsky, and Insup Lee. In IEEE International Conference on Healthcare Informatics 2015 (ICHI 2015), Dallas, TX, USA, October 2015.
• An Intraoperative Glucose Control Benchmark for Formal Verification. Sanjian Chen, Matthew O'Kelly, James Weimer, Oleg Sokolsky, and Insup Lee. In 5th IFAC conference on Analysis and Design of Hybrid Systems (ADHS 2015), Atlanta, GA, USA, October 2015.
• A Hybrid Approach to Causality Analysis. Shaohui Wang, Yoann Geoffroy, Gregor Gossler, Oleg Sokolsky, and Insup Lee. In 15th International Conference on Runtime Verification (RV 2015), Vienna, Austria, September 2015.
• Requirement Engineering for Functional Alarm System for Interoperable Medical Devices. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Vasiliki Sfyrla, Oleg Sokolsky, and Insup Lee. In International Conference on Computer Safety, Reliability & Security (SEFECOMP 2015), Delft, the Netherlands, September 2015.
• Towards Assurance for Plug & Play Medical Systems. Andrew L. King, Lu Feng, Sam Procter, Sanjian Chen, Oleg Sokolsky, John Hatcliff, and Insup Lee. In International Conference on Computer Safety, Reliability & Security (SEFECOMP 2015), Delft, the Netherlands, September 2015.
• Robust Monitoring of Hypovolemia in Intensive Care Patients using Photoplethysmogram Signals. Alexander Roederer, James Weimer, Joseph DiMartino, Jacob Gutsche, Insup Lee. In 37th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC 2015), Milan, Italy, August 2015.
• Towards Non-Invasive Monitoring of Hypovolemia in Intensive Care Patients. Alexander Roederer, James Weimer, Joseph Dimartino, Jacob Gutsche, and Insup Lee. In 6th Workshop on Medical Cyber-Physical Systems (MedicalCPS 2015), Seattle, WA, April 2015.
• Towards a Model-Based Meal Detector for Type I Diabetics. Sanjian Chen, James Weimer, Michael Rickels, Amy Peleckis and Insup Lee. In 6th Workshop on Medical Cyber-Physical Systems (MedicalCPS 2015), Seattle, WA, April 2015.
• Early Detection of Critical Pulmonary Shunts in Infants. Radoslav Ivanov, James Weimer, Allan Simpao, Mohamed Rehman, and Insup Lee. In Proceedings of 6th International Conference on Cyber-Physical Systems (ICCPS 2015), Seattle, WA, April 2015.
• Prediction of Significant Vasospasm in Aneurysmal Subarachnoid Hemorrhage Using Automated Data. Alexander Roederer, John H. Holmes, Michelle J. Smith, Insup Lee, Soojin Park. In Neurocrit Care, Vol. 21, Num. 3, pp. 444-50, December 2014.
• Safety-critical Medical Device Development using the UPP2SF Model Translation Tool. M. Pajic, Z. Jiang, O. Sokolsky, I. Lee and R. Mangharam. In ACM Transactions on Embedded Computing, Volume 13 Issue 4s, Article No. 127, July 2014.
• From Requirements to Code: Model Based Development of A Medical Cyber Physical System. Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Mats Heimdahl, Baek-Gyu Kim, Oleg Sokolsky and Insup Lee. In Proceedings of Joint event of the Fourth Symposium on Foundations of Health Information Engineering and Systems (FHIES) and the Software Engineering in Healthcare (SEHC) workshop (FHIES/SEHC '14), Washington, D.C., July 2014.
• The MIDdleware Assurance Substrate: Enabling Strong Real-Time Guarantees in Open Systems with OpenFlow. Andrew L. King, Sanjian Chen, and Insup Lee. In Proceedings of 17th IEEE Computer Society symposium on object/component/service-oriented realtime distributed computing (ISORC 2014), Reno, Nevada, USA, June 2014.
• Linking abstract analysis to concrete design: A hierarchical approach to verify medical CPS safety. Anitha Murugesan, Oleg Sokolsky, Sanjai Rayadurgam, Michael Whalen, Mats Heimdahl, and Insup Lee. In Proceedings of 5th International Conference on Cyber-Physical Systems (ICCPS 2014), Berlin, Germany, April 2014.
• A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal. Lu Feng, Andrew L. King, Sanjian Chen, Anaheed Ayoub, Junkil Park, Nicola Bezzo, Oleg Sokolsky, and Insup Lee. In Medical Cyber Physical Systems Workshop 2014, Berlin, Germany, April 2014.
• Functional Alarms for Systems of Interoperable Medical Devices. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Oleg Sokolsky and Insup Lee. In 15th IEEE International Symposium on High Assurance Systems Engineering (HASE 2014), Miami, Florida, USA, January 9 - 11, 2014.
• Model-Driven Safety Analysis of Closed-Loop Medical Systems. Miroslav Pajic, Rahul Mangharam, Oleg Sokolsky, David Arney, Julian M. Goldman, and Insup Lee. In IEEE Transactions on Industrial Informatics, 10(1), 2014, pp 3-16. Published in IEEE Xplore Early Access October 2012
• Model-based development of the Generic PCA infusion pump user interface within PVS. Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, Oleg Sokolsky, and Harold Thimbleby. In 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2013, Toulouse, France, September 2013. LNCS Volume 8153, 2013, pp 228-240, doi 10.1007/978-3-642-40793-2_21.
• Evaluation and Enhancement of an Intraoperative Insulin Infusion Protocol via In-Silico Simulation. Benjamin Kohl, Sanjian Chen, Margaret Mullen-Fortino, and Insup Lee. In IEEE International Conference on Healthcare Informatics (ICHI 2013), Philadelphia, PA, September 2013.

• A Modal Specification Approach for On-Demand Medical Systems. Andrew L. King, Lu Feng, Oleg Sokolsky, Insup Lee. In Third International Symposium on Foundations of Health Information Engineering and Systems (FHIES 2013), Macau, August 2013.
• Assuring the Safety of On-Demand Medical Cyber-Physical Systems. Andrew L. King, Lu Feng, Oleg Sokolsky, Insup Lee. In 1st International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2013), Taipei, Taiwan, August 2013.

A Causality Analysis Framework for Component-based Real-time Systems. Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor G ossler, Oleg Sokolsky, and Insup Lee. In 13th International Conference on Runtime Verification (RV '13), INRIA Rennes, France, September 2013.

• Assessing the Overall Sufficiency of Safety Arguments. Anaheed Ayoub, Jian Chang, Oleg Sokolsky, and Insup Lee. In 21st Safety-critical Systems Symposium (SSS'13). Bristol, UK, February 2013.
• Security and Interoperable Medical Device Systems, Part 2: Failures, Consequences and Classifications. Eugene Y. Vasserman, Krishna K. Venkatasubramanian, Oleg Sokolsky, and Insup Lee. In IEEE Security & Privacy. 10(6), pp 70 - 73, November-December 2012.
• Security and Interoperable Medical Device Systems: Part 1. Krishna K. Venkatasubramanian, Eugene Y. Vasserman, Oleg Sokolsky, and Insup Lee. In IEEE Security & Privacy. 10(5), pp 61 - 63, September-October 2012.
• A Model-Based I/O Interface Synthesis Framework for the Cross-Platform Software Modeling. BaekGyu Kim, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In IEEE International Symposium on Rapid System Prototyping (RSP 2012). Tampere, Finland, October 2012.
• Evaluation of a Smart Alarm for Intensive Care using Clinical Data. Andrew King, Kelsea Fortino, Nicholas Stevens, Sachin Shah, Margaret Fortino-Mullen, and Insup Lee. In 34th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC'12). San Diego, California, September, 2012.
• A Systematic Approach to Justifying Sufficient Confidence in Software Safety Arguments. Anaheed Ayoub, BaekGyu Kim, Insup Lee, and Oleg Sokolsky. In 31st International Conference on Computer Safety, Reliability and Security (SAFECOMP 2012), Magdeburg, Germany, September 2012.
• Rationale and Architecture Principles for Medical Application Platforms. John Hatcliff, Andrew King, Insup Lee, Alasdair MacDonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger and Julian Goldman. In ACM/IEEE Third International Conference on Cyber-Physical Systems (ICCPS 2012). Beijing, China, April 2012 (Invited Paper).
• From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study. Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam. In 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012). Beijing, China, April 2012.
• A Safety Case Pattern for Model-Based Development Approach. Anaheed Ayoub, Baek-Gyu Kim, Insup Lee and Oleg Sokolsky. In NASA Formal Methods Symposium (NFM). Norfolk, VA, April 2012.
• Challenges and Research Directions in Medical Cyber-Physical Systems. Insup Lee, Oleg Sokolsky, Sanjian Chen, John Hatcliff, Eunkyoung Jee, BaekGyu Kim, Andrew King, Margaret Mullen-Fortino, Soojin Park, Alexander Roederer, and Krishna Venkatasubramanian. In Special Issue on Cyber-Physical Systems, Proceedings of the IEEE, Volume 100, Issue 1, pp.75-90, January 2012 (Invited Paper).
• The Medical Device Dongle: An Open-Source Standards-Based Platform for Interoperable Medical Device Connectivity. Philip Asare, Danyang Cong, Santosh Vattam, Baek-Gyu Kim, Shan Lin, Oleg Sokolsky, Margaret Mullen-Fortino and Insup Lee. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
• Smart Alarms: Multivariate Medical Alarm Integration for post CABG surgery patients. Stevens Nicholas, Giannareas Ana, Kern Vanessa, Viesca Adrian, Fortino-Mullen Margaret, King Andrew, Lee Insup. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
• Clinical Decision Support for Integrated Cyber-Physical Systems: A Mixed Methods Approach. Alex Roederer, Andrew Hicks, Enny Oyeniran, Insup Lee and Soojin Park. In Proceedings of the 2nd ACM SIGHIT International Health Informatics Symposium (IHI 2012). Miami, FL, January 2012.
• Limitations of Threshold-Based Brain Oxygen Monitoring for Seizure Detection. Soojin Park, Alexander Roederer, Ram Mani, Sarah Schmitt, Peter D. LeRoux, Lyle H. Ungar, Insup Lee, Scott E. Kasner. In Neurocritical Care. December 2011, Volume 15, Issue 3, pp 469-476
• Challenges in the Regulatory Approval of Medical Cyber-Physical Systems. Oleg Sokolsky, Insup Lee, and Mats Heimdahl. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
• Safety-Assured Development of the GPCA Infusion Pump Software. BaekGyu Kim, Anaheed Ayoub, Oleg Sokolsky, Insup Lee, Paul Jones, Yi Zhang, and Raoul Jetley. In Proceedings of the International Conference on Embedded Software (EMSOFT 2011). Taipei, Taiwan, October 2011.
• Biomedical Devices and Systems Security. David Arney, Krishna K. Venkatasbramanian, Oleg Sokolsky, and Insup Lee. In Proceedings of 33rd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC ’11). Boston, MA, August/September 2011.
• On Effective Testing of Health Care Simulation Software. Christian Murphy, M.S. Raunak, Andrew King, Sanjian Chen, Christopher Imbriano, Gail Kaiser, Insup Lee, Oleg Sokolsky, Lori Clarke, Leon Osterweil. In Proceedings of the 3rd International Workshop on Software Engineering in Health Care (SEHC 2011). Honolulu, Hawaii, May 2011.
• GSA: A Framework for Rapid Prototyping of Smart Alarm Systems. Andrew King, Alex Roederer, David Arney, Sanjian Chen, Margaret Fortino-Mullen, Ana Giannareas, C. William Hanson III, Vanessa Kern, Nicholas Stevens, Jonathan Tannen, Adrian Viesca Trevino, Soojin Park, Oleg Sokolsky, and Insup Lee. In Proceedings of the 1st ACM International Health Informatics Symposium (IHI '10), Arlington, Virginia, USA, November 2010. ( ACM Portal)
• Assurance Cases in Model-Driven Development of the Pacemaker Software. Eunkyoung Jee, Insup Lee and Oleg Sokolsky In Proceedings of the 4th International Symposium On Leveraging Application of Formal Methods, Verification and Validation (ISoLA 2010), Part II, LNCS 6416, pp. 343-356, Amirandes, Heraclion, Crete, October 2010.(Springer)
• A Safety-Assured Development Approach for Real-Time Software. Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky, and Insup Lee. In 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2010), Macau, China, August 2010.
• Medical Cyber Physical Systems. Insup Lee and Oleg Sokolsky. In 47th Design Automation Conference (DAC 2010), CPS Demystified Session, Anaheim, CA, June 2010. (Invited Paper) ACM Portal
• Prototyping Closed Loop Physiologic Control with the Medical Sevice Coordination Framework. Andrew King, Dave Arney, Insup Lee, Oleg Sokolsky, John Hatcliff, and Sam Proctor. In 2nd Workshop on Software Engineering in Health Care (SEHC 2010), Cape Town, South Africa, May 2010.
• Toward Patient Safety in Closed-Loop Medical Device Systems. David Arney, Miroslav Pajic, Julian M. Goldman, Insup Lee, Rahul Mangharam, and Oleg Sokolsky. In Cyber-Physical Systems (ICCPS 2010), Stockholm, Sweden, April 2010.
• Model-Based Testing of GUI-Driven Applications, Vivien Chinnapongse, Insup Lee, Oleg Sokolsky, Shaohui Wang, and Paul L. Jones, The Seventh IFIP Workshop on Software Technologies for FutureEmbedded and Ubiquitous Systems (SEUS 2009), Newport Beach, CA, LNCS 5860, pp. 203-214, November 2009.
• Plug-and-Play for Medical Devices: Experiences from a Case Study, David Arney, Sebastian Fischmeister, Julian M. Goldman, Insup Lee, and Robert Trausmuth, Biomedical Instrumentation & Technology, Volume 43, Issue 4 (July-August 2009) p.313-317.
• Synchronizing an X-ray and Anesthesia Machine Ventilator:A Medical Device Interoperability Case Study, David Arney, Julian M. Goldman, Susan F. Whitehead and Insup Lee, Proceedings of International Conference on Biomedical Electronics and Devices (BioDevices 2009), Porto, Portugal, January 2009.
• Formal Methods Based Development of a PCA Infusion Pump Reference Model: Generic Infusion Pump (GIP) Project, David Arney, Raoul Jetley, Paul Jones, Insup Lee, Oleg Sokolsky, Proceedings of 2007 Joint Workshop on High Confidence Medical Devices, Software, and Systems and Medical Device Plug-and-Play Interoperability, Boston, MA, June 2007.
• Securing the Drop-Box Architecture for Assisted Living, Michael J. May, Wook Shin, Carl A. Gunter, Insup Lee, Proceedings of the 4th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE 2006), George Mason University, Fairfax, Virginia, November 2006.
• High-Confidence Medical Device Software and Systems, Insup Lee, George J. Pappas, RanceCleaveland, JohnHatcliff, Bruce H.Krogh, Peter Lee, HarveyRubin, and Lui Sha, IEEE Computer, Volume 39, Issue 4, April 2006, pp. 33-38.
• Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System, Rajeev Alur, David Arney, Elsa L. Gunter, Insup Lee, Jaime Lee, Wonhong Nam, Frederick Pearce, Steve Van Albert, Jiaxiang Zhou International Journal in Software Tools for Technology Transfer (2004) Volume 5, Issue 4, May 2004, pages 308-319.

Safe AI and Autonomy

• Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning. Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee. Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV), Los Angeles, CA, July 2021.
• Detecting OODs as datapoints with High Uncertainty. Ramneet Kaur, Susmit Jha, Anirban Roy, Sangdon Park, Oleg Sokolsky, Insup Lee. Proceedings of Workshop on Uncertainty and Robustness in Deep Learning (UDL), Virtually, July 2021.
• ModelGuard: Runtime Validation of Lipschitz-continuous Models. Taylor Carpenter, Radoslav Ivanov, Insup Lee, James Weimer. Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Brussels, Belgium, July 2021.
• Real-time detectors for digital and physical adversarial inputs to perception systems. Yiannis Kantaros, Taylor Carpenter, Kaustubh Sridhar, Yahan Yang, Insup Lee, and James Weimer. Proceedings of the 12th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Nashville, TN, May 2021.
• Improving Classifier Confidence using Lossy Label-Invariant Transformations. Sooyong Jang, Insup Lee, and James Weimer. Proceedings of International Conference on Artificial Intelligence and Statistics (AISTATS), April 2021.
• Verifying the Safety of Autonomous Systems with Neural Network Controllers. Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. ACM Transactions on Embedded Computing Systems (TECS) 20, Vol 1, Num 1, pp 1-26, December 2020.
• PAC Confidence Predictions for Deep Neural Network Classifiers. Sangdon Park, Shuo Li, Osbert Bastani, and Insup Lee. In submission, November 2020.
• Calibrated Prediction with Covariate Shift via Unsupervised Domain Adaptation. Sangdon Park, Osbert Bastani, James Weimer, and Insup Lee.In Proceedings of 23rd International Conference on Artificial Intelligence and Statistics (AISTATS 2020), Palermo, Italy, June 2020.
• PAC Confidence Sets for Deep Neural Networks via Calibrated Prediction. Sangdon Park, Osbert Bastani, Nikolai Matni, and Insup Lee. In Proceedings of International Conference on Learning Representations (ICLR 2020), Addis Ababa, Ethiopia, April 2020.
• Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller. Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George Pappas, and Insup Lee. To appear in Proceedings of 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2020), Sydney, Australia, April 2020. (Received HSCC repeatability badge)
• Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees.M. Hasanbeig, Y. Kantaros, A. Abate, D. Kroening, G. J. Pappas, I. Lee. In Proceedings of 58th IEEE Conference on Decision and Control (CDC 2019), Nice, France, December 2019.
• Verisig: verifying safety properties of hybrid systems with neural network controllers. Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. In Proceedings of 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2019), Montreal, Canada, April 2019.

Security, Trust Management, and Policy Modeling

• Detecting Security Leaks in Hybrid Systems with Information Flow Analysis. Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, and Rajeev Alur. In Proceedings of 17th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MemoCODE 2019), San Diego, CA, USA, October 2019. (Best Paper Award)
• Injected and Delivered: Fabricating Implicit Control over Actuation Systems by Spoofing Inertial Sensors. Yazhou Tu, Zhiqiang Lin, Insup Lee, Xiali Hei. In Proceedings of 27th USENIX Security Symposium, Baltimore, MD, USA, August 2018.
• LogSafe: Secure and Scalable Data Logger for IoT Devices. Hung Nguyen, Radoslav Ivanov, Linh T.X. Phan, Oleg Sokolsky, James Weimer, and Insup Lee. In Proceedings of 3rd ACM/IEEE International Conference on Internet of Things Design and Implementation (IoTDI 2018), Orlando, FL, USA, April 2018.
• Cyber-Physical System Checkpointing and Recovery. Fanxin Kong, Meng Xu, James Weimer, Oleg Sokolsky, Insup Lee. In Proceedings of 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2018), Porto, Portugal, April 2018.
• Security of Cyber-Physical Systems in the Presence of Transient Sensor Faults. Junkil Park, Radoslav Ivanov, James Weimer, Miroslav Pajic, Sang Hyuk Son, and Insup Lee. In ACM Transactions on Cyber-Physical Systems, Volume 1 Issue 3, Article No. 15, July 2017.
• Design and Implementation of Attack-Resilient Cyber-Physical Systems. Miroslav Pajic, James Weimer, Nicola Bezzo, Oleg Sokolsky, George J. Pappas, and Insup Lee. In IEEE Control Systems , Volume 37 Issue 2, pp. 68-81, April 2017.
• Resilient Linear Classification: An Approach to Deal with Attacks on Training Data. Sangdon Park, James Weimer, and Insup Lee. In 8th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2017), Pittsburgh, PA, April 2017.
• Attack-Resilient State Estimation for Noisy Dynamical Systems. Miroslav Pajic, Insup Lee, George J. Pappas. In IEEE Transactions on Control of Network Systems, Volume 4 Issue 1, pp. 82-92, March 2017.
• Adaptive Transient Fault Model for Sensor Attack Detection. Minsu Jo, Junkil Park, Youngmi Baek, Radoslav Ivanov, James Weimer, Sang Hyuk Son, and Insup Lee. In Proceedings of 2016 IEEE 4th International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2016), Nagoya, Japan, October 2016.
• Scalable Verification of Linear Controller Software. Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. In Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, The Netherlands, April 2016.
• Attack-Resilient Sensor Fusion for Safety-Critical Cyber-Physical Systems. Radoslav Ivanov, Miroslav Pajic, and Insup Lee. In ACM Transactions on Embedded Computing Systems, Volume 15 Issue 1, February 2016.
• Attack-Resilient State Estimation in the Presence of Noise. Miroslav Pajic, Paulo Tabuada, Insup Lee, and George Pappas. In Proceedings of 54th IEEE Conference on Decision and Control (CDC), Osaka, Japan, December 2015.
• Automatic Verification of Linear Controller Software. Miroslav Pajic, Junkil Park, Insup Lee, George J. Pappas, and Oleg Sokolsky. In Proceedings of International Conference on Embedded Software (EMSOFT 2015), Amsterdam, the Netherlands, October 2015.
• Robust Estimation Using Context-Aware Filtering. Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, George Pappas, and Insup Lee. In Proceedings of 53rd Annual Allerton Conference on Communication, Control, and Computing, Urbana-Champaign, IL, September/October 2015.
• Robust Localization Using Context-Aware Filtering. Radoslav Ivanov, Nikolay Atanasov, Miroslav Pajic, Insup Lee, and George Pappas. In Proceedings of Workshop on Multi-View Geometry in Robotics (MVIGRO 2015) (in conjunction with the 2015 Robotics: Science and Systems Conference (RSS 2015)), Rome, Italy, July 2015.
• Verified ROS-Based Deployment of Platform-Independent Control Systems. Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee. In Proceedings of 7th NASA Formal Methods Symposium (NFM 2015), Pasadena, CA, April 2015.
• Sensor attack detection in the presence of transient faults. Junkil Park, Radoslav Ivanov, James Weimer, Miroslav Pajic, and Insup Lee. In Proceedings of 6th International Conference on Cyber-Physical Systems (ICCPS 2015), Seattle, WA, April 2015.
• Attack-Resilient Minimum Mean-Squared Error Estimation. James Weimer, Nicola Bezzo, Miroslav Pajic, Oleg Sokolsky, and Insup Lee. In Proceedings of 2014 American Control Conference (ACC 2014), Portland, Oregon, USA, June 2014.
• Robustness of Attack-resilient State Estimators. Miroslav Pajic, James Weimer, Nicola Bezzo, Paulo Tabuada, Oleg Sokolsky, Insup Lee, George Pappas. In Proceedings of 5th International Conference on Cyber-Physical Systems (ICCPS 2014), Berlin, Germany, April 2014. (Best paper award at ICCPS 2014)
• Resilient Multidimensional Sensor Fusion using Measurement History. Radoslav Ivanov, Miroslav Pajic, Insup Lee. In 3rd ACM International Conference on High Confidence Networked Systems (HiCoNS 2014), Berlin, Germany, April 2014.
• Attack-Resilient Sensor Fusion. Radoslav Ivanov, Miroslav Pajic, Insup Lee. In Design, Automation and Test in Europe (DATE 2014), Dresden, Germany, March 2014.
• AS-CRED: Reputation and Alert Service for Inter-domain Routing. Jian Chang, Krishna Venkatasubramanian, Andrew G. West, Sampath Kannan, Insup Lee, Boon Thau Loo, and Oleg Sokolsky. In IEEE Systems Journal, Vol. 7(3), pp. 396-409, (September 2013).
• A Trust Model for Vehicular Network-Based Incident Reports. Cong Liao, Jian Chang, Insup Lee, and Krishna K. Venkatasubramanian. In IEEE Symposium on Wireless Vehicular Communications (WiVeC 2013). Dresden, Germany, June 2-3, 2013.
• Towards Synthesis of Platform-aware Attack-Resilient Control Systems. Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, and Insup Lee. In 2nd ACM International Conference on High Confidence Networked Systems (HiCoNS), Philadelphia, Pennsylvania, April 2013.
• Resilient Parameter-Invariant Control with Application to Vehicle Cruise Control. James Weimer, Nicola Bezzo, Miroslav Pajic, George J. Pappas, Oleg Sokolsky, and Insup Lee. In Workshop on Control of Cyber-Physical Systems, Johns Hopkins University, Baltimore, MD, March 2013.
• Trust in Collaborative Web Applications. Andrew West, Jian Chang, Krishna Venkatasubramanian, Insup Lee. In Elsevier Future Generation Computer Systems, Volume 28, Issue 8, pp.1238–1251, October 2012 (Invited Paper). Based in part on UPENN MS-CIS-10-33 technical report
• Towards Content-driven Reputation for Collaborative Code Repositories. Andrew G. West and Insup Lee. In Proceedings of the Eighth International Symposium on Wikis and Open Collaboration (WikiSym '12). Linz, Austria. August 2012.
• Spamming for Science: Active Measurement in Web 2.0 Abuse Research. Andrew West, Pedram Hayati, Vidyasagar Potdar, and Insup Lee. In 3rd Workshop on Ethics in Computer Security Research 2012 (WECSR 2012). Bonaire, March 2012.
• Autonomous Link Spam Detection in Purely Collaborative Environments. Andrew G. West, Avantika Agrawal, Phillip Baker, Brittney Exline, and Insup Lee. In Proceedings of Seventh International Symposium on Wikis and Open Collaboration (WikiSym ’11). Mountain View, California, October 2011.
• What Wikipedia Deletes: Characterizing Dangerous Collaborative Content. Andrew G. West, Avantika Agrawal, Phillip Baker, Brittney Exline, and Insup Lee. In Proceedings of Seventh International Symposium on Wikis and Open Collaboration (WikiSym ’11). Mountain View, California, October 2011.
• Multilingual Vandalism Detection using Language-Independent & Ex Post Facto Evidence. Andrew G. West and Insup Lee. In Notebook Papers on Uncovering Plagiarism, Authorship, and Social Software Misuse (CLEF 2011). Amsterdam, Netherlands, September 2011.
• ToMaTo: A Trustworthy Code Mashup Development Tool. Jian Chang, Krishna Venkatasubramanian, Andrew G. West, Sampath Kannan, Oleg Sokolsky, Myuhng Joo Kim, and Insup Lee. In Proceedings of 5th International Workshop on Web APIs and Service Mashups (Mashups 2011). Lugano, Switzerland, September 2011.
• Link Spamming Wikipedia for Profit. Andrew G. West, Jian Chang, Krishna Venkatasubramanian, Oleg Sokolsky, and Insup Lee. In Proceedings of 8th Annual Collaboration, Electronic Messaging, Anti-Abuse, and Spam Conference (CAES 2011). pp. 152-161, Perth, Australia, September 2011 (co-Best Paper Award).
• Towards the Effective Temporal Association Mining of Spam Blacklists. Andrew G. West and Insup Lee. In Proceedings of 8th Annual Collaboration, Electronic Messaging, Anti-Abuse, and Spam Conference (CAES 2011). pp. 73-82, Perth, Australia, September 2011.
• AS-TRUST: A Trust Quantification Scheme for Autonomous Systems in BGP. Jian Chang, Krishna Venkatasubramanian, Andrew G. West, Sampath Kannan, Boon Thau Loo, Oleg Sokolsky, and Insup Lee. In 4th International Conference on Trust and Trustworthy Computing (TRUST 2011). Pittsburgh, PA, June 2011.
• Reputation-based Networked Control with Data-Corrupting Channels. Shreyas Sundaram, Jian Chang, Krishna K. Venkatasubramanian, Chinwendu Enyioha, Insup Lee, George Pappas. In Proceedings of Hybrid Systems: Computation and Control (HSCC), Chicago, IL, April 2011.
• Permission to speak: A logic for access control and conformance. Nikhil Dinesh, Aravind Joshi, Insup Lee, and Oleg Sokolsky. In Journal of Logic and Algebraic Programming, Vol. 80(1), pp. 50-74, January 2011.
• Spam Mitigation using Spatio-Temporal Reputations from Blacklist History. Andrew G. West, Adam J. Aviv, Jian Chang, and Insup Lee. In Proceedings of the 26th Annual Computer Security Applications Conference, Orlando, Florida, December 2010.
• SSTiki: An Anti-Vandalism Tool for Wikipedia using Spatio-Temporal Analysis of Revision Metadata. Andrew G. West, Sampath Kannan, and Insup Lee. In 6th International Symposium on Wikis and Open Collaboration (WikiSym 2010), Gdansk, Poland, July 2010.
• Spatio-Temporal Analysis of Wikipedia Metadata and the STiki Anti-Vandalism Tool. Andrew G. West, Sampath Kannan, and Insup Lee. In 6th International Symposium on Wikis and Open Collaboration (WikiSym 2010), Gdansk, Poland, July 2010.
• Detecting Wikipedia Vandalism via Spatio-Temporal Analysis of Revision Metadata. Andrew G. West, Sampath Kannan, and Insup Lee. In 3rd European Workshop on System Security (EUROSEC 2010), Paris, France, April 2010. - Preliminary Version
• An Evaluation Framework for Reputation Management Systems. Andrew G. West, Sampath Kannan, Insup Lee, and Oleg Sokolsky. In Trust Modeling and Management in Digital Environments: From Social Concept to System Development (Zheng Yan, ed.). 2009.
• Strong and Weak Policy Relations, Michael J. May, Carl A. Gunter, Insup Lee, and Steve Zdancewic, IEEE International Symposium on Policies for Distributed Systemsand Networks (POLICY 2009), London, July 2009.
• QuanTM: A Quantitative Trust Management System, Andrew G. West, Adam J. Aviv, Jian Chang, Vinayak S. Prabhu, Matt Blaze, Sampath Kannan, Insup Lee, Jonathan M. Smith, and Oleg Sokolsky, Proceedings of the European Workshop on System Security (EUROSEC 2009), Nuremberg, Germany, March 2009.
• Dynamic Trust Management, Matt Blaze, Sampath Kannan, Insup Lee, Oleg Sokolsky, Jonathan M. Smith, Angelos D. Keromytis, Wenke Lee, IEEE Computer, Volume 42, Issue 2, February 2009, pp. 44-52.
• Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking, Nikhil Dinesh, Aravind K. Joshi, Insup Lee, and Oleg Sokolsky, Proceedings of the Ninth International Conference on Deontic Logic in Computer Science (DEON'08), Luxembourg, July 2008.
• Logic-based Regulatory Conformance Checking, Nikhil Dinesh, Aravind Joshi, Insup Lee, and Oleg Sokolsky, 14th Monterey Workshop (2007), Monterey, CA, September 2007.
• Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies, Michael J. May, Carl A. Gunter, and Insup Lee, Proceedings of the 19th IEEE Computer Security FoundationsWorkshop (CSFW 2006), Venice, Italy, July 2006.
• Sensor Network Security: More Interesting Than You Think, Madhukar Anand, Eric Cronin, Micah Sherr, Matt Blaze, Zachary Ives and Insup Lee, Proceedings of the 1st USENIX Workshop on Hot Topics in Security(HotSec 2006), Vancouver, B.C. Canada, July 2006.
• Quantifying Eavesdropping Vulnerability in Sensor Networks, Madhukar Anand, Zachary G. Ives, and Insup Lee, Proceedings of the 2nd International VLDB Workshop on Data Management for Sensor Networks, DMSN'05, Trondheim, Norway, August 2005.

Real-Time Resource Management: Compositional Scheduling, Virtualization, Communication

• Towards Virtualization-Agnostic Latency for Time-Sensitive Applications. Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh Phan, Insup Lee, Oleg Sokolsky. Proceedings of the 29th International Conference on Real-Time Networks and Systems (RTNS), Nantes, France, April 2021. (Outstanding paper award)
• Holistic resource allocation for multicore real-time systems. Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, and Insup Lee. In Proceedings of IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2019), Montreal, Canada, April 2019. (Best Paper Award)
• Data Freshness Over-Engineering: Formulation and Results. Dagaen Golomb, Deepak Gangadharan, Sanjian Chen, Oleg Sokolsky, and Insup Lee. In Proceedings of IEEE ISORC 2018, Singapore, May 2018 (Best Paper Award).
• Generic Formal Framework for Compositional Analysis of Hierarchical Scheduling Systems. Jalil Boudjadar, Jin Hyun Kim, Linh Thi Xuan Phan, Insup Lee, Kim G. Larsen, Ulrik Nyman. In Proceedings of IEEE ISORC 2018, Singapore, May 2018.
• MC-Fluid: Multi-Core Fluid-Based Mixed-Criticality Scheduling. Jaewoo Lee, Saravanan Ramanathan, Kieu-My Phan, Arvind Easwaran, Insik Shin, and Insup Lee. In IEEE Transactions on Computers, Volume 67, Issue 4, pp. 469-483, April 2018.
• Multi-Mode Virtualization for Soft Real-Time Systems. Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh T. X. Phan, Insup Lee, and Oleg Sokolsky. In Proceedings of IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2018), Porto, Portugal, April 2018.
• MC-ADAPT: Adaptive Task Dropping in Mixed-Criticality Scheduling. Jaewoo Lee, Hoon Sung Chwa, Linh T.X. Phan, Insik Shin, and Insup Lee. In Proceedings of International Conference on Embedded Software (EMSOFT 2017), Seoul, South Korea, October 2017.
• Extensible Energy Planning Framework for Preemptive Tasks. Jin Hyun Kim, Deepak Gangadharan, Oleg Sokolsky, Axel Legay, and Insup Lee. In Proceedings of 20th International Symposium on Real-Time Computing (ISORC 2017), Toronto, Canada, May 2017.
• vCAT: Dynamic Cache Management Using CAT Virtualization. Meng Xu, Linh T.X. Phan, Hyon-Young Choi, and Insup Lee. In 23th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS' 17), Pittsburgh, PA, April 2017.
• AutoV: An Automotive Testbed for Real-Time Virtualization. Meng Xu and Insup Lee. In Second TCRTS Workshop on Certifiable Multicore Avionics and Automotive Systems (CMAAS 2017), Pittsburgh, PA, April 2017.
• Resilient Linear Classification: An Approach to Deal with Attacks on Training Data. Bong-Ho Kim, Doru Calin, Insup Lee. In IEEE Wireless Communications and Networking Conference (WCNC 2017), San Francisco, CA, March 2017.
• Cloud-Based Secure Logger for Medical Devices. Hung Nguyen, Bipeen Acharya, Radoslav Ivanov, Andreas Haeberlen, Linh T.X. Phan, Oleg Sokolsky, Jesse Walker, James Weimer, C. William Hanson III, and Insup Lee. In Proceedings of IEEE First International Conference on Connected Health: Applications, Systems and Engineering Technologies (CHASE 2016), Washington, DC, USA, June 2016.
• Analysis and Implementation of Global Preemptive Fixed-Priority Scheduling with Dynamic Cache Allocation. Meng Xu, Linh Thi Xuan Phan, Hyon-Young Choi and Insup Lee. In Proceedings of IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2016), Vienna, Austria, April 2016.
• Optimizing the Resource Requirements of Hierarchical Scheduling Systems. Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Abdeldjalil Boudjadar, Ulrik Nyman, Kim G. Larsen, Insup Lee, and Jin-Young Choi. In 8th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2015), held in conjunction with 36th IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
• Towards Compositional Mixed-Criticality Real-Time Scheduling in Open Systems. Jaewoo Lee, Hoon Sung Chwa, Arvind Easwaran, Insik Shin, and Insup Lee. In 8th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2015), held in conjunction with 36th IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
• Cache-aware Interfaces for Compositional Real-Time Systems. Linh T.X. Phan, Meng Xu, and Insup Lee. In 8th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2015), held in conjunction with 36th IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
• Cache-Aware Compositional Analysis of Real-Time Multicore Virtualization Platforms. Meng Xu, Linh T.X. Phan, Oleg Sokolsky, Sisu Xi, Chenyang. Lu, Christopher D. Gill, and Insup Lee. In Real-Time Systems Journal, Volume 51, Issue 6, pp 675-723, November 2015, published online April 2015.
• RT-OpenStack: CPU Resource Management for Real-Time Cloud Computing. Sisu Xi, Chong Li, Chenyang Lu, Christopher D. Gill, Meng Xu, Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In 8th IEEE International Conference on Cloud Computing (IEEE CLOUD), New York, USA, June 2015.
• MC-Fluid: Fluid Model-Based Mixed-Criticality Scheduling on Multiprocessors. Jaewoo Lee, Kieu-My Phan, Xiaozhe Gu, Jiyeon Lee, Arvind Easwaran, Insik Shin, and Insup Lee. In Proceedings of IEEE Real-Time Systems Symposium (RTSS 2014), Rome, Italy, December 2014. (Best Paper runner-up).
• Real-Time Multi-Core Virtual Machine Scheduling in Xen. Sisu Xi, Meng Xu, Chenyang Lu, Linh T.X. Phan, Christopher Gill, Oleg Sokolsky, and Insup Lee. In Proceedings of 14th International Conference on Embedded Software (EMSOFT 2014), New Delhi, India, October 2014.
• Cache-Aware Compositional Analysis of Real-Time Multicore Virtualization Platforms . Meng Xu, Linh T.X. Phan, Insup Lee, Oleg Sokolsky, Sisu Xi, Chenyang Lu, and Christopher Gill. In IEEE Real-Time Systems Symposium (RTSS 2013), Vancouver, Canada, December 2013. (Best Paper Runner-Up).
• A Comparison of Compositional Schedulability Analysis Techniques for Hierarchical Real-Time Systems. Madhukar Anand, Sebastian Fischmeister, and Insup Lee. In ACM Transactions on Embedded Computing Systems (TECS), Volume 13 Issue 1, Article No. 2, August 2013.
• Co-design of Control and Platform with Dropped Signals. Damoon Soudbakhsh, Linh T.X. Phan, Oleg Sokolsky, Insup Lee, and Anuradha Annaswamy. In 4th International Conference on Cyber-Physical Systems (ICCPS 2013). Philadelphia, PA, April 2013.
• Overhead-Aware Compositional Analysis of Real-Time Systems. Linh T. X. Phan, Meng Xu, Jaewoo Lee, Insup Lee, and Oleg Sokolsky. In 19th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS' 13). Philadelphia, PA, April 2013.
• Extending Task-level to Job-level Fixed Priority Assignment and Schedulability Analysis Using Pseudo-deadlines. Hoon Sung Chwa, Hyoungbu Back, Sanjian Chen, Jinkyu Lee, Arvind Easwaran, Insik Shin and Insup Lee. In 33rd IEEE Real-Time Systems Symposium (RTSS 2012), San Juan, Puerto Rico, December 2012 (Best Paper Award)
• Realizing Compositional Scheduling through Virtualization. Jaewoo Lee, Sisu Xi, Sanjian Chen, Linh T.X. Phan, Chris Gill, Insup Lee, Chenyang Lu, Oleg Sokolsky. In 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012). Beijing, China, April 2012. (Corresponding Technical Report)
• Towards A Compositional Multi-Modal Framework for Adaptive Cyber-Physical Systems. Linh T. X. Phan and Insup Lee. In 1st International Workshop on Cyber-Physical Systems, Networks, and Applications (CPSNA). Toyama, Japan, August 2011. (Invited Paper)
• Compositional Analysis of Real-Time Embedded Systems. Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In IEEE International Conference on Compilers, Architectures and Synthesis of Embedded Systems (CASES 2011). Taipei, Taiwan, October 2011. (Tutorial Abstract)
• Removing Abstraction Overhead in the Composition of Hierarchical Real-Time Systems. Sanjian Chen, Linh T. X. Phan, Jaewoo Lee, Insup Lee and Oleg Sokolsky. In Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2011), Chicago, IL, April 2011.
• A Semantic Framework for Multi-Mode Systems. Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2011), Chicago, IL, April 2011.
• On the Feasibility of Dynamic Rescheduling on the Intel Distributed Computing Platform. Zhuoyao Zhang, Linh T.X. Phan, Godfrey Tan, Saumya Jain, Harrison Duong, Boon Thau Loo, and Insup Lee. In Proceedings of the 11th ACM/IFIP/USENIX International Middleware Conference (Middleware 2010), Bangalore, India, December 2010.
• Improving Resource Utilization for Compositional Scheduling using DPRM Interfaces. Jaewoo Lee, Linh T.X. Phan, Sanjian Chen, Oleg Sokolsky, and Insup Lee. In the 3rd Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2010), San Diego, CA, November 2010.
• CARTS: A Tool for Compositional Analysis of Real-Time Systems. Linh T.X. Phan, Jaewoo Lee, Arvind Easwaran, Vinay Ramaswamy, Sanjian Chen, Insup Lee, and Oleg Sokolsky. In the 3rd Workshop on Compositional Theory and Technology for Real-Time Embedded Systems (CRTS 2010), San Diego, CA, November 2010.
• A Process Algebraic Framework for Modeling Resource Demand and Supply. Anna Philippou, Insup Lee, Oleg Sokolsky, and Jin-Young Choi. In 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), IST Austria, Klosterneuburg, Austria, September 2010.
• Compositional Analysis of Multi-Mode Systems. Linh T.X. Phan, Insup Lee, and Oleg Sokolsky. In 22nd Euromicro Conference on Real-Time Systems (ECRTS10), Brussels, Belgium, July 2010.
• Timing Analysis of Mixed Time/Event-Triggered Multi-Mode Systems, Linh T.X. Phan, Samarjit Chakraborty, and Insup Lee, The 30th IEEE Real-Time Systems Symposium(RTSS 2009), Washington, D.C., December 2009.
• Multiprocessor Real-Time Scheduling Considering Concurrency and Urgency, Jinkyu Lee, Arvind Easwaran, Insik Shin, and Insup Lee, The 30th IEEE Real-Time Systems Symposium(RTSS 2009), Work-in-Progress Proceedings, Washington, D.C., December 2009.
• A Compositional Scheduling Framework for Digital Avionics Systems, Arvind Easwaran, Insup Lee, Oleg Sokolsky and Steve Vestal, IEEE Real-Time Computing Systems and Applications (RTCSA 2009), Beijing, China, August 2009.
• Hardware Acceleration for Conditional State-Based Communication Scheduling on Real-Time Ethernet. Sebastian Fischmeister, Robert Trausmuth, and Insup Lee. In IEEE Transactions on Industrial Informatics, Vol.5, no.3, pp. 325-337, August 2009.
• Hardware Acceleration for Verifiable, Adaptive Real-Time Communication, Sebastian Fischmeister, Insup Lee, and Robert Trausmuth, Proceedings of 13th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Hamburg, Germany, September 2008.
• Hierarchical Scheduling Framework for Virtual Clustering of Multiprocessors, Insik Shin, Arvind Easwaran, Insup Lee, Proceedings of the 20th Euromicro Conference on Real-Time Systems (ECRTS 08), Prague, Czech Republic, July 2008.
• Compositional Feasibility Analysis for Conditional Task Models, Madhukar Anand, Arvind Easwaran, Sebastian Fischmeister, and Insup Lee, Proceedings of the 11th IEEE International Symposium on Object-oriented Real-time Distributed Computing (ISORC 2008), Orlando, Florida, May 2008.
• Compositional Real-Time Scheduling Framework with Periodic Model, Insik Shin and Insup Lee, ACM Transactions on Embedded Computing Systems (TECS), vol 7, no 3, April 2008.
• Interface Algebra for Analysis of Hierarchical Real-Time Systems, Arvind Easwaran, Insup Lee, Oleg Sokolsky, Proceedings of the Foundations of Interface Technologies (FIT'08), Satellite workshop of ETAPS'08, Budapest, Hungary, April 5, 2008.
• Compositional Analysis Framework using EDP Resource Models, Arvind Easwaran, Madhukar Anand, and Insup Lee, RTSS 2007, Tucson, Arizona, December 2007.
• A Verifiable Language for Programming Communication Schedules, S. Fischmeister, O. Sokolsky, and I. Lee, IEEE Transactions on Computers, Vol. 56, pp. 1505-1519, November 2007.
• A Dynamic Scheduling Approach to Designing Flexible Safety-Critical Systems, L. Almeida, M. Anand, S. Fischmeister, and I. Lee, Proceedings of the 7th Annual ACM Conference on Embedded Software (emSoft '07), Salzburg, Austria, October 2007.
• Composition Techniques for Tree Communication Schedules, M. Anand and S. Fischmeister and I. Lee, Proceedings of the 19th Euromicro Conference on Real-TimeSystems (ECRTS 2007), Pisa, Italy, July 2007, pp. 235-246.
• Schedulability Analysis of Hierarchical Real-Time Systems, Arvind Easwaran, Insik Shin, Oleg Sokolsky, and Insup Lee, Proceedings of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC 2007), Santorini Island, Greece, May 2007. (Invited Paper)
• Incremental Schedulability Analysis of Hierarchical Real-Time Components, Arvind Easwaran, Insik Shin, Oleg Sokolsky, and Insup Lee, Proceedings of the 6th ACM International Conference onEmbedded Software (EMSOFT 2006), Seoul, South Korea, October 2006.
• An Analysis Framework for Network-Code Programs, Madhukar Anand, Sebastian Fischmeister, and Insup Lee, Proceedings of the 6th ACM International Conference onEmbedded Software (EMSOFT 2006), Seoul, South Korea, October 2006.
• Network-Code Machine: Programmable Real-Time Communication Schedules, Sebastian Fischmeister, and Oleg Sokolsky, and Insup Lee, Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'06), SanJose, California, April 2006. Supplemental Material
• End-to-end Application Performance Impact on Scheduler inCDMA-1XRTT Wireless System, Bong Ho Kim, Insup Lee, and Kelvin Chu, IEEE 61st Vehicular Technology Conference. VTC2005 Spring ,Volume 5, pp. 2770-2774 Stockholm, Sweden, May/June 2005.
• Compositional Real-Time Scheduling Framework, Insik Shin, Insup Lee, Proceedings of the 25th IEEE Real-Time Systems Symposium, RTSS 2004, Lisbon, Portugal, December 2004.
• Periodic Resource Model for Compositional Real-Time Guarantees, Insik Shin and Insup Lee, Proceeding of the 24th IEEE Real-Time Systems Symposium, RTSS 2003, Cancun, Mexico, December 2003 (Awarded as the Best Paper of RTSS 2003).
• Fair Real-time Traffic Scheduling over A Wireless LAN, Maria Adamou, Sanjeev Khanna, Insup Lee, Insik Shin, Shiyu Zhou, Proceedings of the 22nd IEEE Real-Time Systems Symposium, RTSS 2001, London, UK, December 2001.

Real-Time Embedded Systems: Model-Based Development, Programming, Testing

• Bandwidth Optimal Data/Service Delivery for Connected Vehicles via Edges. Deepak Gangadharan, Oleg Sokolsky, Insup Lee, BaekGyu Kim, Chung-Wei Lin and Shinichi Shiraishi. In Proceedings of IEEE International Conference on Cloud Computing (CLOUD 2018), San Francisco, CA, USA, July 2018.
• Joint Rate Control and Demand Balancing for Electric Vehicle Charging. Fanxin Kong, Xue Liu, Insup Lee. In Proceedings of 3rd ACM/IEEE International Conference on Internet of Things Design and Implementation (IoTDI 2018), Orlando, FL, USA, April 2018.
• KRS-DGIST: a resilient CPS testbed for radio-based train control: WiP abstract.. Yuchang Won, Buyeon Yu, Jaegeun Park, In-Hee Park, Haegeon Jeong, Jeanseong Baik, Kyungtae Kang, Insup Lee, Kyung-Joon Park, Yongsoon Eun. In Proceedings of 9th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2018), Porto, Portugal, April 2018.
• Platform-based Plug and Play of Automotive Safety Features - Challenges and Directions. Deepak Gangadharan, Jin Hyun Kim, Insup Lee, Oleg Sokolsky, BaekGyu Kim, and Shinichi Shiraishi. In Proceedings of 22nd IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2016), Daegu, South Korea, August 2016 (Invited paper).
• Platform-Based Automotive Safety Features. Deepak Gangadharan, Oleg Sokolsky, Insup Lee, BaekGyu Kim, Chung-Wei Lin, and Shinichi Shiraishi. In Proceedings of SAE 2016 World Congress and Exhibition, Detroit, MI, USA, April 2016.
• Platform-Specific Code Generation from Platform-Independent Timed Models. BaekGyu Kim, Lu Feng, Oleg Sokolsky and Insup Lee. In IEEE Real-Time Systems Symposium (RTSS 2015), San Antonio, TX, USA, December 2015.
• Platform-Specific Timing Verification Framework in Model-Based Implementation. BaekGyu Kim, Lu Feng, Linh T. X. Phan, Oleg Sokolsky, and Insup Lee. In Proceedings of Design, Automation & Test in Europe (DATE 2015), Grenoble, France, March 2015.

• Architecture-Centric Software Development for Cyber-Physical Systems. Oleg Sokolsky, Miroslav Pajic, Nicola Bezzo, and Insup Lee. In Proceedings of First Workshop on Cyber-Physical System Architectures and Design Methodologies (CPSArch 2014), New Delhi, India, October 2014.
• Towards Assurance Cases for Resilient Control Systems. James Weimer, Oleg Sokolsky, Nicola Bezzo, and Insup Lee. In Proceedings of 2nd International Conference on Cyber-Physical Systems, Networks, and Applications (CPSNA 2014), Hong Kong, China, August 2014.
• From Requirements to Code: Model Based Development of A Medical Cyber Physical System. Anitha Murugesan, Michael Whalen, Sanjai Rayadurgam, John Komp, Lian Duan, Mats Heimdahl, Baek-Gyu Kim, Oleg Sokolsky and Insup Lee. In Proceedings of Joint event of the Fourth Symposium on Foundations of Health Information Engineering and Systems (FHIES) and the Software Engineering in Healthcare (SEHC) workshop (FHIES/SEHC '14), Washington, D.C., July 2014.
• A Layered Approach for Testing Timing in the Model-Based Implementation. BaekGyu Kim, Hyeon I. Hwang, Taejoon Park, Sang H. Son, and Insup Lee. In Design, Automation and Test in Europe (DATE 2014), Dresden, Germany, March 2014.
• Platform-Dependent Code Generation for Embedded Real-Time Software. BaekGyu Kim, Linh T.X. Phan, Oleg Sokolsky and Insup Lee. In International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2013), Montreal, Canada, September/October 2013.
• From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study. Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam. In 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012). Beijing, China, April 2012.
• Video Quality Driven Buffer Sizing via Frame Drops. Deepak Gangadharan, Linh T.X. Phan, Samarjit Chakraborty, Roger Zimmermann, and Insup Lee. In 17th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA). Toyama, Japan, August 2011.
• Modeling Buffers with Data Refresh Semantics in Automotive Architectures. Linh T.X. Phan, Reinhard Schneider, Samarjit Chakraborty, and Insup Lee. In 10th International Conference on Embedded Software (EMSOFT 2010), Scottsdale, Arizona, October 2010. (Best Paper Candidate)
• Automated Test Coverage Measurement for Reactor Protection System Software implemented in Function Block Diagram. Eunkyoung Jee, Suin Kim, Sungdeok Cha, and Insup Lee. In 29th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2010), Vienna, Austria, September 2010.
• A Safety-Assured Development Approach for Real-Time Software. Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky, and Insup Lee. In 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2010), Macau, China, August 2010.
• Resource Scopes: Toward Language Support for Compositional Determinism, Madhukar Anand, Sebastian Fischmeister, and Insup Lee, Proceedings of the 12th IEEE International Symposium on Object/component/service-oriented Real-time distributed Computing(ISORC 2009), Tokyo, Japan, March 2009.
• Robust and Sustainable Schedulability Analysis of Embedded Software, Madhukar Anand and Insup Lee, Proceedings of the ACM SIGPLAN/SIGBED 2008 Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008), Tucson, AZ, Jun 2008.
• A design framework for real-time embedded systems with code size and energy constraints, Sheayun Lee, Insik Shin, Woonseok Kim, Insup Lee, Sang L. Min, ACM Transactions on Embedded Computing Systems (TECS), vol 7, no 2, February 2008.
• Robust Test Generation and Coverage for Hybrid Systems, A Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, and George Pappas, Proceedings of 10th International Conference on Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy, April 2007, pp. 329-342.
• Formal Modeling and Analysis of AFDX Frame Management Design, Madhukar Anand, Samar Dajani-Brown, Steve Vestal, and Insup Lee, Proceedings of the 9th IEEE International Symposium onObject-oriented Real-time Distributed Computing (ISORC 2006),Gyeongiu, Korea, April 2006.
• Abstract Slicing: A New Approach to Program Slicing Based on Abstract Interpretation and Model Checking, Hyoung Seok Hong, Insup Lee, and Oleg Sokolsky, 5th International Workshop on Source Code Analysis and Manipulation (SCAM), Budapest, Hungary, September/October 2005.
• Specification-based Testing with Linear Temporal Logic, Li Tan, Oleg Sokolsky, and Insup Lee, Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration (IRI 2004), Las Vegas, Nevada, USA, November 2004.
• A Design Approach for Real-Time Embedded Systems with Energy and Code Size Constraints, Insik Shin, Insup Lee, and Sang Lyul Min Proceedings of the 10th Real-time and Embedded Computing Systems and Applications Conference, RTCSA 2004, Gothenburg, Sweden, August 2004.
• Testing and Monitoring Model-based Generated Program, Li Tan, Jesung Kim, and Insup Lee, Proceeding of Runtime Verification Workshop (RV'03), Boulder, Colorado, July 2003.
• Data Flow Testing as Model Checking, Hyoung Seok Hong, Sung Deok Сha, Insup Lee, Oleg Sokolsky, and Hasan Ural, Proceedings of ICSE'03, Portland, Oregon, May 2003.
• Embedded System Design Framework for Minimizing Code Size and Guaranteeing Real-Time Requirements, Insik Shin, Insup Lee, Sang Lyul Min, Proceedings of the 23rd IEEE Real-Time Systems Symposium, RTSS 2002, Austin, TX, December 2002.
• A Temporal Logic Based Theory of Test Coverage and Generation, Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, and Hasan Ural, International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002), Grenoble, France, April 2002.
• Automatic Test Generation from Statecharts Using Model Checking, Hyoung Seok Hong, Insup Lee, Oleg Sokolsky and Sung Deok Сha, Proceedings of FATES'01, Workshop on Formal Approaches to Testing of Software, August 2001. BRICS Notes Series, NS-01-4, pp. 15-30.
• An Efficient State Space Generation for the Analysis of Real-time Systems, Inhye Kang, Insup Lee, and Young Si Kim, IEEE Transactions of Software Engineering, Vol. 26, No. 5, 2000.
• Verification of the Redundancy Management System for Space Launch Vehicle, Oleg Sokolsky, Mohamed Younis, Insup Lee, Hee-Hwan Kwak, and JeffZhou, Proceedings of RTAS'98, Jun 1998.
• Automatic Test Generation for the Analysis of a Real-Time System: Case Study, Duncan Clarke and Insup Lee, Proceedings of 3rd IEEE Real-Time Technology and Applications Symposium (RTAS'97), Jun 1997.
• Automatic Generation of Tests for Timing Constraints from Requirements, Duncan Clarke and Insup Lee, Proceedings of WORDS'97: IEEE 3rd International Workshop on Object-oriented Real-time Dependable Systems, Feb 1997.
• The Integrated Specification and Analysis of Functional, Temporal, and Resource Requirements, Hanêne Ben-Abdallah, Insup Lee and Young Si Kim, Proceedings of the International Symposium on Requirements Engineering, Anapolis, MD, Jan 1997.
• An Efficient State Space Generation for the Analysis of Real-time Systems, Inhye Kang and Insup Lee, Proceedings of International Symposium on Software Testing and Analysis, 1996.
• A Hybrid Approach to Formal Verification Applied to an ATM Switching System, Duncan Clarke and Insup Lee, University of Pennsylvania Department of Computer and Information Science Technical Report MS-CIS-96-04, 1996.
• Testing Real-Time Constraints in a Process Algebraic Setting, Duncan Clarke and Insup Lee, Proceedings of the 17th International Conference on Software Engineering, 1995.
• State Minimization for Concurrent System Analysis Based on State Space Exploration, Inhye Kang and Insup Lee, Proceedings of Conference on Computer Assurance, 1994.
• RTC: Language Support for Real-Time Concurrency, Victor Wolfe, Susan Davidson and Insup Lee, Real-Time Systems, Volume 5, Number 1, 1993, pp. 63-87.
• Timed Atomic Commitment, Susan B. Davidson, Insup Lee, Victor Wolfe, IEEE TRANSACTIONS ON COMPUTERS, VOL. 40, NO. 5, MAY 1991.
• A Performance Analysis of Timed Synchronous Comunication Primitives, Insup Lee, Susan B. Davidson, IEEE TRANSACTIONS ON COMPUTERS, VOL. 39, NO. 9, SEPTEMBER 1990.
• Motivating Time As A First Class Entity, Insup Lee, Susan Davidson, and Victor Wolfe, University of Pennsylvania Department of Computer and Information Science Technical Report MS-CIS-87-54, Aug. 1987. (Revised Oct 1987).
• Adding Time to Synchronous Process Communications, Insup Lee, Susan B. Davidson, IEEE TRANSACTIONS ON COMPUTERS, VOL. C-36, NO. 8, August 1987 .
• Language Constructs for Distributed Real-Time Programming, Insup Lee and Vijay Gehlot, Proceedings of 6th Real-Time Systems Symposium (RTSS85), San Diego, California, Dec. 1985.
• A Programming System for Distributed Real-Time Applications, Insup Lee, Proceedings of 5th IEEE Real-Time Systems Symposium (RTSS84), Austin, Texas, December 1984.

Formal Methods in Safety-Critical Systems (Real-Time, Hybrid, and Probabilistic Systems)

• Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning. Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee. Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV), Los Angeles, CA, July 2021.
• Verifying the Safety of Autonomous Systems with Neural Network Controllers. Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. ACM Transactions on Embedded Computing Systems (TECS) 20, Vol 1, Num 1, pp 1-26, December 2020.
• Detecting Security Leaks in Hybrid Systems with Information Flow Analysis. Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, and Rajeev Alur. In Proceedings of 17th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MemoCODE 2019), San Diego, CA, USA, October 2019. (Best Paper Award).
• LCV: A Verification Tool for Linear Controller Software. Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee. In Proceedings of Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee, Prague, Czech Republic, April 2019.
• Process Algebraic Approach to the Schedulability Analysis and Workload Abstraction of Hierarchical Real-Time Systems. Junkil Park, Insup Lee, Oleg Sokolsky, Dae Yon Hwang, Sojin Ahn, Jin-Young Choi, and Inhye Kang. In Journal of Logical and Algebraic Methods in Programming (JLAMP), Volume 92, pp.1-18, November 2017.
• Automatic Verification of Finite Precision Implementations of Linear Controllers. Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee. In Proceedings of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Uppsala, Sweden, April 2017.
• Scalable Verification of Linear Controller Software. Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. In Proceedings of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, The Netherlands, April 2016.
• A Modal Specification Theory for Timing Variability. Andrew King, Oleg Sokolsky, and Insup Lee. In University of Pennsylvania Department of Computer and Information Science Technical Report, No. MS-CIS-13-11, November 2013.
• PADS: An approach to modeling resource demand and supply for the formal analysis of hierarchical scheduling. Anna Philippou, Insup Lee, and Oleg Sokolsky. In Theoretical Computer Science, Volume 413, Issue 1, 2012, pp.2-20. Manuscript Number: TCS-D-10-00731R2, January 2012.
• A Process Algebraic Framework for Modeling Resource Demand and Supply. Anna Philippou, Insup Lee, Oleg Sokolsky, and Jin-Young Choi. In 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), IST Austria, Klosterneuburg, Austria, September 2010.
• Generating Reliable Code from Hybrid-Systems Models. Madhukar Anand, Sebastian Fischmeister, Yerang Hur, Jesung Kim, and Insup Lee. In IEEE Transactions on Computers, Vol. 59(9) pp. 1281--1294, September, 2010.
• Model-based Programming of Modular Robots. David Arney, Sebastian Fischmeister, Insup Lee, Yoshihito Takashima, Mark Yim. In 13th IEEE International Symposium on Object/component/service-oriented Real-time Distributed Computing (ISORC 2010), Carmona, Spain, May 2010.
• Process-Algebraic Interpretation of AADL Models, Oleg Sokolsky, Insup Lee, and Duncan Clarke, 14th International Conference on Reliable Software Technologies (Ada-Europe 2009), Brest, France, LNCS 5570, pp. 222-236, June 2009.
• Resources in Process Algebra, Insup Lee, Anna Philippou, Oleg Sokolsky, Journal of Logic and Algebraic Programming, Vol. 72, pp. 98-122, May/June 2007.
• Robust Test Generation and Coverage for Hybrid Systems, A Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, and George Pappas, Proceedings of 10th International Conference on Hybrid Systems: Computation and Control (HSCC 2007), Pisa, Italy, April 2007, pp. 329-342.
• Compositional modeling for refinement for hierarchical hybrid systems, Rajeev Alur, Radu Grosu, Insup Lee, and Oleg Sokolsky, The Journal of Logic and Algebraic Programming, Volume 68, Issue 1-2, 2006, pp. 105-128.
• Unit & Dynamic Typing in Hybrid Systems Modeling with CHARON, Madhukar Anand, Insup Lee, Oleg Sokolsky, and George Pappas, Proceedings of the IEEE International Symposium onComputer-Aided Control Systems Design (CACSD 2006), Technische Universitet Munchen, Munich, Germany, October 2006.
• Schedulability Analysis of AADL Models, Oleg Sokolsky, Insup Lee, and Duncan Clarke, 14th International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS'06), Island of Rhodes, Greece, April 2006.
• Simulation-Based Graph Similarity, Oleg Sokolsky, Sampath Kannan, and Insup Lee, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Vienna, Austria, LNCS3920, pp. 426-440, March 27-30, 2006.
• R-Charon, a Modeling Language for Reconfigurable Hybrid Systems, Fabian Kratz, Oleg Sokolsky, George J. Pappas, and Insup Lee, Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC 2006), Santa Barbara, CA, USA, LNCS 3927, pp. 392-406, March 2006.
• Generating Sound and Resource-Aware Code from Hybrid System Models, Madhukar Anand, Jesung Kim, Sebastian Fischmeister, and Insup Lee, Proceedings of the 2nd Workshop on Advanced Automotive Softwareand Systems Development (ASWSD 2006), University of California, San Diego, March 2006.
• Distributed Code Generation from Hybrid Systems Models for Timedelayed Multirate Systems, Madhukar Anand, Sebastian Fischmeister, Jesung Kim, and Insup Lee, Proceedings of EMSOFT'05, Jersey City, New Jersey, USA, September 2005.
• Code Generation from Hybrid Systems Models for Distributed Embedded System, Madhukar Anand, Jesung Kim, and Insup Lee, Proceedings of the 8th IEEE International Symposium on Object-oriented Real-time distributed Computing, ISORC'05, Seattle, Washington, May 2005. (Invited Paper)
• Model-based Testing and Monitoring for Hybrid Embedded Systems, Li Tan, Jesung Kim, Oleg Sokolsky, and Insup Lee, Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration (IRI 2004), Las Vegas, Nevada, USA, November 2004.
• Sound Code Generation from Communicating Hybrid Models, Yerang Hur, Jesung Kim, Insup Lee, and Jin-Young Choi, Proceedings of Hybrid Systems: Computation and Control (HSCC04), Philadelphia, PA, LNCS 2939, pp. 432-447, March 2004.
• Generating Embedded Software from Hierarchical Hybrid Models, Rajeev Alur, Franjo Ivancic, Jesung Kim, Insup Lee and Oleg Sokolsky, Proceeding of ACM SIGPLAN Languages, Compilers, and Tools for Embedded Systems (LCTES'03), San Diego, California, June 2003.
• Modular Code Generation from Hybrid Automata based on Data Dependency, Jesung Kim and Insup Lee, Proceedings of The 9th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2003), Washington, DC, May 2003.
• Modeling and Analysis of Power-Aware Systems, Oleg Sokolsky, Anna Philippou,Insup Lee, and Kyriakos Christou, Proceedings of TACAS'03, Warsaw, Poland, April 2003, LNCS 2619, pp. 409-425.
• Hierarchical Modeling and Analysis of Embedded Systems, Rajeev Alur, Thao Dang, Joel Esposito, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George Pappas, and Oleg Sokolsky, Proceedings of IEEE, Vol. 91, No 1, January 2003, pp. 11-28.
• Process Algebraic Modeling and Analysis of Power-Aware Real-Time Systems, Insup Lee, Anna Philippou, and Oleg Sokolsky, Computing and Control Engineering Journal, Vol 13, Number 4, 2002, pp. 180-188.
• A General Resource Framework for Real-Time Systems , Insup Lee, Anna Philippou, and Oleg Sokolsky, Proceedings of the Monterey Workshop, Venice, Italy, October 2002. (Invited Paper)
• Distributed Simulation of Multi-Agent Hybrid Systems, Yerang Hur, Insup Lee, IEEE International Symposium on Object-Oriented Real-time distributed Computing (ISORC), Crystal City, Virginia, USA, April/May 2002.
• Formal Modeling and Analysis of Power-Aware Real-Time Systems, Insup Lee, Anna Philippou, and Oleg Sokolsky, Proceedings of IEEE/IEE Workshop on Real-Time Embedded Systems (RTES'2001),London, UK, December 2001.
• Hiding Resources that Can Fail, Anna Philippou, Oleg Sokolsky, Insup Lee, Rance Cleaveland, and Scott Smolka, Information Processing Letters Volume 80, Issue 1, Oct 2001.
• Hierarchical Hybrid Modeling of Embedded Systems, Rajeev Alur, Thao Dang, Joel Esposito, R. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George Pappas, and Oleg Sokolsky, Proceedings of EMSOFT'01: First Workshop on Embedded Software, Tahoe City, California, USA, Oct 2001. (Invited Paper)
• A Family of Resource-Bound Real-time Process Algebras, Insup Lee, Jin-Young Choi, Hee-Hwan Kwak, Anna Philippou, and Oleg Sokolsky, Proceedings of 21st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'01),Cheju Island, Korea, August 2001. (Invited Paper)
• Characterizing Non-Zenoness on Real-Time Processes, Jitka Stribrna and Insup Lee, Proceedings of Model for Time-Critical Systems (MTCS'01), Aalborg, Denmark, Aug 2001.
• Compositional Refinement for Hierarchical Hybrid Systems, Rajeev Alur, Radu Grosu, Insup Lee, and Oleg Sokolsky, Hybrid Systems: Computation and Control, LNCS 2034, pp. 33-48, March 2001.
• Modular specifications of hybrid systems in CHARON, Rajeev Alur, Radu Grosu, Yerang Hur, Vijay Kumar, and Insup Lee, Hybrid Systems: Computation and Control, LNCS 1790, pp. 6-19, 2000.
• A framework and architecture for multirobot coordination, Rajeev Alur, A. Das, Joel Esposito, R. Fierro, Yerang Hur, G. Grudic, Vijay Kumar, Insup Lee, J. Ostrowski, George Pappas, J. Southall, J. Spletzer, and C. Taylor, Seventh International Symposium on Experimental Robotics-ISER00, Honolulu, Hawaii, Dec. 2000.
• Weak Bisimulation for Probabilistic Systems, Anna Philippou, Insup Lee, and Oleg Sokolsky, Proceedings of CONCUR'00, August 2000.
• Specification and Analysis of Real-Time Systems with PARAGON, Oleg Sokolsky, Insup Lee, and Hanêne Ben-Abdallah, Annals of Software Engineering, Vol. 7, 1999.
• Formal modeling and analysis of hybrid systems: A case study in multi-robot coordination, Rajeev Alur, Joel Esposito, Moonjoo Kim, Vijay Kumar and Insup Lee, Proceedings of FM'99 Toulouse, France, September 1999.
• A Graphical Language for Specifying and Analyzing Real-Time Systems, Hanêne Ben-Abdallah and Insup Lee, Special Issue of Integrated Computer-Aided Engineering on Real-time Engineering Systems, Vol 5, No 4, 1998.
• A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems, Hanêne Ben-Abdallah, Jin-Young Choi, Duncan Clarke, Young Si Kim, Insup Lee and Hong-Liang Xie, Real-Time Systems, Vol 15, 1998.
• Symbolic Schedulability Analysis of Real-time Systems , Hee-Hwan Kwak, Insup Lee, Anna Philippou, Jin-Young Choi and Oleg Sokolsky, IEEE Real-Time Systems Symposium, December 1998.
• Parametric Approach to the Specification and Analysis of Real-time System Designs based on ACSR-VP, Hee-Hwan Kwak, Insup Lee, and Oleg Sokolsky, Proceedings 1998 ARO/ONR/NSF/DARPA Monterey Workshop on Engineering Automation for Computer Based Systems, Carmel-By-The-Sea, CA, Oct 27-29, 1998.
• Probabilistic Resource Failure in Real-Time Process Algebra , Anna Philippou, Rance Cleaveland, Insup Lee, Scott Smolka, and Oleg Sokolsky, CONCUR '98, September 1998.
• Parallel Algorithms for Relational Coarsest Partition Problems, S.Rajasekaran and Insup Lee, IEEE Transactions on Parallel and Distributed Systems, Vol 9, No 7, July 1998.
• Specifying Failures and Recoveries in PACSR, Anna Philippou, Oleg Sokolsky, Insup Lee, Rance Cleaveland, and Scott Smolka, Proceedings of Workshop on Probabilistic Methods in Verification, Jun 1998.
• Symbolic weak Bisimulation for Value-Passing Calculi, Hee-Hwan Kwak, Jin-Young Choi, Insup Lee and Anna Philippou, University of Pennsylvania Department of Computer and Information Science Technical Report MS-CIS-98-22, May 1998.
• A Process Algebra of Communicating Shared Resources with Dense Time and Priorities, Patrice Bremond-Gregoire and Insup Lee, Theoretical Computer Science, 189 1997.
• A Complete Axiomatization of Finite-state (ACSR) Processes, Patrice Bremond-Gregoire, Jin-Young Choi and Insup Lee, Information and Computation, Nov 1997.
• A Graphical Property Specification Language, Insup Lee and Oleg Sokolsky, Proceedings of 2nd IEEE Workshop on High-Assurance Systems Engineering, Aug 1997.
• Operational Semantics for Visual Simulation in PARAGON, Hanêne Ben-Abdallah, Insup Lee and Oleg Sokolsky, Proceedings of IEEE National Aerospace and Electronics Conference, Jul 1997.
• PARAGON: A Paradigm for the Specification, Verification, and Testing of Real-Time Systems, Hanêne Ben-Abdallah, Duncan Clarke, Insup Lee, and Oleg Sokolsky, IEEE Aerospace Conference, Feb 1997.
• Ordering Processes in a Real-Time Process Algebra, Patrice Bremond-Gregoire, Hanêne Ben-Abdallah and Insup Lee, Proceedings of AMAST 3rd International Workshop on Real-Time Systems, 1996.
• Schedulability and Safety Analysis in the Graphical Communicating Shared Resources, Hanêne Ben-Abdallah, Young Si Kim and Insup Lee, Proceedings of IEEE Workshop on Object-Oriented Real-Time and Dependable Systems, Laguna Beach, CA, Feb 1996.
• A Process Algebraic Method for Real-Time Systems, Insup Lee, Hanêne Ben-Abdallah, and Jin-Young Choi, Formal Methods for Real-Time Computing C.Heitmeyer and D.Mandrioli (eds.), John Wiley & Sons Ltd, 1996.
• VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems, Duncan Clarke, Insup Lee and Hong-Liang Xie, Journal of Computer Software Engineering, 3(2) 1995.
• A Graphical Language with Formal Semantics for the Specification and Analysis of Real-Time Systems, Hanêne Ben-Abdallah, Insup Lee, and Jin-Young Choi, Proceedings of the 16th IEEE Real-Time Systems Symposium, 1995.
• The Specification and Schedulability Analysis of Real-Time Systems using ACSR, Jin-Young Choi, Insup Lee and Hong-Liang Xie, Proceedings of the 16th IEEE Real-Time Systems Symposium, 1995.
• Timing Analysis of Superscalar Processor Programs Using ACSR, Jin-Young Choi, Insup Lee, and Inhye Kang, 11th IEEE Workshop on Real-Time Operating Systems and Software, 1994.
• A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems, Insup Lee, Patrice Bremond-Gregoire and Richard Gerber, Proceedings of the IEEE, Special Issue on Real-Time Systems Jan. 1994, pp. 158-171. (Invited Paper). IEEE Version

Run-time Monitoring and Checking (a la Runtime Verification)

• Compositional Probabilistic Analysis of Temporal Properties over Stochastic Detectors. Ivan Ruchkin, Oleg Sokolsky, James Weimer, Tushar Hedaoo, and Insup Lee. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol 39, Num 11, pp 3288-3299, November 2020.
• Overhead-aware deployment of runtime monitors. Teng Zhang, Greg Eakman, Insup Lee, and Oleg Sokolsky. In Proceedings of 19th International Conference on Runtime Verification (RV 2019), Porto, Portuga, October 2019.
• A Retrospective Look at the Monitoring and Checking (MaC) Framework. Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, and Mahesh Viswanathan. In Proceedings of 19th International Conference on Runtime Verification (RV 2019), Porto, Portuga, October 2019.
• Runtime verification of parametric properties using SMEDL. Teng Zhang, Ramneet Kaur, Insup Lee, and Oleg Sokolsky. In Reactive Systems to Cyber-Physical Systems Lecture Notes in Computer Science, vol 11500, 276-293. September 2019
• Correct-by-construction implementation of runtime monitors using stepwise refinement. Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clement Pit-Claudel, Insup Lee, and Oleg Sokolsky. In Proceedings of International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2018), Beijing, China, September 2018.
• Parameter Invariant Monitoring for Signal Temporal Logic. Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, and Insup Lee. In Proceedings of 21st ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2018), Porto, Portugal, April 2018.
• Monitoring Time Intervals. Teng Zhang, John Wiegley, Insup Lee, and Oleg Sokolsky. In Proceedings of 17th International Conference on Runtime Verification (RV 2017), Seattle, USA, September 2017.
• Monitoring Assumptions in Assume-Guarantee Contracts. Oleg Sokolsky, Teng Zhang, Insup Lee, and Michael McDougall. In Proceedings of Workshop on Pre- and Post-Deployment Verification Techniques (PrePost@IFM), Reykjavik, Iceland, June 2016.
• A Hybrid Approach to Causality Analysis. Shaohui Wang, Yoann Geoffroy, Gregor Gossler, Oleg Sokolsky, and Insup Lee. In 15th International Conference on Runtime Verification (RV 2015), Vienna, Austria, September 2015.
• A Causality Analysis Framework for Component-based Real-time Systems. Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor G ossler, Oleg Sokolsky, and Insup Lee. In 13th International Conference on Runtime Verification (RV '13), INRIA Rennes, France, September 2013.
• Contract-based Blame Assignment by Trace Analysis. Shaohui Wang, Anaheed Ayoub, Radoslav Ivanov, Oleg Sokolsky, and Insup Lee. In 2nd ACM International Conference on High Confidence Networked Systems (HiCoNS 2013). Philadelphia, PA, April 8 - 11, 2013.
• Runtime Verification of Traces under Recording Uncertainty. Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky, and Insup Lee. In Proceedings of the 2nd International Conference on Runtime Verification (RV 2011), San Francisco, CA, October 2011.
• DMaC: Distributed Monitoring and Checking, Wenchao Zhou, Oleg Sokolsky, Boon Thau Loo, and Insup Lee, 9th International Workshop on Runtime Verification (RV 2009), Grenoble, France, June 2009.
• Checking Traces for Regulatory Conformance, Nikhil Dinesh, Aravind K. Joshi, Insup Lee, and Oleg Sokolsky, Proceedings of the Eighth Workshop on Runtime Verification (RV'08), Satellite workshop of ETAPS'08, Budapest, Hungary, March 2008.
• Statistical Runtime Checking of Probabilistic Properties, Usa Sammapun, Insup Lee, Oleg Sokolsky, and John Regehr, Proceedings of the 7th Workshop on Run-time Verification, Vancouver, B.C., Canada, LNCS 4839, pp. 164-175, March 2007.
• Checking Correctness At Runtime using Real-Time Java, Usa Sammapun, Insup Lee and Oleg Sokolsky, Proceedings of the 3rd Workshop on Java Technologies for Real-time and Embedded Systems (JTRES'05), San Diego, CA, October 2005.
• RT-MaC: Runtime Monitoring and Checking of Quantitative and Probabilistic Properties, Usa Sammapun, Insup Lee and Oleg Sokolsky, Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA'05, Hong Kong, August 2005.
• Run-Time Checking of Dynamic Properties, Oleg Sokolsky, Usa Sammapun, Insup Lee, and Jesung Kim, Proceedings of the Fifth Workshop on Runtime Verification, RV'05,The University of Edinburgh, Scotland, UK, July 2005.
• Java-MaC: A Run-time Assurance Tool for Java Programs, Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan Formal Methods in Systems Design, Vol 24, No 2, March 2004.
• Simulation of Simultaneous Events in Regular Expressions for Run-Time Verification, Usa Sammapun, Arvind Easwaran, Insup Lee, Oleg Sokolsky, Proceeding of Runtime Verification Workshop (RV'04), Barcelona, Spain, April 2004.
• Regular Expressions for Run-Time Verification, Usa Sammapun, Oleg Sokolsky, Proceedings of the 1st International Workshop on Automated Technology for Verification and Analysis (ATVA'03), Taipei, Taiwan, December 2003.
• Computational Analysis of Run-time Monitoring - Fundamentals of Java-MaC, Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan,  2nd International Workshop on Run-time Verification. Copenhagen, Denmark, July 26, 2002;Electronic Notes in Theoretical Computer Science 70 No. 4.
• Monitoring, Checking, and Steering of Real-Time Systems, Moonjoo Kim, Insup Lee, Usa Sammapun, Jangwoo Shin, Oleg Sokolsky, 2nd International Workshop on Run-time Verification.Copenhagen, Denmark, July 2002; Electronic Notes in Theoretical Computer Science 70 No. 4.
• Verisim: Formal Analysis of Network Simulations, Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan, IEEE Transactions on Software Engineering, Vol. 28, No. 2, Feb 2002, pp. 129-145. (Special Issue on Selected Papers from International Symposium on Sotware Testing and Analysis, 2000).
• Java-MaC: a Run-time Assurance Tool for Java, Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, 1st International Workshop on Run-time Verification. Paris, France, July 2001 Electronic Notes in Theoretical Computer Science 55 No. 2 (2001).
• Verisim: Formal Analysis of Network Simulations, Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan, Proceedings of the International Symposium on Software Testing and Analysis, August 2000.
• Distributed Spatial Control and Global Monitoring of Mobile Agents, Diana Gordon, William Spears, Insup Lee, and Oleg Sokolsky, Proceedings. 1999 International Conference on Information, Intelligence, and Systems, November 1999, pp. 681-688.
• Runtime Assurance Based On Formal Specifications, Insup Lee, Sampath Kannan, MoonjooKim, Oleg Sokolsky, Mahesh Viswanathan, Proceedings of International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, June/July 1999.
• Formally Specified Monitoring of Temporal Properties, MoonjooKim, Mahesh Viswanathan, Insup Lee, HanêneBen-Abdellah, Sampath Kannan, and Oleg Sokolsky, Proceedings of the European Conference on Real-Time Systems, York, UK, June 1999.
• A Monitoring and Checking Framework for Run-time Correctness Assurance, Insup Lee, HanêneBen-Abdellah, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, Mahesh Viswanathan, Proceedings 1998 Korea-U.S. Technical Conference on Strategic Technologies, Vienna, VA, Oct 22-24, 1998. (Invited Paper)

Position Papers

• Cyber Physical Systems: The Next Computing Revolution. Ragunathan (Raj) Rajkumar, Insup Lee, Lui Sha, and John Stankovic. In 47th Design Automation Conference (DAC 2010), CPS Demystified Session, Anaheim, CA, June 2010. (Invited Paper) - ACM Portal
• Medical Cyber Physical Systems. Insup Lee and Oleg Sokolsky. In 47th Design Automation Conference (DAC 2010), CPS Demystified Session, Anaheim, CA, June 2010. (Invited Paper) ACM Portal
• High-Confidence Medical Device Software and Systems, Insup Lee, George J. Pappas, RanceCleaveland, JohnHatcliff, Bruce H.Krogh, Peter Lee, HarveyRubin, and Lui Sha, IEEE Computer, Volume 39, Issue 4, April 2006, pp. 33-38.
• Opportunities and obligations for physical computing systems, John A. Stankovic, Insup Lee, Aloysius Mok, and Raj Rajkumar, Computer, Volume 38, Issue 11, November 2005, pp. 23-31.

Relevant Publications

• Google Scholar
• DBLP


• PRECISE Publications
• RTG Publications