Automatic Verification of Annotated Code. - Doron A. Peled; Hongyang Qu 001 (FORTE, 2003)

Automatic Generation of Path Conditions for Timed Systems. - Saddek Bensalem; Doron A. Peled; Hongyang Qu 001; Stavros Tripakis (ISoLA (Preliminary proceedings), 2004)

Calculating Probabilities of Real-Time Test Cases. - Marcin Jurdzinski; Doron A. Peled; Hongyang Qu 001 (FATES, 2005)

Time Unbalanced Partial Order. - Doron A. Peled; Hongyang Qu 001 (FATES, 2005)

Generating Path Conditions for Timed Systems. - Saddek Bensalem; Doron A. Peled; Hongyang Qu 001; Stavros Tripakis (IFM, 2005)

Theoretical and practical tools for validating discrete and real-time systems. - Hongyang Qu 001 (2005)

The Implementation of Mazurkiewicz Traces in POEM. - Peter Niebert; Hongyang Qu 001 (ATVA, 2006)

Adding Invariants to Event Zone Automata. - Peter Niebert; Hongyang Qu 001 (FORMATS, 2006)

Grey-Box Checking. - Edith Elkind; Blaise Genest; Doron A. Peled; Hongyang Qu 001 (FORTE, 2006)

Stronger Reduction Criteria for Local First Search. - Marcos E. Kurbán; Peter Niebert; Hongyang Qu 001; Walter Vogler (ICTAC, 2006)

Enforcing Concurrent Temporal Behaviors. - Doron A. Peled; Hongyang Qu 001 (Int. J. Found. Comput. Sci., 2006)

Test Case Generation for Ultimately Periodic Paths. - Saddek Bensalem; Doron A. Peled; Hongyang Qu 001; Stavros Tripakis; Lenore D. Zuck (Haifa Verification Conference, 2007)

Verifying Temporal and Epistemic Properties of Web Service Compositions. - Alessio Lomuscio; Hongyang Qu 001; Marek J. Sergot; Monika Solanki (ICSOC, 2007)

Towards verifying compliance in agent-based web service compositions. - Alessio Lomuscio; Hongyang Qu 001; Monika Solanki (AAMAS (1), 2008)

Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic. - Alessio Lomuscio; Wojciech Penczek; Hongyang Qu 001 (MoChArt, 2008)

Automatic generation of path conditions for concurrent timed systems. - Saddek Bensalem; Doron A. Peled; Hongyang Qu 001; Stavros Tripakis (Theor. Comput. Sci., 2008)

A Data Symmetry Reduction Technique for Temporal-epistemic Logic. - Mika Cohen; Mads Dam; Alessio Lomuscio; Hongyang Qu 001 (ATVA, 2009)

MCMAS: A Model Checker for the Verification of Multi-Agent Systems. - Alessio Lomuscio; Hongyang Qu 001; Franco Raimondi (CAV, 2009)

Optimizing Probabilities of Real-Time Test Case Execution. - Nicolás Wolovick; Pedro R. D'Argenio; Hongyang Qu 001 (ICST, 2009)

A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic. - Mika Cohen; Mads Dam; Alessio Lomuscio; Hongyang Qu 001 (IJCAI, 2009)

Reo2MC: a tool chain for performance analysis of coordination models. - Farhad Arbab; Sun Meng; Young-Joo Moon 001; Marta Z. Kwiatkowska; Hongyang Qu 001 (ESEC/SIGSOFT FSE, 2009)

Parallel Model Checking for Temporal Epistemic Logic. - Marta Z. Kwiatkowska; Alessio Lomuscio; Hongyang Qu 001 (ECAI, 2010)

Dependability Analysis and Verification for Connected Systems. - Felicita Di Giandomenico; Marta Z. Kwiatkowska; Marco Martinucci; Paolo Masci 001; Hongyang Qu 001 (ISoLA (2), 2010)

Automatic Data-Abstraction in Model Checking Multi-Agent Systems. - Alessio Lomuscio; Hongyang Qu 001; Francesco Russo 003 (MoChArt, 2010)

Assume-Guarantee Verification for Probabilistic Systems. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (TACAS, 2010)

Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. - Alessio Lomuscio; Wojciech Penczek; Hongyang Qu 001 (Fundam. Informaticae, 2010)

