Research Areas

• Formal Methods, Formal Verification, (Symbolic) Model Checking

• Software Engineering

• Programming Languages

• Web Service Composition/Verification

• Automated Planning

Publications

• RISOPA: Rapid Imperceptible Strong One-Pixel Attacks in Deep Neural Networks.

Mathematics, Vol.12: 1083, Apr 2024.

• AESOP: Adjustable Exhaustive Search for One-Pixel Attacks in Deep Neural Networks.

Applied Sciences, Vol.13: 5092, Apr 2023.

• Formal Verification of Blockchain Smart Contracts via ATL Model Checking.
  IEEE Access 10: 8151-8162, 2022.

• Automatic Incremental Recomposition Algorithm for QoS-aware Internet-of-Things Service Composition.
  International Journal of Web and Grid Services, Vol.17, No.2, pp.118-137, 2021.

• Winning Strategy Tree Construction for BDD-Based ATL Model Checkers.
  International Journal of Software Engineering and Knowledge Engineering. Vol. 30, No. 4, pp. 555-573, 2020.

• Reliable Approximated Number System with Exact Bounds and Three-valued Logic.
  International Journal of Computer Systems Science and Engineering. Vol.33(6):447-455, 2018.

• MemPatrol: Reliable Sideline Integrity Monitoring for High-Performance Systems.
  14th International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA 2017), 48-69, 2017.

• Optimal Algorithm for Internet-of-Things Service Composition Based on Response Time.
  International Journal of Web and Grid Services. Vol.12(4), 388-406.

• Transaction History-based Web Service Composition for Uncertain QoS.
  International Journal of Web and Grid Services. Vol.12(1), 42-62.

• Formal Verification of Gravity-induced Loss of Consciousness Monitoring System for Aircraft.
  Computing in Science and Engineering, Vol. 16(5):96-103, Oct, 2014.

• On-the-fly Learning-based Search for QoS-aware Web Service Composition.
  Applied Mathematics and Information Sciences, Vol. 8(1L):141-147, 2014.

• Semantic Web Service Composition via Model Checking Techniques.
  International Journal of Web and Grid Services. Vol. 9(4):339-350, 2013.

• Efficient Anytime Algorithm for Large Scale QoS-aware Web Service Composition.
  International Journal of Web and Grid Services. Vol. 9(1):82-106, 2013.

• Behavioral Description Based Web Service Composition Using Abstraction and Refinement.
  International Journal of Web and Grid Services. Vol. 9(1):54-81, 2013.

• Reliable Integration of Exact and Approximated Arithmetic with Three-Valued Logic in Python.
  The 1st International Conference on Software Technology, pages 104-109, May 29-31, 2012.

• Efficient Type-aware Web Service Composition Using Formal Verification Techniques.
  The 2012 International Conference on Information Science and Technology, pages 333-336, April 28-30, 2012.

• On the Computational Complexity of Behavioral Description-Based Web Service Composition.
  Theoretical Computer Science, Vol.412(48):6736-6749. Nov 11, 2011.

• Anytime Algorithm for QoS Web Service Composition.
  The 20th International World Wide Web Conference (WWW'11 poster), pages 71-72, March 28-April 1, 2011.

• Modeling Cyber-Physical Systems Using Hybrid System Framework: A Case Study.
  The 2nd International Conference on Research Challenges in Computer Science (ICRCCS 2010), pages 343-346, Dec 18-19, 2010.

• Modeling Autonomous Military Robots Using Hybrid System Framework.
  International Conference on ICT Convergence (ICTC 2010), pages 429-430, Nov 17-19, 2010.

• Active Learning of Plans for Safety and Reachability Goals with Partial Observability.
  IEEE Transactions on Systems, Man, and Cybernetics-Part B: Cybernetics, Vol. 40(2):412-420, April 2010.

• Graph Theoretic Topological Analysis of Web Service Networks.
  World Wide Web Journal, Vol. 12(3):321-343, Sep. 2009.

• QoS-Driven Web Service Composition Using Learning-based Depth First Search.
  The 11th IEEE Conference on Commerce and Enterprise Computing (CEC'09), pages 507-510, Jul 20-23, 2009.

• Efficient Abstraction and Refinement for Behavioral Description Based Web Service Composition.
  The 21st International Joint Conference on Artificial Intelligence (IJCAI-09), pages 1740-1745, July 11-17, 2009.

• Automatic Web Service Composition with Abstraction and Refinement.
  The 18th International World Wide Web Conference (WWW'09 poster), pages 1121-1122, Apr 20-24, Dec 2-5, 2009.

• DL2Go: Editable Digital Libraries in the Pocket.
  The 11th International Conference on Asia-Pacific Digital Libraries (ICADL'08), 2008.

• Computational Complexity of Web Service Composition Based on Behavioral Descriptions.
  The 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'08), pages 359-363, November 3-5, 2008.

• Type-Aware Web Service Composition Using Boolean Satisfiability Solver.
  IEEE Joint Conference on E-Commerce Technology (CEC'08) and Enterprise Computing, E-Commerce and E-Services (EEE'08), page 331-334, Jul 21-24, 2008.

• Automatic Symbolic Compositional Verification by Learning Assumptions.
  Formal Methods in System Design, Vol. 32(3):207-234, June 2008.

• Learning-based Symbolic Assume-guarantee Reasoning with Automatic Decomposition.
  The 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), Beijing, China, Oct 23-26, 2006.

• Formal Verification of Industrial Benchmarks Using Flexible Engine Architecture.
  Cadence Technical Conference, May 8-10, 2006. The best paper award.

• Symbolic Compositional Verification by Learning Assumptions.
  The 17th International Conference on Computer Aided Verification (CAV'05), Edinburgh, Scotland, UK, July 6-10, 2005.

• Synthesis of Interface Specifications for Java Classes.
  The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), Long Beach, California, USA, pp.98-109, January 12-14, 2005.

• Symbolic Computational Techniques for Solving Games.
  International Journal on Software Tools for Technology Transfer (STTT), Vol.7(2), pp.118-128, 2005.

• Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) Infusion Pump Control System.
  International Journal in Software Tools for Technology Transfer (STTT), Vol.5(4), pp.308-319, 2004.

• Symbolic Computational Techniques for Solving Games (Preliminary version).
  The 1st International Workshop on Bounded Model Checking (BMC'03), Boulder, Colorado, USA, July 13, 2003.