Publications

[PLDI] V.C. Ngo, Q. Carbonneaux, and J. Hoffmann. Bounded Expectations: Resource Analysis for Probabilistic Programs. In 2018 Programming Language Design and Implementation (PLDI). ACM, Philadelphia, PA, USA, June 2018.
[Long Version] [Tool and benchmark] [Acceptance Rate: 55/275 = 20.0%]

[JSEP] V.C. Ngo and A. Legay. Formal Verification of Probabilistic SystemC Models with Statistical Model Checking. In Journal of Software: Evolution and Process. Wiley, 2017 (Invited to submit an extended version of HASE paper). [Tool Implementation][Case Studies: Producer-Consumer, Control System, Random Scheduler][Tool Website]
[Oakland] V.C. Ngo, M. Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. Verifying and Synthesizing Constant-Resource Implementations with Types. To appear in 2017 IEEE Symposium on Security & Privacy (Oakland). IEEE, San Jose, CA, USA, May 2017. [Long Version] [Formalization][Tool Implementation] [Examples] [Acceptance Rate: 60/463 = 12.9%]

[CAV] V.C. Ngo, A. Legay, and V. Joloboff. PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. In Proceedings of 28th International Conference on Computer Aided Verification. Springer, Toronto, Ontario, Canada, July 2016. [Tool Implementation][Case Studies: Producer-Consumer, Control System, Random Scheduler][Tool Website] [Acceptance Rate: 58/195 = 29.7%]
[HASE] V.C. Ngo, A. Legay, and J. Quilbeuf. Statistical Model Checking for SystemC Models. In Proceedings of 17th High Assurance Systems Engineering Symposium. IEEE, Orlando, Florida, USA, January 2016. [Long Version][Tool Implementation][Tool Website] [Acceptance Rate: 32/78 = 41%]

[SCOPES] V.C. Ngo, J-P. Talpin, T. Gautier, L. Besnard, and P. Le Guernic. Modular Translation Validation of a Full-sized Synchronous Compiler using Off-the-shelf Verification Tools. In Proceedings of International Workshop on Software and Compilers for Embedded Systems, Invited Presentation. ACM, St. Goar, Germany, June 2015. [Tool Implementation] [Acceptance Rate: 8/18 = 44.4%]
[FORTE] V.C. Ngo, J-P. Talpin, and T. Gautier. Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. In Proceedings of 35th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems. IFIP, Grenoble, France, June 2015. [Long Version][Tool Implementation] [Acceptance Rate: 15/53 = 28.3%]
[FASE] V.C. Ngo, J-P. Talpin, T. Gautier, and P. Le Guernic. Translation Validation for Clock Transformations in a Synchronous Compiler. In Proceedings of 18th International Conference on Fundamental Approaches to Software Engineering. Springer, London, UK, April 2015. [Long Version][Tool Implementation] [Acceptance Rate: 23/80 = 28.7%]

[ESLsyn-DAC] V.C. Ngo, J-P. Talpin, and T. Gautier. Precise Deadlock Detection for Polychronous Data-flow Specifications. In Proceedings of the Electronic System Level Synthesis Conference. IEEE, San Francisco, CA, USA, June 2014.

[FCS] V.C. Ngo, J-P. Talpin, T. Gautier, P. Le Guernic, and L. Besnard. Formal Verification of Synchronous Data-flow Program Transformations Toward Certified Compilers. In Journal of Frontiers of Computer Science. Special Issue on Synchronous Programming, Springer, 2013.

[HLDVT] V.C. Ngo, J-P. Talpin, T. Gautier, P. Le Guernic, and L. Besnard. Formal Verification of Automatically Generated C-code from Polychronous Data-flow Equations. Accepted at International High-Level Design, Validation and Test Workshop. IEEE, California, USA, November 2012.
[IFM] V.C. Ngo, J-P. Talpin, T. Gautier, P. Le Guernic, and L. Besnard. Formal Verification of Compiler Transformations on Polychronous Equations. In Proceedings of 9th International Conference on Integrated Formal Methods. Springer, Pisa, Italy, June 2012. [Tool Implementation] [Acceptance Rate: 22/59 = 37%]

[ESORICS] C. Ene, Y. Lakhnech, and V.C. Ngo. Formal Indistinguishability Extended to the Random Oracle Model. In Proceedings of 14th European Symposium on Research in Computer Security. Springer, Saint-Malo, France, September 2009 (Main author, authors by alphabetical order). [Acceptance Rate: 42/220 = 19.1%]
[FCC] C. Ene, Y. Lakhnech, and V.C. Ngo. Formal Indistinguishability Extended to the ROM. In Proceedings of Workshop on Formal and Computational Cryptography, New York, USA, July 2009 (Main author, authors by alphabetical order).

V.C. Ngo, Q. Carbonneaux, and J. Hoffmann. Bounded Expectations: Resource Analysis for Probabilistic Programs. In CMU, Technical Report, June 2017.
V.C. Ngo, M. Fredrikson, and J. Hoffmann. Quantifying and Preventing Side Channels with Substructural Type Systems. In CMU, Technical Report, June 2016.
V.C. Ngo and A. Legay. Dependability Analysis of Embedded Control Systems Using SystemC and Statistical Model Checking. In HAL-INRIA, Technical Report RR-8762, July 2015.
V.C. Ngo, A. Legay, and J. Quilbeuf. Dynamic Verification of SystemC Specification with Statistical Model Checking. In HAL-INRIA, Technical Report RR-8644, October 2014.
V.C. Ngo, J-P. Talpin, T.Gautier, and P. Le Guernic. Evaluating SDVG Translation Validation: from Signal to C. In HAL-INRIA, Technical Report RR-8508, March 2014.
V.C. Ngo, J-P. Talpin, and P. Le Guernic. Formal Verification of Transformations on Abstract Clocks in Synchronous Compilers. In HAL-INRIA, Technical Report RR-8064, September 2012.
V.C. Ngo, J-P. Talpin, T. Gautier, P. Le Guernic, and L. Besnard. Formal Verification of Synchronous Data-flow Compilers. In HAL-INRIA, Technical Report RR-7921, April 2012.