Thao Dang

HSCC2019 Test-of-Time Award Reachability Analysis via Face Lifting.
T. Dang and O. Maler.
In T.A. Henzinger and S. Sastry, editors,
Hybrid Systems: Computation and Control HSCC'98. LNCS 1386, pp 96-109, Springer-Verlag, Berkeley, USA, 1998. [ps]

ARITH 2017 Best Paper Award Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
Alexandre Rocca, Victor Magron, and Thao Dang.
ARITH24 (24th IEEE Symposium on Computer Arithmetic) 2017.

IFIP TESTCOM/FATE 2008 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]

Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representation.
Victor Magron, Alexandre Rocca, Thao Dang.
IEEE Transactions on Computers, 2019.

Reachability computation for polynomial dynamical systems.
Tommaso Dreossi, Thao Dang, and Carla Piazza.
Formal Methods in System Design, 50(1): 1-38 (2018).

Stability verification and timing contract synthesis for linear impulsive systems using reachability analysis.
Mohammad Al Khatib, Antoine Girard, and Thao Dang.
Nonlinear Analysis: Hybrid Systems, 50(1): 211-226 (2017), Elsevier.

Reachability analysis for polynomial dynamical systems using the Bernstein expansion.
T. Dang and R. Testylier.
Reliable Computing Journal, Special issue: Bernstein Polynomials in Reliable Computing, ISSN 1573-1340, 2012 pdf.

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, 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, 354(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]

Effective Synthesis of Switching Controllers for Linear Systems.
E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli.
Proceedings of the IEEE, 88, Special Issue Hybrid System: Theory & Applications, 1011-1025, 2000. [pdf]

Hybrid Systems Biology - Second International Workshop, HSB 2013, Taormina, Italy, September 2, 2013 and Third International Workshop, HSB 2014, Vienna, Austria, July 23-24, 2014, Revised Selected Papers.
Oded Maler, Adam M. Halasz, Thao Dang, Carla Piazza (editors), Lecture Notes in Computer Science 7699, Springer 2015.

Proceedings of the International Conference Hybrid Systems: Computation and Control HSCC 2012
Thao Dang and Ian Mitchell (editors), [Proceedings], Beijing, April 2012.

Proceedings of the Second International Workshop Hybrid Systems and Biology 2013
Thao Dang and Carla Piazza (editors), [Proceedings], EPTCS 125, Taormina, Italy, Sept 2013.

Proceedings of the first workshop on Verification of Analog Circuits FAC'05.
T. Dang, B. Krogh, O. Maler, and R. Ruttenbar.
Electronic notes in Theoretical Computer Science, Elsevier, 2005.

Thao Dang, Tommaso Dreossi, Eric Fanchon, Carla Piazza and Alexandre Rocca.
Set-Based Analysis for Biological Modelling.
Automated Reasoning for Systems Biology and Medicine, Springer. 2019.

Timing Contracts for Multi-core Embedded Control Systems.
Mohammad Al Khatib, Antoine Girard, and Thao Dang.
Chapter in Control subject to Computational and Communication Constraints: current challenges, LNCIS 475, Springer, 2018.

Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems.
Arvind S. Adimoolam and Thao Dang.
Chapter in Control subject to Computational and Communication Constraints: current challenges, LNCIS 475, Springer, 2018.

Set-Based Analysis for Biological Modelling.
Thao Dang, Tommaso Dreossi, Eric Fanchon, Carla Piazza and Alexandre Rocca.
Automated Reasoning for Systems Biology and Medicine, Springer. 2019.

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.
Model-based Design of Embedded 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]

A geometric approach to scheduling of concurrent real-time processes sharing resources.
T. Dang and Ph. Gerner.
In Vedran Kordic, editors. Multiprocessor Scheduling, Theory and Applications. ARS Press, Vienna, Austria/Pro Literatur Verlag, Mammendorf, Germany, 2007.

Generation of Signals Under Temporal Constraints for CPS Testing.
Benoit Barbot, Nicolas Basset, Thao Dang.
Nasa Formal Methods NFM 2019, LNCS Springer.

Reachability Analysis and Hybrid Systems Biology - In Memoriam Oded Maler.
Thao Dang.
Hybrid Systems Biology 2019, LNCS/LNBI, Springer, 2019.

Occupation measure methods for modelling and analysis of biological hybrid systems
Alexandre Rocca, Marcelo Forets, Victor Magron, Eric Fanchon, and Thao Dang.
IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2018), Oxford, United Kingdom.

Stimulus Generator for Circuit Model Generation
Xavier Avon, Thao Dang.
Workshop MTCPS 2018, 20-21, Porto, 2018.

Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems
Arvind S. Adimoolam and Thao Dang.
FORMATS 2017, LNCS, pages 97-115, Springer, 2017.

Temporal Specification Testing of Hybrid Systems
Thao Dang and Tommaso Dreossi.
CASE 2017 13th Conference on Automation Science and Engineering, IEEE, 2017.

