# Zhenhua Duan

According to our database1, Zhenhua Duan authored at least 152 papers between 1994 and 2019.

Collaborative distances:

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2019
Model checking of pushdown systems for projection temporal logic.
Theor. Comput. Sci., 2019

Model checking open systems with alternating projection temporal logic.
Theor. Comput. Sci., 2019

A temporal logic programming approach to planning.
J. Comb. Optim., 2019

Verifying a scheduling protocol of safety-critical systems.
J. Comb. Optim., 2019

Verifying schedulability of tasks in ROS-based systems.
J. Comb. Optim., 2019

From Box Algebra to Interval Temporal Logic.
Fundam. Inform., 2019

FastDroid: efficient taint analysis for Android applications.
Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, 2019

2018
A Novel Approach to Modeling and Verifying Real-Time Systems for High Reliability.
IEEE Trans. Reliability, 2018

Planning with Spatio-Temporal Search Control Knowledge.
IEEE Trans. Knowl. Data Eng., 2018

A compiler for MSVL and its applications.
Theor. Comput. Sci., 2018

A Runtime Optimization Approach for FPGA Routing.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2018

Verifying temporal properties of programs: A parallel approach.
J. Parallel Distrib. Comput., 2018

On general threshold and general cascade models of social influence.
J. Comb. Optim., 2018

InterpChecker: Reducing State Space via Interpolations - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

A Blockchain Implementation of an Attendance Management System.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2018

Android inter-component communication analysis with intent revision.
Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

Accelerating counterexample detection in software model checking.
Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

RFC-directed differential testing of certificate validation in SSL/TLS implementations.
Proceedings of the 40th International Conference on Software Engineering, 2018

Reducing Extension Edges of Concurrent Programs for Reachability Analysis.
Proceedings of the Combinatorial Optimization and Applications, 2018

A Novel Approach to Verifying Context Free Properties of Programs.
Proceedings of the Algorithmic Aspects in Information and Management, 2018

2017
Two-layer hybrid peer-to-peer networks.
Peer-to-Peer Networking and Applications, 2017

MSVL: a typed language for temporal logic programming.
Frontiers Comput. Sci., 2017

Model Checking Multi-agent Systems with APTL.
Ad Hoc & Sensor Wireless Networks, 2017

Implementing MapReduce with MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2017

More effective interpolations in software model checking.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Temporalising Separation Logic for Planning with Search Control Knowledge.
Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, 2017

Full regular temporal property verification as dynamic program execution.
Proceedings of the 39th International Conference on Software Engineering, 2017

Verifying Temporal Properties of C Programs via Lazy Abstraction.
Proceedings of the Formal Methods and Software Engineering, 2017

Cloning Automata: Simulation and Analysis of Computer Bacteria.
Proceedings of the Combinatorial Optimization and Applications, 2017

Modeling and Verifying Multi-core Programs.
Proceedings of the Combinatorial Optimization and Applications, 2017

2016
A mechanism of function calls in MSVL.
Theor. Comput. Sci., 2016

A complete axiom system for propositional projection temporal logic with cylinder computation model.
Theor. Comput. Sci., 2016

A canonical form based decision procedure and model checking approach for propositional projection temporal logic.
Theor. Comput. Sci., 2016

Verifying safety critical task scheduling systems in PPTL axiom system.
J. Comb. Optim., 2016

Model checking Petri nets with MSVL.
Inf. Sci., 2016

Transformation from business process models to BPEL with overlapped patterns involved.
IJHPCN, 2016

Model checking concurrent systems with MSVL.
SCIENCE CHINA Information Sciences, 2016

Linear optimal estimation for discrete-time systems with measurement-delay and packet dropping.
Applied Mathematics and Computation, 2016

A Proof System for MSVL Programs in Coq.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2016

A Decision Procedure for a Fragment of Linear Time Mu-Calculus.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Extending MSVL with Semaphore.
Proceedings of the Computing and Combinatorics - 22nd International Conference, 2016

Satisfiability of Linear Time Mu-Calculus on Finite Traces.
Proceedings of the Computing and Combinatorics - 22nd International Conference, 2016

