Rongjie Yan

 

Currently I am an Associate 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 of autonomous systems
  • 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, 2013,32(12):1920-1933.
  • Rongjie Yan, Min Yu, Kai Huang, Xiaomeng Zhang. Communication-oriented performance optimisation during code generation from Simulink models. IJES, 2014 6(2/3): 124-134. .
  • Kai Huang, Min Yu, Rongjie Yan, Xiaomeng Zhang, Xiaolang Yan, Lisane B. de Brisolara, Ahmed Amine Jerraya, Jiong Feng. Communication Optimizations for Multithreaded Code Generation from Simulink Models. TECS, 2015, 14(3): 59:1-59:26. .
  • Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan. Component-based verification using incremental design and invariants. SoSYM, 2016, 15(2): 427-451. .

Conference papers

  • Rongjie Yan, Anyu Cai, Hongyu Gao, Feifei Ma, Jun Yan. SMT-based Multi-objective Optimization for Scheduling of MPSoC Applications. TASE 2019.
  • Rongjie Yan, Junjie Yang, Di Zhu, Kai Huang: Design verification and validation for reliable safety-critical autonomous control systems. ICECCS 2018: 170-179.
  • Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang, Kai Huang: Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods. FM 2018: 294-311.
  • Dong Yan, Linjie Pan, Rongjie Yan, Jun Yan, Jian Zhang: Comprehensive Static Analysis for Configurable Software via Combinatorial Instantiation. COMPSAC (1) 2017: 67-74.
  • Rongjie Yan, Yupeng Zhou, Yige Yan, Minghao Yin, Min Yu, Feifei Ma, Kai Huang: A Hybrid Multi-objective Evolutionary Algorithm for Energy-Aware Allocation and Scheduling Optimization of MPSoCs. ICTAI 2017: 701-708.
  • Rongjie Yan, Chih-Hong Cheng, Yesheng Chai: Formal consistency checking over specifications in natural languages. DATE 2015: 1677-1682.
  • Xueyang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang, Guangquan Zhang: Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. FM 2015: 551-569.
  • Lavindra de Silva, Rongjie Yan, Felix Ingrand, Rachid Alami, Saddek Bensalem: A Verifiable and Correct-by-Construction Controller for Robots in Human Environments. HRI (Extended Abstracts) 2015: 281.
  • Rongjie Yan, De Ma, Kai Huang, Xiaoxu Zhang, Siwen Xiu: Annotation and analysis combined cache modeling for native simulation. ASP-DAC 2014: 406-411.
  • Rongjie Yan, Kai Huang, Min Yu, Xiaomeng Zhang. Communication pipelining for Code Generation from Simulink Models. TrustCom/ISPA/IUCC 2013: 1893-1900.
  • 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