Ximeng Li

Ximeng Li
Office: S2|02 E321
Phone: +49 6151 16-25257
Fax: +49 6151 16-25251
Mail: liatmais.informatik.tu-darmstadt.de

TU Darmstadt

Department of Computer Science

Modeling and Analysis of Information Systems

Hochschulstraße 10

D-64289 Darmstadt


GPG Key: 4096R/77486FD1, Fingerprint: 3DB1 E8A0 D0D1 6DD5 93D1 2274 FF13 2DD0 7748 6FD1

Short Bio

I obtained my MSc degree with a thesis on model checking concurrent programs late 2012, and my PhD degree in the information flow security of concurrent programs early 2016, both from the Technical University of Denmark. My PhD was under the supervision of Prof. Flemming Nielson and Prof. Hanne Riis Nielson, and contributed to the European Artemis project SESAMO.
I joined MAIS as a Postdoc under the supervision of Prof. Dr. Heiko Mantel from 2016 to 2018. My research at MAIS was concerned with:
  • the compositional verification of security for concurrent programs, using rely-guarantee-style reasoning
  • the verification of data and information flow security for large software systems across the application-library boundary
I contributed to the CRISP project funded by the German Federal Ministry of Education and Research.


My research interest lies in the verification of security and safety properties for concurrent and distributed systems via formal methods. In particular, the methods I develop include type systems, techniques for compositional reasoning, and state-space-based techniques. I am also interested in formal verification using the proof assistant Coq.



Ximeng Li, Heiko Mantel and Markus Tasch. Taming Message-passing Communication in Compositional Reasoning about Confidentiality.   In Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS), pp. 45 - 66. 

Ximeng Li, Xi Wu, Alberto Lluch-Lafuente, Flemming Nielson, and Hanne Riis Nielson. A Coordination Language for Databases. Logical Methods in Computer Science, Vol 13(1:10), pp. 1-51.

Ben Hermann, Ximeng Li, Heiko Mantel, Mira Mezini, Markus Tasch, and Florian Wendel. Requirements for a Specification Language for Data and Information Flow, and A Literature Review of Analytical and Constructive Research on the Java Native Interface. TU Darmstadt, Technical Report TUD-CS-2017-0025.


Kevin Müller, Sascha Uhrig, Flemming Nielson, Hanne Riis Nielson, Ximeng Li, Michael Paulitsch, and Georg Sigl. Automatic Information Flow Validation for High Assurance Systems. International Journal on Advances in Software, Vol 9 (3&4), pp. 191-206.

Ximeng Li, Flemming Nielson, and Hanne Riis Nielson. Future-dependent Flow Policies with Prophetic Variables. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS), pp. 29 - 42.


Ximeng Li, Flemming Nielson, and Hanne Riis Nielson. Factorization of Behavioral Integrity. In Proceedings of the 20th European Symposium on Research in Computer Security (ESORICS), pp. 500 - 519.

Ximeng Li, Flemming Nielson, Hanne Riis Nielson, and Xinyu Feng. Disjunctive Information Flow for Communicating Processes. In Proceedings of the 10th International Symposium on Trustworthy Global Computing (TGC), pp. 95 - 111.

Hanne Riis Nielson, Flemming Nielson, and Ximeng Li. Hoare Logic for Disjunctive Information Flow. In Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday, pp. 47 - 65.

Xi Wu, Ximeng Li, Alberto Lluch-Lafuente, Flemming Nielson, and Hanne Riis Nielson. Klaim-DB: A Modeling Language for Distributed Database Applications. In Coordination Models and Languages - 17th {IFIP} {WG} 6.1 International Conference (Coordination), pp. 197 - 212


I have been involved in the following courses:
Winter Term 2017/2018: Assistant for the course Static and Dynamic Program Analysis (SDPA)
Summer Term 2017: Assistant for the course Formal Methods for Information Security (FMIS)
Winter Term 2016/2017: Assistant for Current Topics Seminar: Computer Security Foundations

Services to the Scientific Community

I have reviewed for: S&P 2014, NordSec 2014, FM 2016, ECOOP 2017, ESORICS 2017.
A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang