Qinsi Wang
Computer Science Department
School of Computer Science
Carnegie Mellon University
Address: GHC 9129, 5000 Forbes Ave, Pittsburgh, PA 15213
Email: qinsiw [at] cs.cmu.edu
About
I am an independent postdoctoral researcher in the group of Prof. Jean Yang at Carnegie Mellon University. I received my PhD in Computer Science at CMU under the supervision of Prof. Edmund M. Clarke (Turing Award 2007) in Sep 2016. My research interest is to develop formal specification and verification techniques for real-world systems with the emphasis on statistical model checking for models of biological signaling networks, stochastic SMT-based methods for stochastic hybrid systems, and combining model checking techniques with machine learning methods for the study of biological systems and causal networks. Here is my CV.
Recent News
- Nov 2018: SMC4WM, a statistical model checker solving the probabilistic inference problems for multiple types of causal models, is released. Feel free to try!
- August 2017: Got a 4-year DARPA grant - World Modelers - as a coPI.
- July 2017: KaStat, a statistical analyzer for studying the finer-grained relationships between Kappa rules, is released. Feel free to try!
- June 2017: Paper accepted to the 15th conference on Computational Methods in Systems Biology.
- The 13th International Conference on Advanced Data Mining and Applications (ADMA17) - PC member
- The Eighth International Workshop on Static Analysis for Systems Biology (SASB2017) - PC member
- Workshop on Formal Methods for Biological and Biomedical Systems - FMBBS16 - PC co-chair
- Attending the 2016 Rising Stars Workshop in Pittsburgh, October 30th - Nov 1st.
- Attending HLDVT 2016 in Santa Cruz, October 7 – 8, 2016.
- Attending CMSB 2016 in Cambridge, UK from Sep. 21st to 23rd 2016.
- Papers accepted to the 18th IEEE International High-Level Design Validation and Test Workshop.
- Paper accepted to the 14th conference on Computational Methods in Systems Biology.
- Attending the 32nd Annual Mathematical Problems in Industry Workshop @ Duke University, June 13-17, 2016.
- The 12th International Conference on Advanced Data Mining and Applications (ADMA16) - PC member
- Richard King Mellon Foundation Presidential Fellowship in the Life Sciences, 2015-2016.
- Attending CMSB 2015 in Nantes from Sept. 16th to Sept. 18th 2015.
- Attending 3rd Heidelberg Laureate Forum as selected young researcher worldwide in math and cs.
- SReach introduced in our CMSB 2015 paper is released. Feel free to try!
Research
In Submission
- Qinsi Wang, Ziqiang Yuan. Probabilistic Counterexample Generation for Statistical Model Checking against Causal Networks. Ziqiang Yuan,
- Qinsi Wang. SMC4WM: Solving Probabilistic Temporal Inference Problems for Causal Networks using Statistical Model.
- Qinsi Wang, Jean Yang. KaStat: Studying the Fine-grained Inference in Kappa Rule-based Models using Statistical Methods.
Publications
- Kai-Wen Liang, Qinsi Wang, Cheryl A. Telmer, Divyaa Ravichandran, Peter Spirtes, Natasa Miskov-Zivanov. Methods to Expand Cell Signaling Models using Automated Reading and Model Checking. accepted to CMSB 2017.
- Qinsi Wang, Edmund M. Clarke. Formal Modeling of Biological Systems. invited paper to HLDVT2016: the 18th IEEE International High-Level Design Validation and Test Workshop, Santa Cruz, California, U.S.A., October 7 – 8, 2016.[PDF]
- Md. Ariful Islam, Qinsi Wang, Edmund Clarke, Scott Smolka, Ramin Hasani, Radu Grosu and Ondrej Balun. Probabilistic Reachability Analysis of the Tap Withdrawal Circuit in Caenorhabditis elegans. HLDVT2016: the 18th IEEE International High-Level Design Validation and Test Workshop, Santa Cruz, California, U.S.A., October 7 – 8, 2016. [PDF]
- Natasa Miskov-Zivanov, Paolo Zuliani, Qinsi Wang, Edmund Clarke, James Faeder. High-level modeling and verification of cellular signaling. HLDVT2016: the 18th IEEE International High-Level Design Validation and Test Workshop, Santa Cruz, California, U.S.A., October 7 – 8, 2016. [PDF]
- Qinsi Wang, Natasa Miskov-Zivanov, Bing Liu, James Faeder, Michael T. Lotze, Edmund M. Clarke. Formal Modeling and Analysis of Pancreatic Cancer Microenvironment. CMSB 2016: Computational Methods in Systems Biology, Cambridge, UK, Sep 21-23, 2016. [PDF/Slides]
- Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao and Edmund M. Clarke. SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems. CMSB 2015: Computational Methods in Systems Biology, Nantes, France, Sep 16-18, 2015. [PDF/Slides/Tool]
- Qinsi Wang, Natasa Miskov-Zivanov, Cheryl Telmer, Edmund M. Clarke. Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins. GLSVLSI 2015, Pittsburgh, Pennsylvania, USA, May 20-22, 2015. [PDF/Slides]
- Edmund M. Clarke, Qinsi Wang. 2^5 Years of Model Checking. Ershov Memorial Conference 2014: 26-40. [PDF]
- Ronald Watro, Kerry Moffitt, Talib Hussain, Daniel Wyschogrod, John Ostwald, Derrick Kong, Clint Bowers, Eric Church, Joshua Guttman, Qinsi Wang. Ghost Map: Proving Software Correctness using Games. SECURWARE 2014: The Eighth International Conference on Emerging Security Information, Systems and Technologies, Lisbon, Portugal, November 16-20, 2014. [PDF/Tool]
- Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Qinsi Wang (alphabetical order). Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. CAV 2013: 25th International Conference on Computer Aided Verification, Saint Petersburg, Russia, July 13–19, 2013. [PDF/Tool]
- Haijun Gong, Qinsi Wang, Paolo Zuliani, James R. Faeder, Michael Lotze. Symbolic Model Checking of Signaling Pathways in Pancreatic Cancer. BICoB 2011: 3rd International Conference on Bioinformatics and Computational Biology, New Orleans, Louisiana USA, March 23-25, 2011. [PDF]
- Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke. Formal Analysis for Logical Models of Pancreatic Cancer. CDC-ECE 2011, Orlando, FL, USA: 4855-4860. [PDF]
- Qinsi Wang. Constructing Transition-based Generalized Timed Buchi Automata for Metric Interval Temporal Logic. Journal of Computer Engineering and Design, 2011.
Theses
- Qinsi Wang. Model Checking for Biological Systems: Languages, Algorithms, and Applications. Thesis for the Doctoral Degree (Sep 2016).[PDF ]
- Qinsi Wang. Model Checking for Biological Systems: Languages, Algorithms, and Applications. Thesis Proposal for the Doctoral Degree (March 2016).[PDF ]
- Qinsi Wang. Constructing Transition-based Generalized Timed Buchi Automata for Metric Interval Temporal Logic. Master’s Thesis (2010).
- Qinsi Wang. Analysis of Association Rules at Various Granularity Levels. Bachelor's Thesis (2006).
Software
SMC4WM: a statistical model checker solving the probabilistic inference problems for multiple types of causal models, such as (multidimensional) Dynamic Bayesian Networks, Bayesian Networks, and Probabilistic Boolean Networks. It has also implemented several model search methods to generate probabilistic counterexamples for statistical model checking against these causal models.
KaStat: a statistical analyzer for Kappa models. Currently, it carries out the types of analyses: estimating the probability of a certain type of influence between two given Kappa rules, and outputting the causal core that contributes most to the existence of the influence between the given Kappa rules.
SReach: a bounded model checker for hybrid systems with parametric uncertainty, and probabilistic hybrid automata with additional randomness.
GhostMap: a crowd-sourced, online game for formal analysis of the correctness of C programs.
BioCheck+: a biological modeling and analyzing tool that illustrates signaling pathways and checks cellular properties.
MITLCon: a convertor from Real-Time Temporal Logic to Timed Automata.
CATV/LTL: a Linear Temporal Logic (LTL) model checker for Timed Automata.
ARDM_VG: an analyzer of association rules at various granularity levels.
Grant Support
- World Modelers, funded by Defense Advanced Research Projects Agency (DARPA), awarded $973,945, 2018-2021.
Conference Talks and Posters
- SMC4WM: Solving Probabilistic Temporal Inference Problems for Causal Networks using Statistical Model Checking. DARPA World Modelers PI Meeting, Jul 30 - Aug 1, 2018.
- Formal Analysis for Hybrid Causal Models. DARPA World Modelers Kick Off Meeting, Jan 28 - Jan 31, 2018.
- CyberCardia Project: Modeling, Verification andValidation of Implantable Cardiac Devices. FMBBS 2016 (IEEE BIBM 2016), Shenzhen, China, Dec 18, 2016. [Slides]
- Formal Modeling and Analysis of Pancreatic Cancer Microenvironment. CMSB 2016, Cambridge, UK, Sep 21-23, 2016. [Slides]
- SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems. CMSB 2015, Nantes, France, Sep 16-18, 2015. [Slides]
- Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins. GLSVLSI 2015, Pittsburgh, Pennsylvania, USA, May 20-22, 2015. [Slides]
- SReach: Combining SMT-based Model Checking and Statistical Tests. Clarke Symposium, September 2014, Pittsburgh, US. [Slides]
- Poster: GhostMap - Proving Software Correctness using Games. The 3rd Crowd Sourced Formal Verification (CSFV), Automated Program Analysis for Cybersecurity (APAC), and High-Assurance Cyber Military Systems (HACMS) Joint PI Meeting, Stevenson, WA, July 22-26, 2013.
- Poster: Extending the Semantics of the Rule-based Modeling Language for Multi-level Biological Models. CRA-W Graduate Cohort Workshop, Bellevue, Washington, April 13-14, 2012.
- Poster: Construction and Analysis of A Multicellular Model of the Pancreatic Cancer Micro-environment. CMACS Mid-Term Site Visit Review, Carnegie Mellon University, November 3-4, 2011. [Poster]
- A Multicellular Model of the Pancreatic Cancer Microenvironment. Computational Modeling and Analysis for Complex Systems (CMACS) PI Review Meeting, University of Maryland, April 28-29, 2011. [Slides]
Professional Services
PC Co-Chair or Member of Conferences:
The 13th International Conference on Advanced Data Mining and Applications (ADMA17) - PC member
The 8th International Workshop on Static Analysis for Systems Biology (SASB17) - PC member
The 12th International Conference on Advanced Data Mining and Applications (ADMA16) - PC member
Workshop on Formal Methods for Biological and Biomedical Systems - FMBBS16 - PC co-chair
Reviewer of Journals/Conference Proceedings:
IEEE/ACM Transactions on Computational Biology and Bioinformatics, 2018
Theoretical Computer Science Journal, Elsevier, 2018
The 13th International Conference on Advanced Data Mining and Applications, 2017
The 8th International Workshop on Static Analysis for Systems Biology, 2017
Theoretical Computer Science Journal, Elsevier, 2017
Information Sciences Journal, Elsevier, 2017
The 12th International Conference on Advanced Data Mining and Applications, 2016
4th International Workshop on Hybrid Systems Biology (HSB 2015)
Computational Studies of Immune System Function, Computational Biology, 2014
11th International Conference on Quantitative Evaluation of Systems (QEST 2014)
International Conference on Computer Aided Verification (CAV 2013)
Mathematical Tools of Soft Computing, Mathematical Problems in Engineering, 2013
50th IEEE Conference on Decision and Control & 11th European Control Conference (CDC-ECC 2011)
Conference Volunteers:
15th Asia-Pacific Software Engineering Conference (APSEC 2008), Beijing, China, December 3-5, 2008
1st International Conference on Advanced Data Mining and Applications (ADMA 2005), Wuhan, China, July 22-24, 2005.
Education
- 2010.9 - 2016.9, Ph.D. Computer Science Department, Carnegie Mellon University, USA
- 2007.9 - 2010.7, M.S. Computer Science Institute of Software, Chinese Academy of Sciences, China
- 2002.9 - 2006.7, A.B. Computer Science International Institute of Software, Wuhan University, China
Coursework at CMU
- Spring 2015, 46945 Stochastic Calculus II
- Spring 2015, 70462 Stochastic Modeling and Simulations
- Spring 2015, 46944 Stochastic Calculus for Finance I
- Spring 2013, 15750 Graduate Algorithms
- Spring 2013, 15817 Introduction to Model Checking
- Spring 2012, 15745 Compilers for Modern Architecture
- Spring 2012, 15812 Semantics of Programming Language
- Spring 2012, 10708 Probabilistic Graphical Models
- Spring 2012, 15817 Automated Theorem Proving
- Spring 2011, 02730 Cell Systems Modeling
- Spring 2011, 15817 Model Checking and Abstract Interpretation
- Fall 2010, 15781 Machine Learning
- Fall 2010, 15744 Computer Networks
Teaching and Working Experience
- 2017.12 - present, Independent Postdoc Researcher in Computer Science Department, Carnegie Mellon University, USA
- 2016.10 - 2017.11, Postdoc Researcher in Computer Science Department, Carnegie Mellon University, USA
- Spring 2014, Teaching Assistant, CMU 15–414/614 Bug Catching: Automated Program Verification
- Fall 2012, Teaching Assistant, CMU 15–414/614 Automated Program Verification
- Fall 2011, Research Intern, Microsoft Research, Cambridge (with Dr. Jasmin Fisher)
- Fall 2004, Teaching Assistant, WHU course: Software Engineering
Scholarships, Awards, and Honors
- Richard King Mellon Foundation Presidential Fellowship in the Life Sciences, 2015-2016.
- Excellent Student Award (top 5%), Chinese Academy of Sciences, 2007–2008.
- Best Bachelor Thesis Award, Hubei Province, 2006.
- The 1st Creative Software Design Contest-2nd Place, Wuhan University, 2006.
- Excellent Student Award (top 5%), Wuhan University, 2002–2005.