On the verification of social commitments and time. - Mohamed El-Menshawy; Jamal Bentahar; Hongyang Qu 001; Rachida Dssouli (AAMAS, 2011)

Incremental quantitative verification for Markov decision processes. - Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001 (DSN, 2011)

Partial Order Reduction for Model Checking Markov Decision Processes under Unconditional Fairness. - Henri Hansen; Marta Z. Kwiatkowska; Hongyang Qu 001 (QEST, 2011)

Quantitative Multi-objective Verification for Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (TACAS, 2011)

Incremental Runtime Verification of Probabilistic Systems. - Vojtech Forejt; Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001; Mateusz Ujma (RV, 2012)

Towards verifying contract regulated service composition. - Alessio Lomuscio; Hongyang Qu 001; Monika Solanki (Auton. Agents Multi Agent Syst., 2012)

Communicative commitments: Model checking and complexity analysis. - Jamal Bentahar; Mohamed El-Menshawy; Hongyang Qu 001; Rachida Dssouli (Knowl. Based Syst., 2012)

Representing and reasoning about communicative conditional commitments. - Warda El Kholy; Mohamed El-Menshawy; Jamal Bentahar; Hongyang Qu 001; Rachida Dssouli (AAMAS, 2013)

Model Repair for Markov Decision Processes. - Taolue Chen 001; Ernst Moritz Hahn; Tingting Han 001; Marta Z. Kwiatkowska; Hongyang Qu 001; Lijun Zhang 001 (TASE, 2013)

Reasoning about Strategies under Partial Observability and Fairness Constraints - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (SR, 2013)

Compositional probabilistic verification through multi-objective model checking. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Hongyang Qu 001 (Inf. Comput., 2013)

On Incremental Quantitative Verification for Probabilistic Systems. - Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001; Mateusz Ujma (HOWARD-60, 2014)

On efficient consistency checks by robots. - Hongyang Qu 001; Sandor M. Veres (ECC, 2014)

Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (ICFEM, 2014)

Verifying Multiagent-Based Web Service Compositions Regulated by Commitment Protocols. - Warda El Kholy; Mohamed El-Menshawy; Jamal Bentahar; Hongyang Qu 001; Rachida Dssouli (ICWS, 2014)

Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols. - Warda El Kholy; Jamal Bentahar; Mohamed El-Menshawy; Hongyang Qu 001; Rachida Dssouli (Expert Syst. Appl., 2014)

Local abstraction refinement for probabilistic timed programs. - Klaus Dräger; Marta Z. Kwiatkowska; David Parker 001; Hongyang Qu 001 (Theor. Comput. Sci., 2014)

Conditional Commitments: Reasoning and Model Checking. - Warda El Kholy; Jamal Bentahar; Mohamed El-Menshawy; Hongyang Qu 001; Rachida Dssouli (ACM Trans. Softw. Eng. Methodol., 2014)

Behaviour Analysis of Mixed Game-Theoretic Learning Algorithms. - Michalis Smyrnakis; Hongyang Qu 001; Sandor M. Veres (AAMAS, 2015)

Computing Time-Optimal Clearing Strategies for Pursuit-Evasion Problems with Linear Programming. - Hongyang Qu 001; Andreas Kolling; Sandor M. Veres (TAROS, 2015)

Formal Specification and Automatic Verification of Conditional Commitments. - Warda El Kholy; Mohamed El-Menshawy; Jamal Bentahar; Hongyang Qu 001; Rachida Dssouli (IEEE Intell. Syst., 2015)

Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (Inf. Comput., 2015)

A stochastically verifiable autonomous control architecture with reasoning. - Paolo Izzo; Hongyang Qu 001; Sandor M. Veres (CDC, 2016)

Testing, Verification and Improvements of Timeliness in ROS Processes. - Mohammed Y. Hazim; Hongyang Qu 001; Sandor M. Veres (TAROS, 2016)

Improving BDD-based attractor detection for synchronous Boolean networks. - Qixia Yuan; Hongyang Qu 001; Jun Pang 001; Andrzej Mizera (Sci. China Inf. Sci., 2016)

