Yuxin Deng's home page

Department of Computer Science
School of Electronics and Informatics
Shanghai Jiaotong University
800 Dongchuan Road
Shanghai 200240
China

Tel: +86 21 34205060 EXT. 601
Fax: +86 21 34204728
Email: deng-yx AT cs . sjtu . edu . cn

Web: http://basics.sjtu.edu.cn/~yuxin

My research interests include concurrency theory, programming semantics, type theory, and models for probabilistic computation.

Teaching

Fall 2010: Data Structures and Algorithms. The slides are available here.
Spring 2010: Formal Semantics of Programming Languages. The slides are available [PDF].
Fall 2009: Discrete Mathematics
Fall 2009: Data Structures and Algorithms
Spring 2009: Discrete Mathematics.
Spring 2009: Programming semantics. The lecture notes on probabilistic concurrency are available here.
Fall 2008: Discrete Mathematics.
Fall 2008: Data Structures and Algorithms.
Spring 2008: Programming semantics.
Spring 2008: Introduction to Software Engineering.
Fall 2007: Data Structures and Algorithms.

Selected Publications

Yuxin Deng.
Axiomatisations and Types for Probabilistic and Mobile Processes.
PhD thesis, Ecole des Mines de Paris, France, July 2005.
[PS], [PDF], [Abstract], [Bib], [My thesis defense]

Yuxin Deng and Alwen Tiu.
Characterisations of Testing Preorders for a Finite Probabilistic Pi-Calculus.
Formal Aspects of Computing. 2012. To appear.
[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). 2012. To appear.
[PDF], [Abstract], [Bib]

Yuxin Deng, Robert J. Simmons, and Iliano Cervesato.
Relating Reasoning Methodologies in Linear Logic and Process Algebra.
Technical Report CMU-CS-11-145, Carnegie Mellon University, 2011.
[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 307-318. Springer, 2011.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Matthew Hennessy.
On the Semantics of Markov Automata.
Information and Computation, (Special issue of ICALP'11). 2011. To appear.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Wenjie Du.
Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation.
Technical Report CMU-CS-11-110, Carnegie Mellon University, 2011.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng, Stephane Grumbach, and Jean-Francois Monin.
A Framework for Verifying Data-Centric Protocols.
In Proceedings of the 13th IFIP International Conference on Formal Methods for Object-based 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 106-120. Springer, 2011.
[PS], [PDF], [Abstract], [Bib], [Full version]

Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan.
Real-Reward 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: 61-73. 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). 2011. To appear.
[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 278-293. 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.209-225. 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. 401-407. 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:19-33. 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. 274-288. Springer, 2009.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Jean-Francois Monin.
Verifying Self-stabilizing Population Protocols with Coq.
In Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'09), pp. 201-208. 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):73-82. 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. 107-121. Springer, 2008.
[PS], [PDF], [Abstract], [Bib]

Jun Pang, Zhengqin Luo, and Yuxin Deng.
On Automatic Verification of Self-stabilizing Population Protocols.
In Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE'08), pp. 185-192. 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: 207-219, 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. 313-325. 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): 1-33, 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: 359-397, 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. 363-378. 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. 185-203. 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. 50-59. 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. 87-103. 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. 65-79. Springer, 2007.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng, Catuscia Palamidessi, and Jun Pang.
Compositional Reasoning for Probabilistic Finite-State 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. 309-337. 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):55-76. Elsevier, 2007.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang.
Metrics for action-labelled 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. 79-96. Elsevier, 2006.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Catuscia Palamidessi.
Axiomatizations for probabilistic finite-state 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. 110-124. Springer, 2005.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Catuscia Palamidessi.
Axiomatizations for probabilistic finite-state behaviors.
Theoretical Computer Science, 373(1-2): 92-114, 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. 619-632. Kluwer, 2004.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Davide Sangiorgi.
Ensuring termination by typability.
Information and Computation, 204(7): 1045-1082, 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. 445-456. Springer, 2004.
[PS], [PDF], [Abstract], [Bib]

Yuxin Deng and Davide Sangiorgi.
Towards an algebraic theory of typed mobile processes.
Theoretical Computer Science, 350(2-3): 188-212, 2006. (Special issue of ICALP-B 2004, D. Sannella, Ed.)
[PS], [PDF], [Abstract], [Bib]

Miscellaneous:

