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 embedded systems (i.e., control software in safety-critical systems, embedded system hardware designs) by applying formal verification including static analysis, model checking and correctness proof on the source code implementation, or mathematical models of these systems producing by model-based design tool-chains, and formally certifying the correctness of the compilers and code generators in the model-based design tool-chains.

Research Projects

RAML, DANSE, DALI, VERISYNC, SCALP, AVOTE

Softwares

  • 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
  • Mobile embedded applications on iOS and Android
  • Software development in C/C++, C Sharp, Java, 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