Reducing complexity of autonomous control agents for verifiability. - Paolo Izzo; Hongyang Qu 001; Sandor M. Veres (CoRR, 2016)

SMCL - Stochastic Model Checker for Learning in Games. - Hongyang Qu 001; Michalis Smyrnakis; Sandor M. Veres (CoRR, 2016)

Verification of logical consistency in robotic reasoning. - Hongyang Qu 001; Sandor M. Veres (Robotics Auton. Syst., 2016)

A New Decomposition Method for Attractor Detection in Large Synchronous Boolean Networks. - Andrzej Mizera; Jun Pang 001; Hongyang Qu 001; Qixia Yuan (SETTA, 2017)

Taming Asynchrony for Attractor Detection in Large Boolean Networks (Technical Report). - Andrzej Mizera; Jun Pang 001; Hongyang Qu 001; Qixia Yuan (CoRR, 2017)

SMC4AC: A New Symbolic Model Checker for Intelligent Agent Communication. - Warda El Kholy; Jamal Bentahar; Mohamed El-Menshawy; Hongyang Qu 001; Rachida Dssouli (Fundam. Informaticae, 2017)

MCMAS: an open-source model checker for the verification of multi-agent systems. - Alessio Lomuscio; Hongyang Qu 001; Franco Raimondi (Int. J. Softw. Tools Technol. Transf., 2017)

Computational Framework for Verifiable Decisions of Self-Driving Vehicles. - Mohammed Al-Nuaimi; Hongyang Qu 001; Sandor M. Veres (CCTA, 2018)

ASSA-PBN 3.0: Analysing Context-Sensitive Probabilistic Boolean Networks. - Andrzej Mizera; Jun Pang 001; Hongyang Qu 001; Qixia Yuan (CMSB, 2018)

A stochastically verifiable decision making framework for autonomous ground vehicles. - Mohammed Al-Nuaimi; Hongyang Qu 001; Sandor M. Veres (ISR, 2018)

Improving Multi-Robot Coordination by Game-Theoretic Learning Algorithms. - Michalis Smyrnakis; Hongyang Qu 001; Sandor M. Veres (Int. J. Artif. Intell. Tools, 2018)

Online Observability of Boolean Control Networks. - Guisen Wu; Liyun Dai; Zhiming Liu 001; Taolue Chen 001; Jun Pang 001; Hongyang Qu 001 (CoRR, 2019)

A new decomposition-based method for detecting attractors in synchronous Boolean networks. - Qixia Yuan; Andrzej Mizera; Jun Pang 001; Hongyang Qu 001 (Sci. Comput. Program., 2019)

Comparing approaches for model-checking strategies under imperfect information and fairness constraints. - Simon Busard; Charles Pecheur; Hongyang Qu 001; Franco Raimondi (Int. J. Softw. Tools Technol. Transf., 2019)

Taming Asynchrony for Attractor Detection in Large Boolean Networks. - Andrzej Mizera; Jun Pang 001; Hongyang Qu 001; Qixia Yuan (IEEE ACM Trans. Comput. Biol. Bioinform., 2019)

Computationally Grounded Quantitative Trust with Time. - Nagat Drawel; Jamal Bentahar; Hongyang Qu 001 (AAMAS, 2020)

Multi-model Adaptive Learning for Robots Under Uncertainty. - Michalis Smyrnakis; Hongyang Qu 001; Dario Bauso; Sandor M. Veres (ICAART (1), 2020)

On the Combination of Game-Theoretic Learning and Multi Model Adaptive Filters. - Michalis Smyrnakis; Hongyang Qu 001; Dario Bauso; Sandor M. Veres (ICAART (Revised Selected Papers), 2020)

Specification and automatic verification of trust-based multi-agent systems. - Nagat Drawel; Hongyang Qu 001; Jamal Bentahar; Elhadi M. Shakshuki (Future Gener. Comput. Syst., 2020)

Hybrid Verification Technique for Decision-Making of Self-Driving Vehicles. - Mohammed Al-Nuaimi; Sapto Wibowo; Hongyang Qu 001; Jonathan M. Aitken; Sandor M. Veres (J. Sens. Actuator Networks, 2021)