Shengchao Qin

Professor of Computer Science (Chair)

School of Computing, Engineering, & Digital Technologies,
University of Teesside
Tees Valley, TS1 3BX
U.K.


Research

Research Interests

In general: formal methods; programming languages; software engineering; cybersecurity; AI.

Recent & more specific: program analysis and verification, software verfication and validation, fuzz testing, trustworthy AI.

Research/Work Experience

  • Professor (Chair) of Computer Science (6.2011 - ), Teesside University
  • Associate Dean (Research & Innovation) (8.2016-9.2019), SCM->SCMA->SCDT, Teesside University
  • Reader of Computer Science (6.2010-5.2011), School of Computing, Teesside University
  • University Lecturer (1.2005-5.2010), Department of Computer Science, Durham University
  • Research Fellow (7.2002 - 12.2004), Singapore-MIT Alliance, National University of Singapore
  • PhD student & Research/Teaching Assistant (9.1997 - 7.2002), Peking University
  • BSc student (9.1993-7.1997), Peking University
  • Selected Publications

    [More Publications]           [DBLP]           [Google Scholar]           [ORCID]

  • Y. Tao, J. Jiang, Y. Liu, Z. Xu, S. Qin. Understanding Performance Concerns in the API Documentation of Data Science Libraries. The 35th IEEE/ACM International Conference on Automated Software Engineering (ASE 2020). 21-25 September 2020, Melbourne, Australia. Held virtually in September 2020.
  • C. Wen, H. Wang, Y. Li, S. Qin, Y. Liu, Z. Xu, H. Chen, X. Xie, G. Pu, T. Liu. MemLock: Memory Usage Guided Fuzzing . 42nd International Conference on Software Engineering (ICSE 2020), 6-11 July 2020, Seoul, South Korea (held virtually).
  • H. Wang, X. Xie, Y. Li, C. Wen, Y. Li, Y. Liu, S. Qin, H. Chen, Y. Sui. Typestate-Guided Fuzzer for Discovering Use-after-Free Vulnerabilities . 42nd International Conference on Software Engineering (ICSE 2020), 6-11 July 2020, Seoul, South Korea (held virtually).
  • C. Huang, X. Chen, E. Tang, M. He, L. Bu, S. Qin, Y. Zeng. Navigating Discrete Difference Equation Governed WMR by Virtual Linear Leader Guided HMPC. International Conference on Robotics and Automation (ICRA 2020). 31 May - 4 June 2020. Paris, France. Held virtually between 31 May - 31 August 2020.
  • H. Wang, X. Xie, S.-W. Lin, Y. Lin, Y. Li, S. Qin, Y. Liu and T. Liu. Locating Vulnerabilities in Binaries via Memory Layout Recovering. The 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2019). Tallinn, Estonia. 26-30 Aug 2019. (Also available at TU Pure Portal)
  • L. H. Pham, Q. L. Le, Q.-S. Phan, J. Sun and S. Qin. Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation. International Symposium on Automated Technology for Verification and Analysis (ATVA 2019). 28-31 October 2019. Taipei City.
  • J. Wang, J. Sun, S. Qin and C. Jegourel. Automatically 'Verifying' Discrete-Time Complex Systems through Learning, Abstraction and Refinement. (DOI). IEEE Transactions on Software Engineering. 47(1):189-203, 2021. (Available at TU Pure Portal)
  • Z. Xu, C. Wen and S. Qin. Type Learning for Binaries and its Applications. IEEE Transactions on Reliability. 68(3):893-912. September 2019. (Available at TU Pure Portal)
  • S. Qin, G. He, W.-N. Chin, F. Craciun, M. He, Z. Ming. Automated Specification Inference in a Combined Domain via User-Defined Predicates . Science of Computer Programming. Elsevier. (DOI)
  • X. Wang, J. Sun, T. Wang and S. Qin. Language Inclusion Checking of Timed Automata with Non-zenoness. IEEE Transactions on Software Engineering. 43(11):995-1008 (2017). (DOI)
  • Richard Banach, Michael Butler, Shengchao Qin, Huibiao Zhu. Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines. Science of Computer Programming. Volume 139. Pages 1--35. June 2017. Elsevier. (DOI)
  • J. Sun, H. Xiao, Y. Liu, S.-W. Lin and S. Qin. TLV: Abstraction through Testing, Learning and Validation. The Joint Meeting of ACM SIGSOFT Symposium on the Foundations of Software Engineering and the European Software Engineering Conference (FSE/ESEC 2015). Bergamo, Italy. 2-4 Sep 2015.
  • T. C. Le, S.Qin and W.-N. Chin. Termination and Non-termination Specification Inference. The 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'15), Pages 489-498. Portland, Oregon, United States, June 13 - 17, 2015. The ACM Press.
  • R. Banach, M. Butler, S. Qin, N. Verma, and H. Zhu. Core Hybrid Event-B I: Single Hybrid Event-B Machines. Science of Computer Programming. (online)
  • H. Zhu, J. He, S. Qin and P. J. Brooke. Denotational semantics and its algebraic derivation for an event-driven system-level language. Formal Aspects of Computing. 27(1): 133-166 (2015).
  • Q. L. Le, C. Gherghina, S. Qin and W.-N. Chin. Shape Analysis via Second-Order Bi-Abduction. 26th International Conference on Computer Aided Verification (CAV 2014). LNCS 8559. Pages:52-68. July 18-22, 2014. Vienna, Austria. (online demo)
  • S. Qin, G. He, C. Luo, W.-N. Chin, and H. Yang. Automatically Refining Partial Specifications for Heap-Manipulating Programs. Science of Computer Programming. 82 (2014):56-76. Elsevier. (online)
  • S. Qin, G. He, C. Luo, W.-N. Chin, and X. Chen. Loop Invariant Synthesis in a Combined Abstract Domain. Journal of Symbolic Computation. 50 (2013):386-408. Elsevier. (online)
  • L. Zou, N. Zhan,S. Wang, M. Franzle, and S. Qin. Verifying Simulink Diagrams via a Hybrid Hoare Logic Prover. International Conference on Embedded Software (EMSOFT'13). Sept 29 - Oct 04, 2013. Montreal, Canada. The ACM Press.
  • W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated Verification of Shape, Size and Bag Properties via User-Defined Predicates in Separation Logic. Science of Computer Programming. 77(2012):1006-1036. Elsevier. (Available online)
  • H. Zhu, F. Yang, J. He, J. Bowen, J. W. Sanders, and S. Qin. Linking Operational Semantics and Algebraic Semantics for a Probabilistic Timed Shared-Variable Language. Journal of Logic and Algebraic Programming. 81(1):2-25. 2012. Elsevier. (Available online)
  • W.-N. Chin, C. Gherghina, R. Voicu, Q. L. Le, F. Craciun and S. Qin. A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. Computer-Aided Verification (CAV 2011). Snowbird, Utah. July 2011. Lecture Notes in Computer Science. Springer.
  • S. Qin, C. Luo, W.-N. Chin, and G. He. Automatically Refining Partial Specifications for Program Verification. Formal Methods (FM2011). Limerick, Ireland. June 2011. Lecture Notes in Computer Science. Springer.
  • C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured Specifications for Better Verification of Heap-Manipulating Programs. Formal Methods(FM2011). Limerick, Ireland. June 2011. Lecture Notes in Computer Science. Springer.
  • C. Luo, F. Craciun, S. Qin, G. He, and W.-N. Chin. Verifying Pointer Safety for Programs with Unknown Calls. Journal of Symbolic Computation. 45 (11): 1163-1183. Elsevier. (Available online)
  • J. S. Dong, P. Hao, S. Qin, J. Sun and Wang Y., Timed Automata Patterns. IEEE Transactions on Software Engineering. 34 (6): 844-859. 2008.
  • W.-N. Chin, C. David, H. H. Nguyen, and S. Qin, Enhancing Modular OO Verification with Separation Logic. The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08). San Francisco, USA. January 10-12, 2008.
  • H.-H. Nguyen, C. David, S. Qin, W.-N. Chin, Automated Verification of Shape and Size Properties via Separation Logic. VMCAI'07. Nice France. January 2007. Lecture Notes in Computer Science 4349, Springer-Verlag.
  • W.-N. Chin, H. H. Nguyen, S. Qin, and M. Rinard, Memory Usage Verification for OO Programs. The 12th International Static Analysis Symposium (SAS 05), London, UK. September 2005. Lecture Notes in Computer Science 3672, Springer-Verlag. ISBN: 3-540-28584-9.
  • W.-N. Chin, S.-C. Khoo, S. Qin, C. Popeea, and H. H. Nguyen, Verifying Safety Policies with Size Properties and Alias Controls. 27th International Conference on Software Engineering (ICSE 05), 15-21 May, 2005. St. Louis, Missouri, USA. ISBN:1-59593-963-2.
  • W.-N. Chin, F. Craciun, S. Qin and M. Rinard, Region Inference for an Object-Oriented Language, ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (PLDI 04), June 9-11, 2004, Washington, DC, USA. ISBN:1-58113-807-5.
  • S. Qin, J. S. Dong and W.-N. Chin, A Semantic Foundation for TCOZ in Unifying Theories of Programming, Formal Methods (FM 03), Pisa, Italy, Sep. 2003. Lecture Notes in Computer Science 2805, Springer-Verlag. ISBN: 3-540-40828-2.

  • Externally Funded Research Projects


    Professional Activities/Services

    Research Council Service

  • Full Member of the EPSRC Peer Review College
  • Member of UKRI Future Leaders Fellowship Peer Review College
  • Professional Membership

  • Fellow of the Higher Education Academy
  • Senior Member of the ACM
  • Senior Member of the IEEE
  • Member of the ACM SIGPLAN
  • Program Committee (Co-)Chair

  • FROM 2020: 4th Working Formal Methods Symposium. Babes-Bolyai University, Romania. 4-6 September 2020.
  • ICFEM 2019: 21st International Conference on Formal Engineering Methods , Shenzhen, China.. 5-9 Nov 2019.
  • TASE 2019: 13th International Symposium on Theoretical Aspects of Software Engineering, Guilin, China, 29-31 July 2019.
  • ICFEM 2011: 13th International Conference on Formal Engineering Methods , Radisson Blu Hotel Durham, UK. 26-28 Oct 2011.
  • UTP 2010:3rd International Symposium on Unifying Theories of Programming, Shanghai, China, 15-16 November 2010.
  • TASE 2009: 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, 29-31 July 2009.
  • Program Committee Membership

  • More than 50 international conferences/symposiums, e.g. IJCAI, AAAI, ICFEM, SETTA, ICTAC, TASE, UTP, FM, LCTES, ICECCS, ABZ.
  • Steering Committee Membership

  • ICFEM:International Conference on Formal Engineering Methods
  • TASE: IEEE International Symposium on Theoretical Aspects of Software Engineering
  • UTP: International Symposium on Unifying Theories of Programming
  • Other Conference Organisation Activities

  • FM'2014, May, 2014, Singapore. (Workshop Chair)
  • APLAS'04, November, 2004, Taipei. (Publicity Chair)
  • ICFEM'03, November, 2003, Singapore. (Publicity Co-Chair)


  • Some Links

  • The Formal Methods Wiki
  • Resources for Programming Language Research
  • Forthcoming Conferences in Formal Methods and Soft. Technology
  • So long, and thanks for the Ph.D.!

  • Thank you for your visit. My email: S.Qin[at]tees.ac.uk