Shaohui Wang (aka Vincent)

Department of Computer and Information Science
School of Engineering and Applied Science
University of Pennsylvania
Levine Hall 514, 3330 Walnut Street
Philadelphia, PA 19104, USA
shaohui@seas.upenn.edu

I’m a Ph.D. student in Department of Computer and Information Science at Penn. I am affiliated with the PRECISE center and the RTG group. I work with Professor Insup Lee and Professor Oleg Sokolsky.

Previously I was an undergraduate in the major of Information and Computing Science in Department of Mathematical Sciences at Tsinghua University, and then a graduate student in the major of Mathematical Logic in Department of Philosophy at Peking University.

My research interest lies in topics in formal methods, especially formal specification, verification, and algorithms and applications of model checking techniques. More broadly, I'm interested in studies which help build reliable, safe, and efficient software systems, such as topics appeared in software engineering, computer aided verification and theory of programming languages. I am/was involved in the following projects:

  • Medical Device Data Loggers
  • Causality Analysis for Medical Device Interoperability
  • Runtime Monitoring and Runtime Verification
  • Assurance and Safety Cases for Medical Devices
  • Medical Devices Plug and Play
  • The Pacemaker Challenge
  • Model-Extraction via Program Analysis

  • Shaohui Wang, Yoann Geoffroy, Gregor Goessler, Oleg Sokolsky, and Insup Lee. (2015)
    A Hybrid Approach to Causality Analysis.
    In Proceedings of RV’15, the 6th International Conference on Runtime Verification.
    pdf
  • Shaohui Wang. (2013)
    Advances in Theory and Applications of Token Causality in Trace Analysis.
    Write-up for partial fulfillment of the WPE II requirement.
    pdf, slides
  • Shaohui Wang, Anaheed Ayoub, BaekGyu Kim, Gregor Goessler, Oleg Sokolsky, and Insup Lee. (2013)
    A Causality Analysis Framework for Component-based Real-time Systems.
    In Proceedings of RV’13, the 4th International Conference on Runtime Verification.
    pdf
  • Shaohui Wang, Anaheed Ayoub, Radoslav Ivanov, Oleg Sokolsky, and Insup Lee. (2013).
    Contract-based Blame Assignment by Trace Analysis.
    In Proceedings of HiCoNS’13, the 2nd International Conference on High Confidence Networked System.
    pdf
  • Shaohui Wang, Srinivasan Dwarakanathan, Oleg Sokolsky, and Insup Lee. (2012).
    High-level model extraction via symbolic execution.
    Technical Report MS-CIS-12-04, University of Pennsylvania.
    pdf
  • Shaohui Wang, Anaheed Ayoub, Oleg Sokolsky, and Insup Lee. (2011).
    Runtime Verification of Traces Under Recording Uncertainty.
    In Proceedings of RV’11, the 2nd International Conference on Runtime Verification.
    pdf
  • Eunkyoung Jee, Shaohui Wang, Jeong Ki Kim, Jaewoo Lee, Oleg Sokolsky, and Insup Lee. (2010).
    A Safety-assured Development Approach for Real-time Software.
    In 16th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), pages 133-142.
    pdf
  • Vivien Chinnapongse, Insup Lee, Oleg Sokolsky, Shaohui Wang, and Paul L. Jones. (2009).
    Model-based testing of GUI-driven applications.
    In Software Technologies for Embedded and Ubiquitous Systems, volume 5860 of LNCS, pages 203-214. Springer.
    pdf
I have been external reviewer for the following conferences/journals.
  • ASSURE’13: 1st International Workshop on Assurance Cases for Software-Intensive Systems
  • ATVA’09, ATVA’10, ATVA’11, ATVA’12, ATVA’13, ATVA’14: International Symposium on Automated Technology for Verification and Analysis
  • BSN’10: International Conference on Wearable and Implantable Body Sensor Networks
  • DATE’12, DATE’15: Design, Automation, Test & Test in Europe
  • ECRTS’10: Euromicro Conference on Real-Time Systems
  • EMSOFT’12, EMSOFT’14, EMSOFT’15: International Conference on Embedded Software
  • FM’09: 16th International Symposium on Formal Methods
  • Formal Methods in System Design (journal)
  • FORMATS’09: 7th International Conference on Formal Modeling and Analysis of Timed Systems
  • HEALTHTECH’13: 2013 USENIX Workshop on Health Information Technologies
  • ICCAD’11: The International Conference on Computer-Aided Design
  • ICCPS’10, ICCPS’12: International Conference on Cyber-Physical Systems
  • ICFEM’12: International Conference on Formal Engineering Methods
  • ICHI’13: The IEEE International Conference on Healthcare Informatics
  • IHI’12: ACM SIGHIT International Health Informatics Symposium
  • ISORC’10, ISORC’12: International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing
  • LCTES’09: ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems
  • MPE: Mathematical Problems in Engineering (journal)
  • NFM’12: The 4th NASA Formal Methods Symposium
  • RTAS’11, RTAS’15: The 17th IEEE Real-Time and Embedded Technology and Applications Symposium
  • RTCSA’10, RTCSA’11: IEEE International Conference on Embedded and Real-Time Computing Systems and Applications
  • RTSS’09, RTSS’10, RTSS’11, RTSS’12, RTSS’13: IEEE Real-Time Systems Symposium
  • RV’09, RV’11, RV’12, RV’13, RV’14: International Conference on Runtime Verification
  • SEHC’12, SEHC’14: 4th International Workshop on Software Engineering in Health Care
  • SMC: IEEE Transactions on Systems, Man, and Cybernetics (journal)
  • SPIN’13: The International SPIN Symposium on Model Checking of Software
  • SRDS’12: 31st IEEE International Symposium on Reliable Distributed Systems
  • STTT: International Journal on Software Tools for Technology Transfer (journal)
  • TECS’09: ACM Transactions on Embedded Computing Systems (journal)
  • TOSEM’11: ACM Transactions on Software Engineering and Methodology (journal)
I have been involved in the following conference-organizing events.
  • CPSWEEK’13: Cyber-Physical Systems Week
  • ICHI’13: The IEEE International Conference on Healthcare Informatics
Awards
  • Peking University: Guanghua Scholarship. 2006.
  • University of Pennsylvania: Doctoral Fellowship. 2008—now.
  • Fall 2012 (University of Pennsylvania)
    Teaching Assistant for CIS 441/541
    Embedded Software for Life-Critical Applications
    • Office Hours: By Appointment
    • Everything is available at Blackboard.
    • We also use ThinkBinder for class discussions.
  • Fall 2011 (University of Pennsylvania)
    Teaching Assistant for CIS 441/541
    Embedded Software for Life-Critical Applications
  • Fall 2010 (University of Pennsylvania)
    Teaching Assistant for CIS 441
    Embedded Software for Life-Critical Applications
  • Spring 2010 (University of Pennsylvania)
    Teaching Assistant for CIS 541
    Embedded and Cyber Physical Systems
  • Fall 2009 (University of Pennsylvania)
    Teaching Assistant for CIS 140
    Introduction to Cognitive Science
    • Office Hours: Monday 1pm-2pm & Tuesday 11am-12pm @ Levine 612
    • All course materials, homeworks, information are available at Blackboard.
    • Last year’s Course Webpage
  • Fall 2005 (Peking University)
    Teaching Assistant for Mathematical Logic