About me

  • I am a software engineer at IAR Systems Group AB. I have been developing a verification tool that can analyze real-world models. The topics of the job include State machine, Software verification, Symbolic model checking, and Binary Decision Diagram (BDD).

Recent News

  • Aug 10, 2019. A paper titled “Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency” was accepted in OOPSLA’19.
  • 1 Jun 2019. I started my job at IAR Systems.
  • March 2019 - May 2019. I worked as a reseacher in Department of Information Technology at Uppsala University with Prof. Bengt Jonsson.
  • 21 Jan, 2019. I defended my thesis and open for job opportunities in Sweden.
  • Oct 12, 2018. I will serve on the AEC of TACAS’19.
  • Nov 4 - Nov 9, 2018. I attended SPLASH’18 held in Boston, USA for a talk on our optimal stateless model checking technique for concurrent programs running under the Release-Acquire memory model. You can watch my video presentation video.
  • Aug 16, 2018. A paper titled “Optimal Stateless Model Checking under The Release-Acquire Semantics” was accepted in OOPSLA’18.
  • Jan 23, 2018: A journal paper titled “A Load-Buffer Semantics for Total Store Ordering” was accepted in LMCS. This is an extension of our CONCUR’16 paper “The Benefits of Duality in Verifying Concurrent Programs under TSO”.
  • Apr 22 - Apr 29, 2017. I attended ETAPS’17 held in Uppsala, Sweden for a talk on our context-bounded model checking technique for concurrent programs running under the POWER memory model.
  • Jan 20, 2017. Our TACAS’17 paper “Context-bounded Analysis for POWER” was nominated as one of the best papers in ETAPS’17.
  • Dec 22, 2016. A paper titled “Context-bounded Analysis for POWER” was accepted in TACAS’17.
  • Oct 2, 2016: We got an invitation to submit a journal version of our CONCUR’16 paper “The Benefits of Duality in Verifying Concurrent Programs under TSO” to the special issue of LMCS devoted to the conference.
  • Aug 23 - Aug 26, 2016. I attended CONCUR’16 held in Quebec, Canada for a talk on our novel Dual TSO memory model and its application to (parameterized) verification of concurrent programs running under the TSO memory model.
  • Jun 10, 2016. A paper titled “The Benefits of Duality in Verifying Concurrent Programs under TSO” was accepted in CONCUR’16.
  • May 13 - May 15, 2015. I attended NETYS’15 held in Agadir, Morocco for a talk on our fence insertion technique to automatically correct concurrent programs running under the PSO memory model.
  • Mar 16, 2015. A paper titled “Precise and Sound Automatic Fence Insertion Procedure under PSO” was accepted in NETYS’15.
  • Apr 14 - Apr 16, 2015. I attended ESOP’15 held in London, UK for a talk on our fence insertion technique to automatically correct concurrent programs running under the TSO memory model.
  • Feb 23 - Feb 24, 2015. I attended MM’15 held in Uppsala, Sweden for a talk on our fence insertion technique to automatically correct concurrent programs running under the TSO model.
  • Dec 14, 2014. A paper titled “The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO” was accepted in ESOP’15.