Using Unified Model Checking to Verify Heaps.
Proceedings of the Combinatorial Optimization and Applications, 2016

2015
Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts.
Theor. Comput. Sci., 2015

Transformation from PLTL to automata via NFGs.
J. Comb. Optim., 2015

A structural transformation from p-π to MSVL.
J. Comb. Optim., 2015

An extended strange planet protocol.
J. Comb. Optim., 2015

Verification of distributed systems with the axiomatic system of MSVL.
Formal Asp. Comput., 2015

PPTL_SPIN: A SPIN Based Model Checker for Propositional Projection Temporal Logic.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2015

LtlNfBa: Making LTL Translation More Practical.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2015

Model Checking Process Scheduling over Multi-core Computer System with MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2015

Modeling and Verification of an Interrupt System in \mu μ C/OS-III with TMSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2015

A Self-ORganizing Trust Model Based on HP2P.
Proceedings of the 11th International Conference on Mobile Ad-hoc and Sensor Networks, 2015

Model Checking \mu μ C/OS-III Multi-task System with TMSVL.
Proceedings of the Formal Methods and Software Engineering, 2015

Verification of a real time scheduling protocol of safety-critical systems.
Proceedings of the 19th IEEE International Conference on Computer Supported Cooperative Work in Design, 2015

Model Checking MSVL Programs Based on Dynamic Symbolic Execution.
Proceedings of the Computing and Combinatorics - 21st International Conference, 2015

Symbolic Model Checking for Alternating Projection Temporal Logic.
Proceedings of the Combinatorial Optimization and Applications, 2015

2014
Making CEGAR More Efficient in Software Model Checking.
IEEE Trans. Software Eng., 2014

A formal proof of the deadline driven scheduler in PPTL axiomatic system.
Theor. Comput. Sci., 2014

A practical decision procedure for Propositional Projection Temporal Logic with infinite models.
Theor. Comput. Sci., 2014

Secure communications with strange planet protocol.
Optimization Letters, 2014

Linear time-dependent constraints programming with MSVL.
J. Comb. Optim., 2014

Bounded Model Checking of Traffic Light Control System.
Electr. Notes Theor. Comput. Sci., 2014

Modeling and Verification of RBC Handover Protocol.
Electr. Notes Theor. Comput. Sci., 2014

An Improved Recursive Algorithm for Parity Games.
Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, 2014

Unified Bounded Model Checking for MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2014

A Memory Management Mechanism for MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2014

Clustering and Partition Based Divide and Conquer for SAT Solving.
Proceedings of the 10th International Conference on Mobile Ad-hoc and Sensor Networks, 2014

Interval Temporal Logic Semantics of Box Algebra.
Proceedings of the Language and Automata Theory and Applications, 2014

Extending MSVL with Function Calls.
Proceedings of the Formal Methods and Software Engineering, 2014

Model Checking Rate-Monotonic Scheduler with TMSVL.
Proceedings of the 2014 19th International Conference on Engineering of Complex Computer Systems, 2014

Simulation and verification of the virtual memory management system with MSVL.
Proceedings of the IEEE 18th International Conference on Computer Supported Cooperative Work in Design, 2014

An Axiomatization for Cylinder Computation Model.
Proceedings of the Computing and Combinatorics - 20th International Conference, 2014

Normal Form Expressions of Propositional Projection Temporal Logic.
Proceedings of the Computing and Combinatorics - 20th International Conference, 2014

Improved Even Order Magic Square Construction Algorithms and Their Applications.
Proceedings of the Combinatorial Optimization and Applications, 2014

2013
A cylinder computation model for many-core parallel computing.
Theor. Comput. Sci., 2013

A complete proof system for propositional projection temporal logic.
Theor. Comput. Sci., 2013

ITL semantics of composite Petri nets.
J. Log. Algebr. Program., 2013

Integration of Linear Constraints with a Temporal Logic Programming Language.
Proceedings of the Seventh International Symposium on Theoretical Aspects of Software Engineering, 2013

Formalizing and Implementing Types in MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2013

Improved Net Reductions for LTL $$\setminus$$ \ X Model Checking.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2013

Integrating Separation Logic with PPTL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2013

Present-Future Form of Linear Time $$\mu$$ -Calculus.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2013

A Transformation from p-π to MSVL.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

Detecting spurious counterexamples efficiently in abstract model checking.
Proceedings of the 35th International Conference on Software Engineering, 2013

Translation from Workflow Nets to MSVL.
Proceedings of the Formal Methods and Software Engineering, 2013

Simulation of CTCS-3 protocol with temporal logic programming.
Proceedings of the 2013 IEEE 17th International Conference on Computer Supported Cooperative Work in Design (CSCWD), 2013

Deternimization of Büchi Automata as Partitioned Automata.
Proceedings of the Computing and Combinatorics, 19th International Conference, 2013

Bounded Model Checking for Propositional Projection Temporal Logic.
Proceedings of the Computing and Combinatorics, 19th International Conference, 2013

An Extended Strange Planet Protocol.
Proceedings of the Combinatorial Optimization and Applications, 2013

Some Fixed-Point Issues in PPTL.
Proceedings of the Theories of Programming and Formal Methods, 2013

2012
Model Checking.
Proceedings of the Handbook of Finite State Based Models and Applications., 2012

An efficient approach for abstraction-refinement in model checking.
Theor. Comput. Sci., 2012

Efficient and scalable scheduling for performance heterogeneous multicore systems.
J. Parallel Distrib. Comput., 2012

Symbolic Model Checking for Propositional Projection Temporal Logic.
Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

Model Checking C Programs with MSVL.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2012

Abstract Model Checking with SOFL Hierarchy.
Proceedings of the Structured Object-Oriented Formal Language and Method, 2012

Time Constraints with Temporal Logic Programming.
Proceedings of the Formal Methods and Software Engineering, 2012

2011
Expressiveness of propositional projection temporal logic with star.
Theor. Comput. Sci., 2011

Focus Game for Projection Temporal Logic.
Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Specification and Verification of UML2.0 Sequence Diagrams Using Event Deterministic Finite Automata.
Proceedings of the Fifth International Conference on Secure Software Integration and Reliability Improvement, 2011

Asynchronous Communication in MSVL.
Proceedings of the Formal Methods and Software Engineering, 2011

ESHMP: A Stall-Time-Based Scheduling for Performance Heterogeneous Multicore Systems.
Proceedings of the 13th IEEE International Conference on High Performance Computing & Communication, 2011

Making Abstraction-Refinement Efficient in Model Checking.
Proceedings of the Computing and Combinatorics - 17th Annual International Conference, 2011

A Semantic Model for Many-Core Parallel Computing.
Proceedings of the Combinatorial Optimization and Applications, 2011

Public Communication Based on Russian Cards Protocol: A Case Study.
Proceedings of the Combinatorial Optimization and Applications, 2011

2010
Axiomatic semantics of projection temporal logic programs.
Mathematical Structures in Computer Science, 2010

Unconditional secure communication: a Russian Cards protocol.
J. Comb. Optim., 2010

Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic.
Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

Axiomatic Temporal Logic Programs Verification.
Proceedings of the 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2010

An Executable Concurrent Model for OWL-S Process Models.
Proceedings of the 10th International Conference on Quality Software, 2010

Non-Functional Requirements Elicitation and Incorporation into Class Diagrams.
Proceedings of the Intelligent Information Processing V, 2010

Alternating Interval Based Temporal Logics.
Proceedings of the Formal Methods and Software Engineering, 2010

An Improved Decision Procedure for Propositional Projection Temporal Logic.
Proceedings of the Formal Methods and Software Engineering, 2010

A Transformation from PPTL to S1S.
Proceedings of the Combinatorial Optimization and Applications, 2010

