Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol. - Weiqiang Kong; Kazuhiro Ogata 001; Jianwen Xiang; Kokichi Futatsugi (CIT, 2004)

A Lightweight Integration of Theorem Proving and Model Checking for System Verification. - Weiqiang Kong; Takahiro Seino; Kokichi Futatsugi; Kazuhiro Ogata 001 (APSEC, 2005)

Formal Analysis of Workflow Systems with Security Considerations. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (SEKE, 2005)

Induction-Guided Falsification. - Kazuhiro Ogata 001; Masahiro Nakano; Weiqiang Kong; Kokichi Futatsugi (ICFEM, 2006)

Falsification of OTSs by Searches of Bounded Reachable State Spaces. - Kazuhiro Ogata 001; Weiqiang Kong; Kokichi Futatsugi (SEKE, 2006)

Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. - Jianwen Xiang; Weiqiang Kong; Kokichi Futatsugi; Kazuhiro Ogata 001 (WEBIST (2), 2006)

Formal support for e-government system design with transparency consideration. - Xiaoyi Chen; Weiqiang Kong; Kokichi Futatsugi (ICEGOV, 2007)

Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IFM, 2007)

Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (Int. J. Softw. Eng. Knowl. Eng., 2007)

From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ. - Jianwen Xiang; Kazuhiro Ogata 001; Weiqiang Kong; Kokichi Futatsugi (Inf. Media Technol., 2007)

Trace anonymity in the OTS/CafeOBJ method. - Weiqiang Kong; Kazuhiro Ogata 001; Jian Cheng; Kokichi Futatsugi (CIT, 2008)

A Specification Translation from Behavioral Specifications to Rewrite Specifications. - Masaki Nakamura 001; Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2008)

An SMT Approach to Bounded Model Checking of Design in State Transition Matrix. - Weiqiang Kong; Tomohiro Shiraishi; Yuki Mizushima; Noriyuki Katahira; Akira Fukuda; Masahiko Watanabe (ICCSA Workshops, 2010)

Model Checking of Software Design in State Transition Matrix. - Tomohiro Shiraishi; Weiqiang Kong; Yuki Mizushima; Noriyuki Katahira; Michihiro Matsumoto; Masahiko Watanabe; Tetsuro Katayama; Akira Fukuda (Software Engineering Research and Practice, 2010)

Towards Reliable E-Government Systems with the OTS/CafeOBJ Method. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2010)

Formal Verification of Software Designs in Hierarchical State Transition Matrix with SMT-based Bounded Model Checking. - Weiqiang Kong; Noriyuki Katahira; Masahiko Watanabe; Tetsuro Katayama; Kenji Hisazumi; Akira Fukuda (APSEC, 2011)

An SMT-Based Approach to Bounded Model Checking of Designs in Communicating State Transition Matrix. - Weiqiang Kong; Noriyuki Katahira; Wanpeng Qian; Masahiko Watanabe; Tetsuro Katayama; Akira Fukuda (ICCSA Workshops, 2011)

An SMT-Based Approach to Bounded Model Checking of Designs in State Transition Matrix. - Weiqiang Kong; Tomohiro Shiraishi; Noriyuki Katahira; Masahiko Watanabe; Tetsuro Katayama; Akira Fukuda (IEICE Trans. Inf. Syst., 2011)

Formal Verification of Communicating HSTM Designs. - Leyuan Liu 002; Weiqiang Kong; Shijie Zhou 002; Zhiguang Qin; Akira Fukuda (CIT, 2012)

On Accelerating SMT-based Bounded Model Checking of HSTM Designs. - Weiqiang Kong; Leyuan Liu 002; Yoriyuki Yamagata; Kenji Taguchi 001; Hitoshi Ohsaki; Akira Fukuda (APSEC, 2012)

A dynamic channel assignment method based on location information of mobile terminals in indoor WLAN positioning systems. - Ming Li; Long Han; Weiqiang Kong; Shigeaki Tagashira; Yutaka Arakawa; Akira Fukuda (IPIN, 2012)

Formal semantics of extended hierarchical state transition matrix by CSP. - Yoriyuki Yamagata; Weiqiang Kong; Akira Fukuda; Nguyen Van Tang; Hitoshi Ohsaki; Kenji Taguchi 001 (ACM SIGSOFT Softw. Eng. Notes, 2012)

Harnessing SMT-Based Bounded Model Checking through Stateless Explicit-State Exploration. - Weiqiang Kong; Leyuan Liu 002; Takahiro Ando; Hirokazu Yatsu; Kenji Hisazumi; Akira Fukuda (APSEC (1), 2013)

