Professor of Computer Science
School of Computer Science and Software Engineering
East China Normal University
3663 North Zhongshan Road
Shanghai 200062
China
Phone: +86 21 62231281
Fax: +86 21 62235255
Email: yxdeng (AT) sei.ecnu.edu.cn
Web: http://basics.sjtu.edu.cn/~yuxin


I am a member of BASICS (by courtesy) at Shanghai Jiao Tong University.
My research interests include concurrency theory, programming semantics, type theory, and models for probabilistic computation.
Teaching
Selected Publications
 Ming Xu and Yuxin Deng.
TimeBounded Termination Analysis for Probabilistic Programs with Delays.
Information and Computation 275, 104634, 2020.
[PDF],
[Abstract],
[Bib]
 Xin Li, Patrick Gardy, Yuxin Deng, and Hiroyuki Seki.
Reachability of Patterned Conditional Pushdown Systems.
Journal of Computer Science and Technology 35(6): 12951311, 2020.
[PDF],
[Abstract],
[Bib]
 Hua Wu, Yuxin Deng, Ming Xu, and Wenjie Du.
Qsimulation V2.0: An Optimized Quantum Simulator.
In Proceedings of the 17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020), Lecture Notes in Computer Science 12545, pages 307316. Springer, 2020.
[PDF],
[Abstract],
[Bib]
 Xudong Qin, Yuxin Deng, and Wenjie Du.
Verifying Quantum Communication Protocols with Ground Bisimulation.
In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Lecture Notes in Computer Science 12079, pages 2138. Springer, 2020.
[PDF],
[Abstract],
[Bib]
 Xudong Qin, Simon Bliudze, Eric Madelaine, Zechen Hou, Yuxin Deng, and Min Zhang.
SMTBased Generation of Symbolic Automata.
Acta Informatica 57:627656, 2020.
[PDF],
[Abstract],
[Bib]
 Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu.
Proving Expected Sensitivity of Probabilistic Programs with Randomized VariableDependent Termination Time.
In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), PACMPL 4, Article 25, 2020.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and JeanFrancois Monin.
Formalisation of Probabilistic Testing Semantics in Coq.
In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy  Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, Lecture Notes in Computer Science 11760, pages 276292. Springer, 2019.
[PDF],
[Abstract],
[Bib]
 Patrick Gardy and Yuxin Deng.
