Publications de Emmanuelle Encrenaz-Tiphène
Habilitation à diriger des recherches.
2007 : E. Encrenaz-Tiphène, Contributions pour la conception et la vérification de systèmes matériels embarqués, Université Paris VI, juin 2007, 96 pages
Journaux internationaux
2011 :S. Baarir, C. Braunstein, E. Encrenaz, JM. Ilié, ,I. Mounier, D. Poitrenaud, S. Younes, Feasibility Analysis for MEU Robustness Quantification by Symbolic Model-Checking, Formal Methods in System Design, 2011, Springer (fmsd_11.pdf).
2010 :V.Beaudenon, E. Encrenaz, S.Taktak, Data Decision Diagrams for Promela Systems Analysis, Software Tools and Technology Transfert International Journal, vol 12(5), pp 337-352, 2010, Springer (lien vers la publication électronique).
2009 :E. André, T. Chatain, E. Encrenaz, L. Fribourg, An inverse method for parametric timed automata, International Journal of foundations of Computer Sciences, vol 20, no 5, pages 819-836, World Scientific Publishing Company. ijfcs2009.pdf
2009 :R. Chevallier, E. Encrenaz, L. Fribourg, W. XuTimed Verification of a generic architecture of a memory circuit using parametric timed automata, Formal Methods in System Design International Journal, vol 34, no 1, pages 59-81, Springer. fmsd_08.ps
2008 :S. Taktak, E. Encrenaz, J.-L. Desbarbieux, A tool for automatic detection of deadlocks in wormhole networks on chip, ACM Transactions on Design Automation of Electronic Systems, vol 1, no 2, 01-2008, 22 pages. todaes_08.ps
2007 : C. Braunstein, E. Encrenaz, CTL-property transformations along an incremental design process, Software Tools and Technology Transfer International Journal, vol 9(1), fev 2007, pp 77-88. Springer. sttt06.pdf link to the electronic springer publication
2006 : R. Chevallier, E. Encrenaz-Tiphene, L. Fribourg, W. Xu, Timing Analysis of an Embedded Memory: SPSMALL, WSEAS Transactions on Circuits and Systems, vol 5(7), pp 973-978, 2006,wseas06.pdf
Journaux nationaux et francophones
2011 : H. Mokrani, R. Ameur-Boulifa, E. Encrenaz, S. Coudert, Approche pour l'intégration du raffinement formel dans le processus de conception des SOCs, Journal Européen des Systèmes Automatisés, Special Issue MSR'11, vol. 45(1-3), pp 221-236.
Conférences et workshop internationaux avec comité de lecture et actes
2012 : S.-H. Alwi, C. Braunstein, E. Encrenaz An efficient Refinement StrategyExploiting Components' Properties in a CEGAR Process, Int. Forum on Design Languages (FDL'12), pp. to appear, ECSI Press. Sept. 2012
2010 : A. Bara, P. Bazargan-Sabet, R. Chevallier, E. Encrenaz, D. LeDu, P. Renault, Formal Verification of Timed VHDL Programs, Int. Forum on Design Languages (FDL'10), pp. 80-85, ECSI Press. Sept. 2010, fdl_10.pdf
2010 : S. Taktak, E. Encrenaz, J.-L. Desbarbieux, A polynomial algorithm to prove deadlock-freeness of wormhole networks, 18th Int. Euromicro Conf. on Parallel, Distributed and Network-based Computing (PDP'10), pp. 121-128, IEEE Computer Society. feb. 2010.
2009 : S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.-M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud, Complementary Formal Approaches for Dependability Analysis, IEEE 24th Int. Symp. Defect and Fault Tolerance in VLSI Systems (DFT 2009), pp. 331-339. IEEE Computer Society. oct. 2010.
2008 : E. André, T. Chatain, E. Encrenaz, L. Fribourg, An Inverse Method for Parametric Timed Automata, 2nd International Workshop on Reachability Problems (RP'08), sept. 2008, U.K., Electronic Notes in Theoretical Computer Science (ENTCS) , 223, pages 29-46, Elsevier Sciences Publishers 2008, rp08.pdf
2008 : E. Encrenaz, L. Fribourg, Time Separation of Events: an Inverse Method, 9th LIX Colloqium on Emerging Trends on Concurrency Theory (LIX'06), nov. 2006, France, Electronic Notes in Theoretical Computer Science (ENTCS) 209, pp. 135-148, Elsevier Science Publisher, 2008 lix06.pdf
2007 : E. Encrenaz, A. Finkel, Automatic verification of counter systems with ranking functions, 9th International Workshop on Verification of Infinite-state Systems (INFINITY'2007), satellite workshop of CONCUR'2007, pp. 12-23, sept. 2007, Portugal, Electronic Notes in Theoretical Computer Science (ENTCS) 239, pages 85-103, Elsevier Publishers, 2008. infinity07.ps, version longue
2007 : C.Braunstein, E. Encrenaz, Using CTL Formulae as Component Abstraction in a Design and Verification Flow, 6th International Conference on Application of Concurrency to Systems Design (ACSD'2007), pp. 80-89, IEEE Computer Society Press, jul 2007, Slovak Republik, acsd07.pdf
2006 : S. Taktak, E. Encrenaz, J.-L. Desbarbieux, A Tool for Automatic Detection of Deadlock in Whormhole Networks on Chip, 11th IEEE international workshop on High-Level Design Verification and Test (HLDVT'2006), nov 2006, California, hldvt06.pdf
2006 : R. Chevallier, E. Encrenaz, L. Fribourg, W. Xu, Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata, 4th international conference on Formal Modelling and Analysis of Timed Systems (FORMATS'2006), sept 2006, France. formats06.pdf
2006 : C. Braunstein, E. Encrenaz, Formalizing the incremental design and verification process of a pipelined protocol converter, IEEE 17th international workshop on Rapid System Prototyping (RSP'2006) june 2006, Crete. rsp06.pdf
2004 : C. Braunstein, E. Encrenaz, CTL-property transformations along an incremental design process, 4th international workshop on Automated Verification of Critical Systems (AVoCS 2004), sept 2004, United Kingdom. Appeared in Electronic Notes on Theoretical Computer Sciences, volume 128, Issue 6, pp 263-278.avocs2004.pdf
2004 : H. Charlery, A. Greiner, E. Encrenaz, L. Mortiez, A. Andriahantenaina, Using VCI in an on-chip system around SPIN network, IEEE 11th international conference on mixed design of integrated circuits and systems (MIXDES 2004), jun 2004, Poland.mixdes2004.pdf
2003 : C. Roux, E. Encrenaz, CTL may be ambigous when model-checking Moore Machines, (short paper) IFIP WG 10.5 12th international advanced research working conference on correct harware design and verification methods (CHARME 2003), nov 2003, Italy. Lecture Notes in Computer Science vol 2860. charme2003.ps | long version
2003 : V. Beaudenon, E. Encrenaz, J.-L. Desbarbieux, Design validation of ZCSP with SPIN, IEEE 3rd international conference on application of concurrency to system design (ACSD 2003), jun 2003, Portugal.acsd2003.ps
2002 : J.-M. Couvreur, E.Encrenaz, E. Paviot-Adet, D. Poitrenaud, P. Wacrenier, Data Decision Diagram for Petri Nets Analysis, 23rd international conference on application and theory of Petri Nets (ATPN 2002), jun 2002, Australia. Lecture Notes in Computer Science vol 2360. atpn2002.pdf
1998 : F. Rahim, E. Encrenaz, M. Minoux, R.K. Bawa, Modular Model-checking of VLSI designs described in VHDL, IEEE international conference on computers and theirs applications, mar 1998, Hawai, USA.
1996 : R.K. Bawa, E. Encrenaz, A plat-form for the formal verification of VHDL programs, 4th international workshop on symbolic methods and application in circuit design (SMACD 96), oct 1996, Belgium.
1996 : R.K. Bawa, E. Encrenaz, A tool for the transaltion of VHDL descriptions into a formal model and its application to formal verification and synthesis, 4th international symposium on formal methods in real-time and fault-tolerant systems, sept 1996, Sweden.
1996 : R.K. Bawa, E. Encrenaz, VMC : a tool for model-checking VHDL descriptions, IFIP 10.5 VHDL user-forum in Europe SIG-VHDL spring’96 working conference, may 1996, Germany.
1996 : R.K. Bawa, E. Encrenaz, Formal Verification of VHDL descriptions by symbolic state-space exploration applied to finite-state machines, VHDL international user forum spring 96, mar 96, California, USA.
1995 : A. Evans, E. Encrenaz, R.K. Bawa, L. Jacomme, An approach to the synthesis of VHDL concurrent processes as a FSM, IFIP WG 10.5 workshop on logic and architectural synthesis, dec 1995, France.
1995 : E. Encrenaz, A symbolic transition relation for a subset of VHDL’87 descriptions and its application to symbolic model-checking, IFIP WG 10.5 international advanced research working conference on correct hardware design and verification methods (CHARME 95), nov 1995, Germany. Lecture Notes in Computer Science vol 987.
1993 : E. Encrenaz, J.-M. Couvreur, R.K. Bawa, Validation of VHDL systems based on Petri Nets Modelling, IFIP WG 10.2 workshop on design methodologies for microelectronics and signal processing, oct 1993, Poland.
Autres Conférences
2010 : S. Baarir, C. Braunstein, E. Encrenaz, J.-M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes, Quantifying Robustness by Symbolic Model checking, Int. workshop on Hardware Verification (HWVW'10), satellite event of CAV'10. Jul. 2010.
2006 : R. Chevallier, E. Encrenaz, L. Fribourg, W. Xu, Timing Analysis of an Embedded Memory: SPSMALL, WSEAS 10th international conference on circuits (part of the 10th International Multiconference on Circuits, Systems, Communication and Computers (CSCC'2006)), july 2006, Greece. Also published in WSEAS Transations on Circuits and Systems journal.wseas06.pdf
2004 : V. Beaudenon, E. Encrenaz, Utilisation des diagrammes de décision de données pour la vérification fonctionnelle de systèmes matériels,2 e Manifestation CNRS des jeunes chercheurs du département STIC (MAJECSTIC 2004), oct 2004, France. majecstic2004.pdf
2003 : H. Charlery, E. Encrenaz, A. Greiner, A. Andriahantenaina, L. Mortiez, SPIN : un micro-réseau à commutation de paquets respectant la norme VCI ; concepts généraux et validation, Symposium en Architecture et Adéquation Architecture-Algorithmes (SympAAA 2003), jun 2003, France.
Rapport de contrat
2001 : E. Encrenaz, D. Poitrenaud, E. Paviot-Adet, Vérification de programmes VHDL à l’aide des DDD, rapport final du marché 99-34-024 contracté entre la DGA et le LIP6.clovis_final_lip6_2001.pdf
Rapports de recherche
2009 : E. andré, E. Encrenaz, L. Fribourg Synthesizing Parametric Constraints on Various Case Studies using IMITATOR, LSV research report LSV-09-13, 18 pages, 06/09.rr-lsv-2009-13.pdf
2008 : S. Amari, E. andré, T. Chatain, O. de Smet, B. Denis, E. Encrenaz, L. Fribourg, S. Ruel, Timed Analysis of Distributed Control Systems Combining Simulation and Parametric Model-checking , LSV research report LSV-09-14, 49 pages, 06/09. rr-lsv-2009-14.pdf
2006 : R. Chevallier, E. Encrenaz, L. Fribourg, W. Xu, Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata, LSV research report number 2006-14, 07/06.rr-lsv-2006-14.pdf
2005 : C. Braunstein, E. Encrenaz, Incremental Specification and Design of a Pipelined Protocol Converter , LIP6 research report, 06/05.RR_LIP6_braunstein_encrenaz_06_05.pdf
2005 : V.Beaudenon, E. Encrenaz, Data Decision Diagrams for Promela systems Analysis, LIP6 research report, 06/05.RR_LIP6_beaudenon_encrenaz_06_05.pdf
Thèse de doctorat
1995 : E. Encrenaz, Une méthode de vérification de propriétés de programmes VHDL basée sur des réseaux de Petri , Thèse de doctorat de l'Université Paris VI, spécialité Informatique, décembre 1995.these_encrenaz.tgz