[BEST PAPER AWARD] Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
Alexandre Rocca, Victor Magron, and Thao Dang.
ARITH24 (24th IEEE Symposium on Computer Arithmetic) 2017.

Classification and Coverage-Based Falsification for Embedded Control Systems.
Arvind S. Adimoolam, Thao Dang, Alexandre Donze, James Kapinski, Xiaoqing Jin.
CAV 2017, pages 483-503, Springer, 2017.

Self-triggered control for sampled-data systems using reachability analysis.
Mohammad Al Khatib, Antoine Girard, and Thao Dang.
IFAC World Congress, Toulouse, France, 2017.

Template complex zonotopes for stability and invariant verifica- tion.
Arvind S. Adimoolam and Thao Dang.
ACC 2017, Seattle, USA, 2017.

Scheduling of Embedded Controllers Under Timing Contracts.
Mohammad Al Khatib, Antoine Girard, and Thao Dang.
HSCC 2017, ACM, pages 131-140, 2017.

Using Complex Zonotopes for Stability Verification.
Arvind S. Adimoolam and Thao Dang.
Proceedings of ACC, 2016, Boston, USA.

Verification and Synthesis of Timing Contracts for Embedded Controllers.
Mohammad Al Khatib, Antoine Girard, and Thao Dang.
Proceedings of HSCC 2016, ACM, pages 115-124, 2016.

Template Complex Zonotopes: A New Set Representation for Verication of Hy- brid Systems.
Thao Dang.
International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2016).

Parallelotope Bundles for Polynomial Reachability
Tommaso Dreossi, Thao Dang, and Carla Piazza.
International Conference on Hybrid Systems: Computation and Control HSCC 2016, LNCS, Springer, April 2016.

Verification and synthesis of timing contracts for embedded controllers
Mohammad Al Khatib, Antoine Girard and Thao Dang.
Proc. 5th IFAC Conference on Analysis and Design of Hybrid Systems, 2016.

Stability Verification of Nearly Periodic Impulsive Linear Systems Using Reachability Analysis
Mohammad Al Khatib, Antoine Girard and Thao Dang.
Proc. ADHS 2015, Atlanta, 2015.

Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems
Tommaso Dreossi, Thao Dang, Alexandre Donze, James Kapinski, Jyo Deshmukh, and Xiaoquin Jin.
NASA Formal Methods NFM 2015, LNCS, Springer, 2015.

Test Coverage Estimation Using Threshold Accepting
Thao Dang and Noa Shalev.
ATVA 2014, Int. Symposium on Automated Technology for Verification and Analysis, LNCS, Springer, 2014.

Parameter Synthesis for Polynomial Biological Models.
Tommasi Dreossi and Thao Dang
17th International Conference on Hybrid Systems: Computation and Control HSCC 2014, pp 233 - 242, ACM, 2014.

Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models.
Tommaso Dreossi, Thao Dang and Carla Piazza
International Workshop Hybrid Systems and Biology HSB 2014, Springer LNBI 2015.

Exploiting the Eigenstructures of Linear Systems to Speed up Reachability Computation.
Alexandre Rocca, Thao Dang and Eric Fanchon
International Workshop Hybrid Systems and Biology HSB 2014, Springer LNBI 2015.

NLTOOLBOX: A Library for Reachability Computation of Non-Linear Dynamical Systems
Romain Testylier and Thao Dang.
ATVA 2013, LNCS, Springer-Verlag, 2013. [pdf]

Falsifying Oscillation Properties of Parametric Biological Models
Tommaso Dreossi and Thao Dang.
Hybrid Systems and Biology (HSB 2013), EPTCS 125, Springer, Sept 2013.[pdf]

Verification of embedded control programs
Thao Dang, Bertrand Jeannet and Romain Testylier.
Proceedings of European Conrol Conference ECC 2013[pdf]

State estimation and property-guided exploration for hybrid systems testing.
Thao Dang and Noa Shalev.
24th IFIP Int. Conference on Testing Software and Systems, LNCS, Springer-Verlag, 2012. [paper], [slides]

Reachability Analysis of Polynomial Systems using Linear Programming Relaxations.
Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang and Antoine Girard.
ATVA 2012, LNCS, Springer-Verlag, 2012, (to appear). [pdf]

Analysis of Parametric Biological Models.
Romain Testylier and Thao Dang.
Workshop on Hybrid Systems and Biology HSB 2012, EPTCS, New Castle, 2012. [pdf]

Reachability analysis using the Bernstein expansion over polyhedra..
Romain Testylier and Thao Dang.
Fifth International Workshop on Numerical Software Verification NSV, June 2012. [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, St Louis, April 2008. [pdf]

Test Coverage for Continuous and Hybrid Systems
Tarik Nahhal and Thao Dang.
Computer Aided Verification CAV 2007, LNCS 4590, pp 449-462, Springer, Berlin, Germany, July 2007. [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]