Simulations for MultiAgent Systems with Imperfect Information.
In Proceedings of the 21st International Conference on Formal Engineering Methods (ICFEM'19)., Lecture Notes in Computer Science 11852, pages 138153. Springer, 2019.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng
Bisimulations for Probabilistic and Quantum Processes (Invited Paper).
In Proceedings of the 29th International Conference on Concurrency Theory (CONCUR'18), LIPIcs 118, pages 2:12:14. Schloss Dagstuhl  LeibnizZentrum fuer Informatik, 2018.
[PDF],
[Abstract],
[Bib]
 Hengyang Wu and Yuxin Deng.
DistributionBased Behavioural Distance for Nondeterministic Fuzzy Transition Systems.
IEEE Transactions on Fuzzy Systems 26(2): 416429, 2018.
[PDF],
[Abstract],
[Bib]
 Hengyang Wu, Yixiang Chen, Tianming Bu, and Yuxin Deng.
Algorithmic and Logical Characterizations of Bisimulation for Nondeterministic Fuzzy Transition Systems.
Fuzzy Sets and Systems 333: 106123, 2018.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Yuan Feng.
Probabilistic Bisimilarity as Testing Equivalence.
Information and Computation 257: 5864, 2017.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Yuan Feng.
Bisimulations for Probabilistic Linear Lambda Calculi.
In Proceedings of the 11th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'17), pages 18. IEEE Computer Society, 2017.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Min Zhang, and Guoqing Lei.
An Algebraic Approach to Automatic Reasoning for NetKAT Based on its Operational Semantics.
In Proceedings of the 19th International Conference on Formal Engineering Methods (ICFEM'17)., Lecture Notes in Computer Science 10610, pages 464480. Springer, 2017.
[PDF],
[Abstract],
[Bib]
 Chen Fu, Yuxin Deng, David N. Jansen, and Lijun Zhang.
On Equivalence Checking of Nondeterministic Finite Automata.
In Proceedings of the 3rd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA'17), Lecture Notes in Computer Science 10606, pages 216231. Springer, 2017.
[PDF],
[Abstract],
[Bib]
 Wenjie Du, Yuxin Deng, and Daniel Gebler.
Behavioural Pseudometrics for Nondeterministic Probabilistic Systems.
In Proceedings of the 2nd International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA'16), Lecture Notes in Computer Science 9984, pages 6784. Springer, 2016.
[PDF],
[Abstract],
[Bib]
 Hengyang Wu and Yuxin Deng.
Logical Characterizations of Simulation and Bisimulation for Fuzzy Transition Systems.
Fuzzy Sets and Systems 301: 1936, 2016
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Yuan Feng, and Ugo Dal Lago.
On Coinduction and Quantum Lambda Calculi.
In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR'15), LIPIcs 42, pages 427440. Schloss Dagstuhl  LeibnizZentrum fuer Informatik, 2015.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Yu Zhang.
Program Equivalence in Linear Contexts.
Theoretical Computer Science, 585: 7190, 2015.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob J. Simmons, and Iliano Cervesato.
Relating Reasoning Methodologies in Linear Logic and Process Algebra.
Mathematical Structures in Computer Science, pages 139. Cambridge University Press, December 2014.
[PDF],
[Abstract],
[Bib]
 Yuan Feng, Yuxin Deng, and Mingsheng Ying.
Symbolic bisimulation for quantum processes.
ACM Transactions on Computational Logic, Vol. 15, No. 2, Article 14, April 2014.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.
RealReward Testing for Probabilistic Processes.
Theoretical Computer Science, 538:1636, June 2014.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Hengyang Wu.
Modal Characterisations of Probabilistic and Fuzzy Bisimulations.
In Proceedings of the 16th International Conference on Formal Engineering Methods (ICFEM'14). Lecture Notes in Computer Science 8829, pages 123138. Springer, 2014.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Matthew Hennessy.
Compositional Reasoning for Weighted Markov Decision Processes.
Science of Computer Programming, 78: 25372579, 2013.
[PS],
[PDF],
[Abstract],
[Bib]
 Xiaojie Deng, Yu Zhang, Yuxin Deng and Farong Zhong.
The Buffered PiCalculus: A Model for Concurrent Languages.
In Proceedings of the 7th International Conference on Language and Automata Theory and Applications (LATA'13). Lecture Notes in Computer Science 7810, pages 250261. Springer, 2013.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Yuan Feng.
Open Bisimulation for Quantum Processes.
In Proceedings of the 7th IFIP International Conference on Theoretical Computer Science (TCS'12). Lecture Notes in Computer Science 7604, pages 119133. Springer, 2012.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Alwen Tiu.
Characterisations of Testing Preorders for a Finite Probabilistic PiCalculus.
Formal Aspects of Computing, 24(46):701726, 2012.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Robert J. Simmons, and Iliano Cervesato.
Relating Reasoning Methodologies in Linear Logic and Process Algebra.
In Proceedings of the 2nd International Workshop on Linearity (LINEARITY'12). Electronic Proceedings in Theoretical Computer Science 101: 5060, 2012.
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Matthew Hennessy.
On the Semantics of Markov Automata.
In Proceedings of the 38th International Colloquium on Automata,
Languages and Programming (ICALP'11). Lecture Notes in Computer
Science 6756, pages 307318. Springer, 2011.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Matthew Hennessy.
On the Semantics of Markov Automata.
Information and Computation, 222:139168, 2013. (Special issue of ICALP'11, track B).
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Wenjie Du.
Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation.
Technical Report CMUCS11110, Carnegie Mellon University, 2011.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Stephane Grumbach, and JeanFrancois Monin.
A Framework for Verifying DataCentric Protocols.
In Proceedings of the 13th IFIP International Conference on Formal
Methods for Objectbased Distributed Systems & the 31th IFIP
International Conference on Formal Techniques for Networked and
Distributed Systems (FMOODS & FORTE'11), Lecture Notes in
Computer Science 6722, pages 106120. Springer, 2011.
[PS],
[PDF],
[Abstract],
[Bib],
[Full version]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.
RealReward Testing for Probabilistic Processes.
In Proceedings of the 9th Workshop on Quantitative Aspects of
Programming Languages (QAPL'11). Electronic Proceedings in Theoretical Computer Science 57: 6173. 2011.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Matthew Hennessy.
Compositional Reasoning for Markov Decision Processes (Extended Abstract).
In Proceedings of the 4th International Conference on Foundamentals of Software Engineering (FSEN'11). Lecture Notes in Computer Science 7141, pages 143157. Springer, 2012.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Rob van Glabbeek.
Characterising Probabilistic Processes Logically.
In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'10), Lecture Notes in Computer Science 6397, pages 278293. Springer, 2010.
[PS],
[PDF],
[Abstract],
[Bib]
 Xiangxi Li, Yu Zhang, and Yuxin Deng.
Verifying Anonymous Credential Systems in Applied Pi Calculus.
In Proceedings of the 8th International Conference on Cryptology and Network Security (CANS'09), Lecture Notes in Computer Science 5888, pp.209225. Springer, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Wenjie Du.
A Local Algorithm for Checking Probabilistic Bisimilarity.
In Proceedings of the 4th International Conference on Frontier of Computer Science and Technology (FCST'09), pp. 401407. IEEE Computer Society, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Wenjie Du and Yuxin Deng.
On Mobility and Communication.
In Proceedings of the 5th International Symposium on Domain Theory (ISDT'09), Electronic Notes in Theoretical Computer Science 257:1933. Elsevier, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.
Testing Finitary Probabilistic Processes (Extended Abstract).
In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR'09), Lecture Notes in Computer Science 5710, pp. 274288. Springer, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and JeanFrancois Monin.
Verifying Selfstabilizing Population Protocols with Coq.
In Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09), pp. 201208. IEEE Computer Society, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Wenjie Du.
Kantorovich Metric in Computer Science: A Brief Survey.
In Proceedings of the 7th Workshop on Quantitative Aspects of
Programming Languages (QAPL'09), Electronic Notes in Theoretical Computer Science 253(3):7382. Elsevier, 2009.
[PS],
[PDF],
[Abstract],
[Bib]
 Xin Chen and Yuxin Deng.
Game Characterizations of Process Equivalences.
In Proceedings of the 6th Asian Symposium on Programming Languages and Systems (APLAS'08)
, Lecture Notes in Computer Science 5356, pp. 107121. Springer, 2008.
[PS],
[PDF],
[Abstract],
[Bib]
 Jun Pang, Zhengqin Luo, and Yuxin Deng.
On Automatic Verification of Selfstabilizing Population Protocols.
In Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'08), pp. 185192. IEEE Computer Society, 2008.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng.
A simple completeness proof for the axiomatisations of weak
behavioural equivalences.
Bulletin of the European Association for Theoretical
Computer Science 93: 207219, 2007.
[PS],
[PDF],
[Abstract],
[Bib],
[Full version]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan, and Chenyi Zhang.
Characterising Testing Preorders for Finite Probabilistic Processes (Extended Abstract).
In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS'07), pp. 313325. IEEE Computer Society, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.
Characterising Testing Preorders for Finite Probabilistic Processes.
In Logical Methods in Computer Science, 4(4:4): 133, 2008.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan, and Chenyi Zhang.
Remarks on Testing Probabilistic Processes.
In Computation, Meaning, and Logic: Articles dedicated to Gordon
Plotkin (L. Cardelli, M. Fiore and G. Winskel, Eds.), Electronic
Notes in Theoretical Computer Science, 172: 359397, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Rob van Glabbeek, Carroll Morgan, and Chenyi Zhang.
Scalar Outcomes Suffice for Finitary Probabilistic Testing.
In Proceedings of the 16th European Symposium on Programming (ESOP'07)
, Lecture Notes in Computer Science 4421, pp. 363378.
Springer, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Wenjie Du.
Probabilistic Barbed Congruence.
In Proceedings of the 5th Workshop on Quantitative Aspects of
Programming Languages (QAPL'07), Electronic Notes in Theoretical
Computer Science 190(3), pp. 185203. Elsevier, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Lin Song, Yuxin Deng, and Xiaojuan Cai.
Towards automatic measurement of probabilistic processes.
In Proceedings of the 7th International Conference on Quality
Software (QSIC'07), pp. 5059. IEEE Computer Society, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Zhengqin Luo, Xiaojuan Cai, Jun Pang, and Yuxin Deng.
Analyzing an Electronic Cash Protocol Using Applied Pi Calculus.
In Proceedings of the 5th International Conference on
Applied Cryptography and Network Security (ACNS'07),
Lecture Notes in Computer Science 4521, pp. 87103.
Springer, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Jun Pang, and Peng Wu.
Measuring Anonymity with Relative Entropy.
In Proceedings of the 4th International Workshop on Formal Aspects
in Security and Trust (FAST'06), Lecture Notes in Computer
Science 4691, pp. 6579. Springer, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Catuscia Palamidessi, and Jun Pang.
Compositional Reasoning for Probabilistic FiniteState Behaviors.
In Processes, Terms and Cycles: Steps on the Road to Infinity,
Essays Dedicated to Jan Willem Klop, on the Occasion of
His 60th Birthday, Lecture Notes in Computer Science 3838,
pp. 309337. Springer, 2005.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Catuscia Palamidessi, and Jun Pang.
Weak probabilistic anonymity.
In Proceedings of the 3rd International Workshop on Security
Issues in Concurrency (SecCo'05), Electronic Notes in Theoretical
Computer Science 180(1):5576. Elsevier, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang.
Metrics for actionlabelled quantitative transition systems.
In Proceedings of the 3rd Workshop on Quantitative Aspects of
Programming Languages (QAPL'05), Electronic Notes in Theoretical
Computer Science 153(2), pp. 7996. Elsevier, 2006.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Catuscia Palamidessi.
Axiomatizations for probabilistic finitestate behaviors (Extended Abstract).
In Proceedings of the 8th International Conference on Foundations
of Software Science and Computation Structures (FOSSACS'05),
Lecture Notes in Computer Science 3441, pp. 110124. Springer, 2005.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Catuscia Palamidessi.
Axiomatizations for probabilistic finitestate behaviors.
Theoretical Computer Science, 373(12): 92114, 2007.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Davide Sangiorgi.
Ensuring termination by typability (Extended Abstract).
In Proceedings of the 3rd IFIP International Conference on
Theoretical Computer Science (TCS'04), pp. 619632. Kluwer, 2004.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Davide Sangiorgi.
Ensuring termination by typability.
Information and Computation, 204(7): 10451082, 2006.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Davide Sangiorgi.
Towards an algebraic theory of typed mobile processes (Extended Abstract).
An early version appeared in Proceedings of the 31st
International Colloquium on Automata, Languages and Programming
(ICALP'04), Lecture Notes in Computer Science 3142, pp. 445456.
Springer, 2004.
[PS],
[PDF],
[Abstract],
[Bib]
 Yuxin Deng and Davide Sangiorgi.
Towards an algebraic theory of typed mobile processes.
Theoretical Computer Science, 350(23): 188212, 2006.
(Special issue of ICALPB 2004, D. Sannella, Ed.)
[PS],
[PDF],
[Abstract],
[Bib]
Miscellaneous: