Thao Dang

Computing reachable states for nonlinear biological models.
Thao Dang, Colas Le Guernic, and Oded Maler.
Theoretical Computer Science, 2010. [pdf]

Coverage-Guided Test Generation for Continuous and Hybrid Systems
Thao Dang and Tarik Nahhal.
Journal Formal Methods in System Design, Jan 2009, [pdf].

Scheduling of multi-threaded real-time programs using geometry of timed PV diagrams
Thao Dang and Philippe Gerner.
ACM Transactions on Embedded Computing Systems, submitted, Jan 2007.

Hybridization Methods for the Analysis of Non-Linear Systems.
Eugene Asarin, Thao Dang, and Antoine Girard
Acta Informatica, 43(7):451-476, 2007. [pdf]

Counter-Example Guided Predicate Abstraction of Hybrid Systems.
Rajeev Alur, Thao Dang, and Franjo Ivancic.
Journal of Theoretical Computer Science TCS, v.354 n.2, p.250-271, 28 March 2006. [pdf]

Reachability Analysis of Hybrid Systems via Predicate Abstraction.
Rajeev Alur, Thao Dang, and Franjo Ivancic.
ACM transactions on embedded computing systems TECS, v.5 n.1, p.152-199, February 2006, [pdf]

Application of Reachability Analysis to Idle Speed Control Synthesis.
Thao Dang
International Journal of Software Engineering and Knowledge Engineering IJSEKE, May 2005.

Hierarchical Modeling and Analysis of embedded systems.
R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky.
Proceedings of the IEEE, October 2002. [pdf]

Model-based Testing of Hybrid Systems. Thao Dang.
Monograph in Model-Based Testing for Embedded Systems, CRC Press, 2010. [pdf]

Modeling, Verification and Testing using Timed and Hybrid Automata
Stavros Tripakis and Thao Dang.
Chapter in Book Model-based Design of Heterogeneous Systems, CRC Press, 2009. [pdf]

Outils pour l'analyse des modèles hybrides.
Thao Dang, Goran Frehse, Antoine Girard, and Colas Le Guernic.
Chapter in Olivier Roux and Claude Jard, editors, Approches formelles des systèmes embarqués communicants,
Traité IC2, série Informatique et systèmes d'information, pages 245-268. Hermes Lavoisier, 2008. [pdf]

Time Elapse over Template Polyhedra in Polynomial Time through Max-Strategy Iteration.
Thao Dang and Thomas Martin Gawlitza.
APLAS 2011, Ninth Asian Symposium on Programming Languages and Systems, LNCS, Springer, Taiwan, 2011. [pdf]

Discretizing Affine Hybrid Automata with Uncertainty.
Thao Dang and Thomas Martin Gawlitza.
AVTA 2011, Int. Symposium on Automated Technology for Verification and Analysis, LNCS, Springer, October 2011, Taiwan. [pdf]

SpaceEx: Scalable Verification of Hybrid Systems.
Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, Oded Maler.
CAV 2011, LNCS, Springer, 379-395, July 2011, Snowbird, USA. [pdf]

Hybridization Domain Construction using Curvature Estimation.
Thao Dang and Romain Testylier.
Hybrid Systems: Computation and Control HSCC 2011, LNCS, Springer, April 2011, Chicago, USA. [pdf]

Using redundant constraints for refinement.
E. Asarin, T. Dang, O. Maler, and R. Testylier.
ATVA'10 8th Int. Symposium on Automated Technology for Verification and Analysis, LNCS, Springer, Oct 2010. [pdf]

Accurate hybridization of nonlinear systems.
Thao Dang, Oded Maler, and Romain Testylier.
Hybrid Systems: Computation and Control HSCC'10, LNCS, Springer, Apr 2010. [pdf]

Computing reachable states for nonlinear biological models.
Thao Dang, Colas Le Guernic, and Oded Maler.
Computational Methods for Systems Biology CMSB, Bologna, Italy, Sept 2009. [pdf]

