Rongjie Yan

 

Currently I am an Assistant Researcher in Laboratory of Computer Science, Institute of Software,Chinese Academy of Sciences
Phone: +86 10 62661654       

Email: yrj at ios.ac.cn

Room 332, No.5 Building

Beijing, 100190, P. R. China 

กก

Research Interests

  • Verification
  • System Modeling
  • Formal Methods
  • Software Engineering
  • Component-based Development

Tools (collaborated)

  • SpecCC. A tool for consistency checking of requirements in natural language.
  • DFinder. A toolset for compositional deadlock detection and verification.
  • CTAV/LTL. An LTL model checker for real time systems modeled by closed timed automata.
  • CTAV/Reach. A tool for reachability analysis of real time systems modeled by closed timed automata.
  • FPTA. A verifier for reachability analysis of real time systems modeled by finite precision timed automata.
  • XYZ/E development environment.

Recent Papers

Journal papers

  • Saddek Bensalem, Lavindra De Silva, Felix Ingrand, and Rongjie Yan. A Verifiable and Correct-by-Construction Controller for Robot Functional Levels. Joser, 2011, Vol 2, No 1:1-19(pdf).
  • De Ma, Rongjie Yan, Kai Huang, Min Yu, Haitong Ge, Xiaolang Yan, A. Jerraya. Performance Estimation Techniques with MPSoC Transaction-Accurate Model. TCAD, accepted.

Conference papers

  • Rongjie Yan, Kai Huang, Min Yu, Xiaomeng Zhang. Communication pipelining for Code Generation from Simulink Models. M2A2 2013, accepted.
  • Chih-Hong Cheng, Rongjie Yan, Harald Ruess, Saddek Bensalem. Distributed Priority Synthesis using Knowledge. AGERE!@SPLASH 2012.
  • Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem, Harald Ruess: Distributed Priority Synthesis. The 7th International Conference on Systems Software Verification. SSV 2012: 57-72.
  • Chih-Hong Cheng, Saddek Bensalem, Yu-Fang Chen, Rongjie Yan, Barbara Jobstmann, Harald Ruess, Christian Buckl and Alois knoll. Algorithms for Synthesizing Priorities in Component-based Systems. ATVA11.
  • Saddek Bensalem, Lavindra De Silva, Andreas Griesmayer, Felix Ingrand, Axel Legay and Rongjie Yan. A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems SC11.
  • Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis and Rongjie Yan. D-Finder 2: Towards Efficient Correctness of Incremental Design. NASA Formal Methods 2011: 453-458.
  • Chih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann, Rongjie Yan, Alois Knoll and Harald Ruess. Model Construction and Priority Synthesis for Simple Interaction Systems. NASA Formal Methods 2011: 466-471.
  • Saddek Bensalem, Marius Bozga, Axel Legay, Thanh Hung Nguyen, Joseph Sifakis and Rongjie Yan. Incremental Component-based Construction and Verification using Invariants. FMCAD10 .
  • Saddek Bensalem, Axel Legay, Thanh Hung Nguyen, Joseph Sifakis and Rongjie Yan. Incremental Invariant Generation for Compositional Design. TASE10.
  • Saddek Bensalem, Lavindra de Silva, Matthieu Gallien, Felix Ingrand, Rongjie Yan.  ``Rock Solid'' Software: A Verifiable and Correct-by-Construction Controller for Rover and Spacecraft Functional Levels. ISAIRAS10.
  • Saddek Bensalem, Lavindra de Silva, Matthieu Gallien, Felix Ingrand, Rongjie Yan. A Verifiable and Correct by Construction Controller for Robots in Human Environment. DRHE10.
  • Rongjie Yan, Guangyuan Li, Wenliang Zhang and Yunquan Peng. Improvements for the Symbolic Verification of Timed Automata(pdf, slide). FORTE07.
  • Rongjie Yan, Guangyuan Li, Zhisong Tang. Symbolic Model Checking of Finite Precision Timed Automata(pdf,slide). ICTAC05.

Papers in Chinese

  • Rongjie Yan, Wenliang Zhang, Zhisong Tang. Truly Bitstate-hashing for SCC-based Emptiness Checking Algorithms, Chinese Journal of Computers, 2008, 6: 979-988.
  • Rongjie Yan, Guangyuan Li, Yubo Xu, Chunming Liu, Zhisong Tang. Reachability Checking of Finite Precision Timed Automata. Software Journal, 2006, 17(1): 1-10.
  • Rongjie Yan, Guangquan Zhang. Component-based Software Architecture Refinement and Its Application. Journal of Chongqing Normal University (Natural Science Edition), 2003, 20(2): 1-5.

Techniques Reports

  • Saddek Bensalem, Axel Legay, Thanh Hung Nguyen, Joseph Sifakis and Rongjie Yan. Incremental Invariant Generation for Compositional Design, Verimag Technical Report number TR-2010-6, Feb, 2010.
  • Saddek Bensalem, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan: Incremental Component-based Construction and Deadlock Checking, Verimag Technical Report number TR-2009-12, Sep 2009.
  • Rongjie Yan, Chunming Liu, Yubo Xu. User Manual for FPTA Verifier. Technical Reports of State Key Laboratory of Computer Science, ISCAS-LCS-04-01 (in Chinese).

Invited Talks

  • XYZ System and its Features, Jun. 2008, Xi'an
  • Concurrent System Modeling and Verification, May 2005, Suzhou

Some Links

CADP case studies, BEEP case studies

Spin, Uppaal, NuSMV, CUDD manual,

LTL to automata

C Minor, Coq Cooker, Coq online Compcert C, Online document

Online dictionary

Publication resources

Software theory, Dates of conferences

Software engineering, Dates of conferences

High performance computing, Dates of conferences