# Cong Tian

According to our database

^{1}, Cong Tian## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2017

Two-layer hybrid peer-to-peer networks.

Peer-to-Peer Networking and Applications, 2017

MSVL: a typed language for temporal logic programming.

Frontiers of Computer Science, 2017

Model Checking Multi-agent Systems with APTL.

Ad Hoc & Sensor Wireless Networks, 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

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

Model checking concurrent systems with MSVL.

SCIENCE CHINA Information Sciences, 2016

A Proof System for MSVL Programs in Coq.

Proceedings of the Structured Object-Oriented Formal Language and Method, 2016

How android app developers manage power consumption?: an empirical study by mining power management commits.

Proceedings of the 13th International Conference on Mining Software Repositories, 2016

A Decision Procedure for a Fragment of Linear Time Mu-Calculus.

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 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

Verifying OSEK/VDX applications: An optimized SMT-based bounded model checking approach.

Proceedings of the 15th IEEE/ACIS International Conference on Computer and Information Science, 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

Extending PPTL for Verifying Heap Evolution Properties.

CoRR, 2015

An Improved Decision Procedure for Linear Time Mu-Calculus.

CoRR, 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

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

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

Buchi Determinization Made Tighter.

CoRR, 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

Towards more accurate content categorization of API discussions.

Proceedings of the 22nd International Conference on Program Comprehension, 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

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

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

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

2011

Expressiveness of propositional projection temporal logic with star.

Theor. Comput. Sci., 2011

Detecting Spurious Counterexamples Efficiently in Abstract Model Checking

CoRR, 2011

Synthesising Classic and Interval Temporal Logic.

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Focus Game for Projection Temporal Logic.

Proceedings of the 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, 2011

Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates.

Proceedings of the Fourth IEEE International Conference on Software Testing, 2011

Making Abstraction-Refinement Efficient in Model Checking.

Proceedings of the Computing and Combinatorics - 17th Annual International Conference, 2011

2010

Making Abstraction Refinement Efficient in Model Checking

CoRR, 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

Complexity of propositional projection temporal logic with star.

Mathematical Structures in Computer Science, 2009

A note on stutter-invariant PLTL.

Inf. Process. Lett., 2009

2008

A decision procedure for propositional projection temporal logic with infinite models.

Acta Inf., 2008

Propositional Projection Temporal Logic, Bchi Automata and omega-Regular Expressions.

Proceedings of the Theory and Applications of Models of Computation, 2008

A Unified Model Checking Approach with Projection Temporal Logic.

Proceedings of the Formal Methods and Software Engineering, 2008

2007

Decidability of Propositional Projection Temporal Logic with Infinite Models.

Proceedings of the Theory and Applications of Models of Computation, 2007

Model Checking Propositional Projection Temporal Logic Based on SPIN.

Proceedings of the Formal Methods and Software Engineering, 2007