49 citations · 223 across the 35 of their papers we have counts for
8 papers · 1 filter
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Taolue Chen, Matthew Hague, Jinlong He +4
Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths…
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
Chong Gao, Taolue Chen, Zhilin Wu
We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic con…
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague +2
Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strin…
On the Axiomatizability of Impossible Futures
Taolue Chen, Wan Fokkink, Rob van Glabbeek
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the proc…
On the Total Variation Distance of Labelled Markov Chains
Taolue Chen, Stefan Kiefer
Labelled Markov chains (LMCs) are widely used in probabilistic verification, speech recognition, computational biology, and many other fields. Checking two LMCs for equivalence is…
Model Checking Stochastic Branching Processes
Taolue Chen, Klaus Dräger, Stefan Kiefer
Stochastic branching processes are a classical model for describing random trees, which have applications in numerous fields including biology, physics, and natural language proces…
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen +1
We study the verification of a finite continuous-time Markov chain (CTMC) C against a linear real-time specification given as a deterministic timed automaton (DTA) A with finite or…
On Finite Bases for Weak Semantics: Failures versus Impossible Futures
Taolue Chen, Wan Fokkink, Rob van Glabbeek
We provide a finite basis for the (in)equational theory of the process algebra BCCS modulo the weak failures preorder and equivalence. We also give positive and negative results re…