Formalization and Model Checking of SysML State Machine Diagrams by CSP#. - Takahiro Ando; Hirokazu Yatsu; Weiqiang Kong; Kenji Hisazumi; Akira Fukuda (ICCSA (3), 2013)

Towards Formal Description of Standards for Automotive Operating Systems. - Hirokazu Yatsu; Takahiro Ando; Weiqiang Kong; Kenji Hisazumi; Akira Fukuda; Toshiaki Aoki; Kokichi Futatsugi (ICST Workshops, 2013)

A formal semantics of extended hierarchical state transition matrices using CSP#. - Yoriyuki Yamagata; Weiqiang Kong; Akira Fukuda; Nguyen Van Tang; Hitoshi Ohsaki; Kenji Taguchi 001 (Formal Aspects Comput., 2014)

Translation rules of SysML state machine diagrams into CSP# toward formal model checking. - Takahiro Ando; Hirokazu Yatsu; Weiqiang Kong; Kenji Hisazumi; Akira Fukuda (Int. J. Web Inf. Syst., 2014)

Software for Wearable Devices: Challenges and Opportunities. - He Jiang 001; Xin Chen 032; Shuwei Zhang; Xin Zhang 093; Weiqiang Kong; Tao Zhang 001 (COMPSAC Workshops, 2015)

Facilitating Multicore Bounded Model Checking with Stateless Explicit-State Exploration. - Weiqiang Kong; Leyuan Liu 002; Takahiro Ando; Hirokazu Yatsu; Kenji Hisazumi; Akira Fukuda (Comput. J., 2015)

ZipPath: A Simple-But-Useful Path Finder for HSTM Designs in ZIPC. - Weiqiang Kong; Gang Hou; Xiangpei Hu; Yasuhito Arimoto; Masahiko Watanabe; Takahiro Ando; Kenji Hisazumi; Akira Fukuda (ICA, 2016)

Towards Sustainable Information Infrastructure Platform for Smart Mobility - Project Overview. - Akira Fukuda; Kenji Hisazumi; Shigemi Ishida; Tsunenori Mine; Tsuneo Nakanishi; Hiroki Furusho; Shigeaki Tagashira; Yutaka Arakawa; Kunihiko Kaneko; Weiqiang Kong (IIAI-AAI, 2016)

Garakabu2: an SMT-based bounded model checker for HSTM designs in ZIPC. - Weiqiang Kong; Gang Hou; Xiangpei Hu; Takahiro Ando; Kenji Hisazumi; Akira Fukuda (J. Inf. Secur. Appl., 2016)

Performance Evaluation for Interrupt-Driven Embedded Software Based on EDSPN. - Gang Hou; Kuanjiu Zhou; Tie Qiu 001; Weiqiang Kong; Mingchu Li (IEEE Access, 2017)

A Branch History Directed Heuristic Search for Effective Binary Level Dynamic Symbolic Execution. - Yan Hu; Weiqiang Kong; Yizhi Ren; Kim-Kwang Raymond Choo (IEEE Access, 2017)

Verification Model Translation Method toward Behavior Model for CAST. - Takahiro Ando; Bo Wang; Kenji Hisazumi; Weiqiang Kong; Akira Fukuda; Yasutaka Michiura; Keita Sakemi; Michihiro Matsumoto (DSA, 2018)

Method-Level Permission Analysis Based on Static Call Graph of Android Apps. - Yan Hu; Weiqiang Kong; Deng Ding; Jun Yan 009 (DSA, 2018)

Toward Sustainable Smart Mobility Information Infrastructure Platform - Current Status -. - Akira Fukuda; Tsuneo Nakanishi; Kenji Hisazumi; Kunihiko Kaneko; Shigeaki Tagashira; Tsunenori Mine; Yutaka Arakawa; Shigemi Ishida; Takahiro Ando; Shuichi Ashihara; Masakatsu Ura; Yoshimichi Nakamura; et al. (IIAI-AAI, 2018)

Analysis of Interrupt Behavior Based on Probabilistic Model Checking. - Gang Hou; Weiqiang Kong; Kuanjiu Zhou; Jie Wang 004; Xun Cao; Akira Fukuda (IIAI-AAI, 2018)

A Survey of Formal Techniques for Hardware/Software Co-verification. - Kun Liu; Weiqiang Kong; Gang Hou; Akira Fukuda (IIAI-AAI, 2018)

Multilevel Permission Extraction in Android Applications for Malware Detection. - Zhen Wang; Kai Li; Yan Hu; Akira Fukuda; Weiqiang Kong (CITS, 2019)

Interpolation-Based Multi-core Bounded Model Checking of HSTM Designs. - Kun Liu; Xiaozhen Zhang; Weiqiang Kong; Gang Hou; Masahiko Watanabe; Akira Fukuda (DSA, 2019)