Image computation for polynomial dynamical systems using the bernstein expansion.
Thao Dang and David Salinas.
In A. Bouajjani and O. Maler, editors, Computer Aided Verification CAV'09, LNCS, pages 277-287. Springer, 2009.[pdf]

Sensitive State Space Exploration
T. Dang, A. Donze, O. Maler, N. Shalev
Proceedings of the IEEE International Conference on Control and Decision CDC, Cancun, Mexico, Dec 2008. [pdf]

IFIP Best Paper Award: Using disparity to enhance test generation for hybrid systems.
Thao Dang and Tarik Nahhal
TESTCOM/FATE 2008, 19th IFIP Int. Conf. on Testing of Communicating Systems and
7th Int. Workshop on Formal Approaches to Testing of Software, LNCS 5047, pp 54-69, Springer, Tokyo, June 2008. [pdf]

Symbolic Model Checking of Hybrid Systems using Template Polyhedra.
Sriram Sankaranarayanan, Thao Dang and Franjo Ivancic
TACAS'08 - Tools and Algorithms for the Construction and Analysis of Systems,
LNCS 4963, pp 188-202, Springer, Budapest, April 2008. [pdf]

A Policy Iteration Technique for Time Elapse over Template Polyhedra.
Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic,
Hybrid Systems: Control and Computation HSCC'08, LNCS 4981, pp 654-657, Springer, St Louis, April 2008. [pdf]

A Coverage-Guided Test Generation Tool for Hybrid Systems [pdf]
Tarik Nahhal and Thao Dang.
ARTIST WS: Tool Platforms for ES Modelling, Analysis and Validation, Berlin, 2007.

Guided Randomized Simulation
Tarik Nahhal and Thao Dang.
Hybrid Systems: Control and Computation HSCC'07, LNCS 4416, pp 731-735, Springer, Pisa, April 2007. [pdf]

Scheduling for multithreaded real-time programs via path planning
Thao Dang and Philippe Gerner.
ACM Int. Conference on Embedded Software EMSOFT 2006, pp 282-291, ACM, Seoul, South Korea, October 2006. [pdf]

Randomized simulation of hybrid systems for circuit validation.
Thao Dang and Tarik Nahhal.
Proceedings of FDL06 - Forum on specification and Design Languages, Darmstadt, Germany, Septembre 2006. [pdf]

Randomized Simulation of Hybrid Systems
Thao Dang and Tarik Nahhal
Technical Report, VERIMAG, May 2006. [pdf]

Recent progress in continuous and hybrid reachability analysis
E. Asarin, T. Dang, G. Frehse, A. Girard, C. Le Guernic and O. Maler.
CACSD 2006: Computer Aided Control Systems Design, October 2006.

Approximate reachability computation for polynomial systems.
Thao Dang.
Hybrid Systems: Control and Computation HSCC'06, LNCS 3927, pp 138-152, Springer, March 2006, Santa Barbara. [pdf]

Application of Reachability Analysis to Idle Speed Control Synthesis.
Thao Dang.
International Embedded and Hybrid Systems Conference, 2005, Singapore. [pdf]

Computing Schedules for Multithreaded Real-Time Programs Using Geometry.
Philippe Gerner and Thao Dang.
Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, LNCS 3252, pp 325-342, Springer, Grenoble, 2004. [pdf]
Long version as Technical report, TR-2004-8 [pdf]

Verification of Analog and Mixed-Signal Circuits using Hybrid Systems Techniques.
Thao Dang, Alexandre Donze, and Oded Maler.
Formal Methods for Computer Aided Design FMCAD'04, LNCS 3312, pp 21-36, Springer, Austin, USA, Nov 2004. [pdf] [slides]

Abstraction by projection and application to multi-affine systems.
Eugene Asarin and Thao Dang.
Hybrid Systems: Control and Computation HSCC'04, LNCS 2993, pp 32-47, Springer, Philadelphia, USA, March 2004. [ps.gz]