2009
A Proof System for Projection Temporal Logic.
Proceedings of the Computer and Information Science 2009 [outstanding papers from the 8th ACIS/IEEE International Conference on Computer and Information Science, 2009

Complexity of propositional projection temporal logic with star.
Mathematical Structures in Computer Science, 2009

A note on stutter-invariant PLTL.
Inf. Process. Lett., 2009

An Efficient Algorithm for Finding Empty Space for Reconfigurable Systems.
Proceedings of the TASE 2009, 2009

Verification of Use Case with Petri Nets in Requirement Analysis.
Proceedings of the Computational Science and Its Applications, 2009

Generalized Russian Cards Problem.
Proceedings of the Combinatorial Optimization and Applications, 2009

A Model-Driven Approach for Generating Business Processes and Process Interaction Semantics.
Proceedings of the 8th IEEE/ACIS International Conference on Computer and Information Science, 2009

2008
Framed temporal logic programming.
Sci. Comput. Program., 2008

Operational semantics of Framed Tempura.
J. Log. Algebr. Program., 2008

A decision procedure for propositional projection temporal logic with infinite models.
Acta Inf., 2008

A Complete Axiomatization of Propositional Projection Temporal Logic.
Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Symbolic Algorithm Analysis of Rectangular Hybrid Systems.
Proceedings of the Theory and Applications of Models of Computation, 2008

Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions.
Proceedings of the Theory and Applications of Models of Computation, 2008

From Business Process Models to Web Services Orchestration: The Case of UML 2.0 Activity Diagram to BPEL.
Proceedings of the Service-Oriented Computing, 2008

Kapa: A File Sharing System Based on HP2P.
Proceedings of the Third International Conference on Internet and Web Applications and Services, 2008

A Unified Model Checking Approach with Projection Temporal Logic.
Proceedings of the Formal Methods and Software Engineering, 2008

Semi-automatically annotating data semantics to web services using ontology mapping.
Proceedings of the 12th International Conference on CSCW in Design, 2008

Dynamic Critical-Path based on Fit Degree scheduling for reconfigurable multi-FPGAs.
Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD 2008), 2008

2007
Integrating AJAX and Web Services for Cooperative Image Editing.
IT Professional, 2007

An Interpreter for Framed Tempura and Its Application.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Decidability of Propositional Projection Temporal Logic with Infinite Models.
Proceedings of the Theory and Applications of Models of Computation, 2007

Operational Semantics of Framed Temporal Logic Programs.
Proceedings of the SOFSEM 2007: Theory and Practice of Computer Science, 2007

Model Checking Propositional Projection Temporal Logic Based on SPIN.
Proceedings of the Formal Methods and Software Engineering, 2007

HP2P: A Hybrid Hierarchical P2P Network.
Proceedings of the First International Conference on the Digital Society (ICDS 2007), 2007

Incorporating Clusters into Hybrid P2P Network.
Proceedings of the First International Conference on the Digital Society (ICDS 2007), 2007

Automating Web Service Composition for Collaborative Business Processes.
Proceedings of the 11th International Conference on Computer Supported Cooperative Work in Design, 2007

Utilizing Fuzzy Petri Net for Choreography Based Semantic Web Services Discovery.
Proceedings of the Petri Nets and Other Models of Concurrency, 2007

2006
Implementing Chord for HP2P Network.
Proceedings of the On the Move to Meaningful Internet Systems 2006: OTM 2006 Workshops, 2006

Transforming OWL-S Process Model into EDFA for Service Discovery.
Proceedings of the 2006 IEEE International Conference on Web Services (ICWS 2006), 2006

A Comprehensive Framework for Dynamic Web Services Integration.
Proceedings of the Fourth IEEE European Conference on Web Services (ECOWS 2006), 2006

Building Business Processes or Assembling Service Components: Reuse Services with BPEL4WS and SCA.
Proceedings of the Fourth IEEE European Conference on Web Services (ECOWS 2006), 2006

Semantic Matching of Web Services for Collaborative Business Processes.
Proceedings of the Computer Supported Cooperative Work in Design III, 2006

Semantic Matching of Web Services Based on Choreographies.
Proceedings of the 10th International Conference on CSCW in Design, 2006

2005
Semantics of Framed Temporal Logic Programs.
Proceedings of the Logic Programming, 21st International Conference, 2005

2004
A Framed Temporal Logic Programming Language.
J. Comput. Sci. Technol., 2004

1996
An extended interval temporal logic and a framing technique for temporal logic programming.
PhD thesis, 1996

1994
Projection in Temporal Logic Programming.
Proceedings of the Logic Programming and Automated Reasoning, 5th International Conference, 1994