Research

My research activities aim at building reliable and secure computer systems by developing formal frameworks which guarantee that software satisfies formally its specification, especially embedded safety-critical software such as automotive, avionic, and health-care applications. The construction of a formal framework involves the research and knowledge of principles of programming languages, compiler design and development, and formal methods including model checking, theorem proving, and static analysis for providing formal assurances that the specification is fulfilled.

A common theme is constructing correct Machine Learning-based safety-critical systems such as autonomous vehicles by applying formal verification including static analysis, model checking and correctness proof on the source code implementation, or mathematical models of these systems. One of the application is the correctness and robustness analysis of localization, perception, and motion planning software modules in the autonomous software stack. Another application is providing analysis w.r.t the safety standards such as ISO-26262-6 and SOTIF.

Research Projects

RAML, DANSE, DALI, VERISYNC, SCALP, AVOTE

Softwares

  • TaskFW: Task framework (TaskFW) is a infrastructure middle-ware layer on top of the Real-time Operating System (RTOS) QNX at Motional. It provides a set of fundamental services to enable safe and highly reliable autonomous vehicle software
  • RTVerifier: Run-Time Verifier (RTVerifier) is a tool that monitors the middle-ware layer of autonomous vehicle software system at APTIV Mobility at run-time to check that the failure recovery mechanism and inter-process communication satisfy their requirements
  • Absynth: Automatic Bound Synthesizer (Absynth) is a tool that automatically and statically computes upper bounds on the expected resource usage for imperative probabilistic programs, Tool and Benchmark
  • RAML: Resource Aware ML (RAML) is a tool that automatically and statically computes resource-use bounds (lower and upper) for OCaml programs. It also can check the constant resource-use programs used in preventing timing side-channel attacks, RAML
  • PSCV: A runtime verification tool for probabilistic SystemC models. It consists of two components: the plug-in for Plasma Lab in Java and tool for generating C++ monitor and aspect advices in C++, PSCV
  • Plasma Lab: Plasma Lab is a compact, efficient and flexible platform for statistical model checking of stochastic models, Plasma Lab
  • Polychrony: The Polychrony tool-set developed in C++ and Java, based on Signal, provides a formal framework to design, develop and validate critical systems, from abstract specification until deployment on distributed systems, Polychrony
  • SigCert: The tool developed in OCaml checks the correctness of the compilation of Signal compiler w.r.t clock semantics, data dependence, and value-equivalence (not fully implemented), SigCert
  • SigCV: PDS Simulation Relation Checking with SIGALI: implementation of the theory works in IFM 2012 article as the libraries in SIGALI tool-set, SigCV
  • Mobile Apps: Mobile applications: RATP, Turnstone, Saigon Places, A86, PhotoEnc,…on Apple AppStore

Development

  • Embedded software in Assembly, C/C++, and Ada for AVR, ARM, and Arduino Development Boards
  • Realtime OS (RTOS) such as QNX and FreeRTOS
  • Mobile embedded applications on iOS and Android
  • Software development in C/C++, OCaml, and Python

Review Activity

  • PC Member: Developments in Implicit Computational Complexity (DICE’18), Thessaloniki, Greece, April 2018
  • ACM Transactions on Programming Languages and Systems (TOPLAS’18), 2018
  • The 29th International Conference on Computer Aided Verification (CAV’17), Heidelberg, Germany, July 2017
  • The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’17), Barcelona, Spain, June 2017
  • The 26th International Conference on Compiler Construction (CC’17), Austin, Texas, US, February 2017
  • The 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD’16), Mountain View, CA, US, October 2016
  • The 27th International Conference on Concurrency Theory (CONCUR’16), Quebec City, Canada, August 2016
  • The 13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE’15), Austin, US, September 2015
  • The 8th International Conference on Language and Automata Theory and Applications (LATA’14), Madrid, Spain, March 2014