Counter-example Guided Predicate Abstraction of Hybrid Systems.
Rajeev Alur, Thao Dang, and Franjo Ivancic.
Tools and Algorithms for the Construction and Analysis of Systems TACAS'03, LNCS 2619, pp 208-223, Springer, Warsar, Poland, March 2003. [ps.gz]

Reachability Analysis of Nonlinear Systems Using Conservative Approximation.
Eugene Asarin, Thao Dang, and Antoine Girard.
Hybrid Systems: Control and Computation HSCC'03, LNCS, pp 20-35, Springer, Prague, April 2003. [pdf]

Progress on Reachability Analysis of Hybrid Systems using Predicate Abstraction.
Rajeev Alur, Thao Dang, and Franjo Ivancic.
Hybrid Systems: Control and Computation HSCC'03, LNCS 2623, pp 4-19, Springer, Prague, April 2003. [ps.gz]

The d/dt Tool for Verification of Hybrid Systems.
Eugene Asarin, Thao Dang, and Oded Maler.
Computer Aided Verification CAV'02, LNCS 2404, pp 365-370, Springer-Verlag, Copenhagen, Denmark, July 2002. [ps.gz]

Reachability Analysis Via Predicate Abstraction.
Rajeev Alur, Thao Dang, and Franjo Ivancic.
Hybrid Systems: Computation and Control HSCC'02, LNCS 2404, pp 35-48, Springer, March 2002, Stanford, California, USA. [pdf]

The d/dt Tool for Verification of Hybrid Systems
E. Asarin, T. Dang, and O. Maler.
Computer Aided Verification CAV 2002, LNCS, Springer. [ps.gz]

Hierarchical hybrid modeling of embedded systems.
R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. Pappas, and O. Sokolsky.
Embedded Software 2001, LNCS 2211, pp 14-31, Springer, Lake Tahoe City, USA, October 2001. [pdf]

Stability and reachability analysis of a hybrid model of luminescence in the marine bacterium Vibrio Fisheri.
C. Belta, J. Schug, T. Dang, V. Kumar, G. Pappas, H. Rubin, and P. Dunlap.
CDC'01 - Conference on Decision and Control, 2001, Florida, USA. [ps.gz]

d/dt: a Tool for Reachability Analysis of Continuous and Hybrid systems.
E. Asarin, T. Dang, and O. Maler.
Invited Session "Numerical Computation of Reachable Sets and Related Problems"
5th IFAC Symposium Nonlinear Control Systems NOLCOS, 2001, Saint-Petersburg, Russia. [ps.gz]

On Hybrid Control of Under-actuated Mechanical Systems.
E. Asarin, S. Bansal, T. Dang, B. Espiau, and O. Maler.
Hybrid Systems: Computation and Control HSCC'01, LNCS 2034, pp 77-88, Springer-Verlag, Rome, 2001. [ps.gz]

Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems.
E. Asarin, O. Bournez, T. Dang, and O. Maler.
Hybrid Systems: Computation and Control HSCC'00. LNCS 1790, pp 20-31, Springer-Verlag, Pittsburgh, USA, 2000. [ps.gz]

Test generation for analog and mixed-signal circuits using hybrid system models
Tarik Nahhal and Thao Dang, Research report VERIMAG, 2008.

Approximate Reachability Decomposition for Singularly Perturbed Linear Systems.
Thao Dang and George J. Pappas.
CIS, UPenn, Oct 2001.

Verification and Synthesis of Hybrid Systems. Thèse doctorale (Ph.D. thesis)
Thao Dang. Verimag, Institut National Polytechnique de Grenoble, 2000.
Abstract

Reachability Analysis of Hybrid Systems.
T. Dang and O. Maler. Reachability Analysis of Hybrid Systems.
In Proceedings of VICA, April 2000, Hanoi, Vietnam.

Modeling CheckSum fault coverage using Stochastic Petri nets.
Technical report (in French), Schneider Electric, Meylan Sept 1996.

Simulation of Stochastic Petri nets in the scope of Dependability Assessment and two techniques of speeding up rare event simulations.
DEA Technical report (in French), Schneider Electric, Meylan, Sept 1996