From Local to Global Semantic Clone Detection. - Yuan Yuan 020; Weiqiang Kong; Gang Hou; Yan Hu; Masahiko Watanabe; Akira Fukuda (DSA, 2019)

Non-Deterministic Behavior Analysis for Embedded Software Based on Probabilistic Model Checking. - Gang Hou; Weiqiang Kong; Kuanjiu Zhou; Jie Wang 004; Chi Lin 001 (ICPADS, 2019)

Steering Interpolants Generation with Efficient Interpolation Abstraction Exploration. - Xiaozhen Zhang; Weiqiang Kong; Jianguo Jiang; Gang Hou; Akira Fukuda (TASE, 2019)

ROSF: Leveraging Information Retrieval and Supervised Learning for Recommending Code Snippets. - He Jiang 001; Liming Nie; Zeyi Sun 003; Zhilei Ren; Weiqiang Kong; Tao Zhang 001; Xiapu Luo (IEEE Trans. Serv. Comput., 2019)

A Multi-Strategy Combination Framework for Android Malware Detection Based on Various Features. - Zhen Wang; Xiaoning Han; Weiqiang Kong; Yong Piao; Gang Hou; Masahiko Watanabe; Akira Fukuda (TASE, 2020)

Compiler testing: a systematic literature analysis. - Yixuan Tang; Zhilei Ren; Weiqiang Kong; He Jiang 001 (Frontiers Comput. Sci., 2020)

SDLV: Verification of Steering Angle Safety for Self-Driving Cars. - Huihui Wu; Deyun Lv; Tengxiang Cui; Gang Hou; Masahiko Watanabe; Weiqiang Kong (Formal Aspects Comput., 2021)

An Empirical Comparison Between Tutorials and Crowd Documentation of Application Programming Interface. - Yixuan Tang; Zhilei Ren; He Jiang 001; Xiao-Chen Li; Weiqiang Kong (J. Comput. Sci. Technol., 2021)

Bounded Model Checking of Synchronous Reactive Models in Ptolemy II. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (APSEC, 2022)

Formal Verification of Hierarchical Ptolemy II Synchronous-Reactive Models with Bounded Model Checking. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (QRS, 2022)

Detecting Compiler Bugs Via a Deep Learning-Based Framework. - Yixuan Tang; Zhilei Ren; He Jiang 001; Lei Qiao 002; Dong Liu 025; Zhide Zhou; Weiqiang Kong (Int. J. Softw. Eng. Knowl. Eng., 2022)

Detecting Compiler Warning Defects Via Diversity-Guided Program Mutation. - Yixuan Tang; He Jiang 001; Zhide Zhou; Xiaochen Li; Zhilei Ren; Weiqiang Kong (IEEE Trans. Software Eng., 2022)

A Single-sample Pruning and Clustering Method for Neural Network Verification. - Huanzhang Xiong; Gang Hou; Long Zhu; Jie Wang 004; Weiqiang Kong (APSEC, 2023)

Verification of Safety for Synchronous-Reactive System Using Bounded Model Checking. - Xiaozhen Zhang; Zhaoming Yang; Hui Kong 004; Weiqiang Kong (Int. J. Softw. Eng. Knowl. Eng., 2023)

A Dual Relaxation Method for Neural Network Verification. - Huanzhang Xiong; Gang Hou; Yueyuan Qin; Jie Wang 004; Weiqiang Kong (Int. J. Softw. Eng. Knowl. Eng., 2024)

A transformer-based framework for software vulnerability detection using attention-driven convolutional neural networks. - Abdelkarim Smaili; Yanan Zhang; Mekkaoui Djamel Eddine; Mohamed Amine Midoun; Mohamed Zakariya Talhaoui; Hamidaoui Meryem; Weiqiang Kong (Eng. Appl. Artif. Intell., 2025)

Ethical Principles of Integrating ChatGPT Into IoT-Based Software Wearables: A Fuzzy-TOPSIS Ranking and Analysis Approach. - Maseeh Ullah Khan; Muhammad Farhat Ullah; Sabeeh Ullah Khan; Weiqiang Kong (Int. J. Intell. Syst., 2025)

Space-Constrained Random Sparse Adversarial Attack. - Yueyuan Qin; Gang Hou; Tingting Yu; Bing Gao; Weiqiang Kong; Xiaoshan Liu (Neurocomputing, 2025)

Bounded Verification of Atomicity Violations for Interrupt-Driven Programs via Lazy Sequentialization. - Yuan Zhang; Lei Qu; Yifei Wu; Leihuan Wu; Tingting Yu; Rui Chen; Weiqiang Kong (ACM Trans. Softw. Eng. Methodol., 2025)