Dominique Borrione

74 papers A* 1A 2B 2C 18Journal 13Unranked 34

Year	Rank	Type	Title / Venue / Authors
2019	J	`jnl`	Mining Missing Assumptions from Counter-Examples. ACM Trans. Embed. Comput. Syst. Guillaume Plassan, Katell Morin-Allory, Dominique Borrione
2017	C	`conf`	Extraction of missing formal assumptions in under-constrained designs. MEMOCODE Guillaume Plassan, Katell Morin-Allory, Dominique Borrione
2017	J	`jnl`	Synthesis of Regular Expressions Revisited: From PSL SEREs to Hardware. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Fatemeh Negin Javaheri, Katell Morin-Allory, Dominique Borrione
2016	C	`conf`	Conclusively verifying clock-domain crossings in very large hardware designs. VLSI-SoC Guillaume Plassan, Hans-Jörg Peter, Katell Morin-Allory, Fahim Rahim, Shaker Sarwary, Dominique Borrione
2016	—	`conf`	Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings. VLSI-SoC (Selected Papers) Guillaume Plassan, Hans-Jörg Peter, Katell Morin-Allory, Shaker Sarwary, Dominique Borrione
2015	J	`jnl`	Efficient and Correct by Construction Assertion-Based Synthesis. IEEE Trans. Very Large Scale Integr. Syst. Katell Morin-Allory, Fatemeh Negin Javaheri, Dominique Borrione
2015	C	`conf`	Enabler-based synchronizer model for clock domain crossing static verification. FDL Mejid Kebaili, Katell Morin-Allory, Jean-Christophe Brignone, Dominique Borrione
2014	C	`conf`	A tool for the automatic TLM-to-RTL conversion of embedded systems requirements for a seamless verification flow. VLSI-SoC Zeineb Bel Hadj Amor, Laurence Pierre, Dominique Borrione
2013	C	`conf`	Application of formal methods for design space exploration and refinement. FDL Dominique Borrione, Ashraf M. Salem
2013	C	`conf`	Fast prototyping from assertions: A pragmatic approach. MEMOCODE Katell Morin-Allory, Fatemeh Negin Javaheri, Dominique Borrione
2013	C	`conf`	SyntHorus-2: Automatic prototyping from PSL. VLSI-SoC Katell Morin-Allory, Fatemeh Negin Javaheri, Dominique Borrione
2010	J	`jnl`	Validating Assertion Language Rewrite Rules and Semantics With Automated Theorem Provers. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Katell Morin-Allory, Marc Boule, Dominique Borrione, Zeljko Zilic
2009	J	`jnl`	A Formal Approach to the Verification of Networks on Chip. EURASIP J. Embed. Syst. Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz
2009	C	`conf`	From Assertion-Based Verification to Assertion-Based Synthesis. VLSI-SoC Yann Oddos, Katell Morin-Allory, Dominique Borrione
2009	C	`conf`	High-level symbolic simulation for automatic model extraction. DDECS Florent Ouchet, Dominique Borrione, Katell Morin-Allory, Laurence Pierre
2009	—	`conf`	MYGEN: automata-based on-line test generator for assertion-based verification. ACM Great Lakes Symposium on VLSI Yann Oddos, Katell Morin-Allory, Dominique Borrione, Marc Boule, Zeljko Zilic
2008	J	`jnl`	A functional formalization of on chip communications. Formal Aspects Comput. Julien Schmaltz, Dominique Borrione
2008	C	`conf`	Assertion-Based Design with Horus. MEMOCODE Yann Oddos, Katell Morin-Allory, Dominique Borrione
2008	—	`conf`	Executable formal specification and validation of NoC communication infrastructures. SBCCI Dominique Borrione, Amr Helmy, Laurence Pierre, Julien Schmaltz
2008	—	`conf`	Proving and disproving assertion rewrite rules with automated theorem provers. HLDVT Katell Morin-Allory, Marc Boule, Dominique Borrione, Zeljko Zilic
2007	—	`conf`	A Generic Model for Formally Verifying NoC Communication Architectures: A Case Study. NOCS Dominique Borrione, Amr Helmy, Laurence V. Pierre, Julien Schmaltz
2007	C	`conf`	Asynchronous online-monitoring of logical and temporal assertions. FDL Katell Morin-Allory, Laurent Fesquet, Benjamin Roustan, Dominique Borrione
2007	C	`conf`	Prototyping Generators for On-line Test Vector Generation Based on PSL Properties. DDECS Yann Oddos, Katell Morin-Allory, Dominique Borrione
2007	J	`jnl`	Synthesis of Property Monitors for Online Fault Detection. J. Circuits Syst. Comput. Katell Morin-Allory, Eric Gascard, Dominique Borrione
2006	C	`conf`	Asynchronous Assertion Monitors for multi-Clock Domain System Verification. IEEE International Workshop on Rapid System Prototyping Katell Morin-Allory, Laurent Fesquet, Dominique Borrione
2006	—	`conf`	Formalizing On Chip Communications in a Functional Style. Trustworthy Software Julien Schmaltz, Dominique Borrione
2006	C	`conf`	On-Line Test Vector Generation from Temporal Constraints Written in PSL. VLSI-SoC Yann Oddos, Katell Morin-Allory, Dominique Borrione
2006	C	`conf`	On-line Monitoring of Properties Built on Regular Expressions. FDL Katell Morin-Allory, Dominique Borrione
2006	A	`conf`	Proven correct monitors from PSL specifications. DATE Katell Morin-Allory, Dominique Borrione
2006	—	`conf`	Towards a formal theory of on chip communications in the ACL2 logic. ACL2 Julien Schmaltz, Dominique Borrione
2005	—	`conf`	A Generic Network on Chip Model. TPHOLs Julien Schmaltz, Dominique Borrione
2005	—	`conf`	A proof of correctness for the construction of property monitors. HLDVT Katell Morin-Allory, Dominique Borrione
2005	—	`ed.`	Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings CHARME Dominique Borrione, Wolfgang J. Paul
2005	—	`conf`	Formal Verification of a SHA-1 Circuit Core Using ACL2. TPHOLs Diana Toma, Dominique Borrione
2005	—	`conf`	Verification of behavioral descriptions by combining symbolic simulation and automatic reasoning. ACM Great Lakes Symposium on VLSI Ghiath Al Sammane, Dominique Borrione, Remy Chevallier
2004	B	`conf`	A Functional Approach to the Formal Specification of Networks on Chip. FMCAD Julien Schmaltz, Dominique Borrione
2004	—	`conf`	Combining Several Paradigms for Circuit Validation and Verification. CASSIS Diana Toma, Dominique Borrione, Ghiath Al Sammane
2004	—	`conf`	TheoSim: combining symbolic simulation and theorem proving for hardware verification. SBCCI Ghiath Al Sammane, Julien Schmaltz, Diana Toma, Pierre Ostier, Dominique Borrione
2003	—	`conf`	An Approach to the Introduction of Formal Validation in an Asynchronous Circuit Design Flow. HICSS Dominique Borrione, Menouer Boubekeur, Emil Dumitrescu, Marc Renaudin, Jean-Baptiste Rigaud, Antoine Siriani
2003	—	`conf`	Constrained Symbolic Simulation with Mathematica and ACL2. CHARME Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione
2003	C	`conf`	Modeling CHP descriptions in Labeled Transitions Systems for an efficient formal validation of asynchronous circuit specifications. FDL Dominique Borrione, Menouer Boubekeur
2003	—	`conf`	Symbolic Simulation as a Simplifying Strategy for SoC Verification. IWSOC Emil Dumitrescu, Dominique Borrione
2003	—	`conf`	Validation of Asynchronous Circuit Specifications Using IF/CADP. VLSI-SoC (Selected Papers) Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Siriani
2003	C	`conf`	Validation of asynchronous circuit specifications using IF/CADP. VLSI-SOC Dominique Borrione, Menouer Boubekeur, Laurent Mounier, Marc Renaudin, Antoine Siriani
2002	A	`conf`	Formal Verification Techniques: Industrial Status and Perspectives. DATE Joel Blasquez, Marten van Hulst, Andrea Fedeli, Jean-Luc Lambert, Dominique Borrione, Coby Hanoch, Pierre Bricaud
2002	—	`conf`	Improving Static Ordering of BDDs for Reachability Analysis. IWLS Jorgiano Vidal, David Déharbe, Dominique Borrione
2001	—	`conf`	On the use of don't cares during symbolic reachability analysis. ISCAS (5) Sherief Reda, Ayman Wahba, Ashraf Salem, Dominique Borrione, M. Ghonaimy
2000	J	`jnl`	A compositional model for the functional verification of high-level synthesis results. IEEE Trans. Very Large Scale Integr. Syst. Dominique Borrione, Julia Dushina, Laurence V. Pierre
2000	—	`conf`	An ACL2 Model of VHDL for Symbolic Simulation and Formal Verification. SBCCI Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin
2000	J	`jnl`	Using the ACL2 Theorem Prover to Reason about VHDL Components. RITA Vanderlei Moraes Rodrigues, Dominique Borrione, Philippe Georgelin
1999	—	`conf`	Design Error Diagnosis in Digital Circuits without Error Model. VLSI Raimund Ubar, Dominique Borrione
1998	—	`conf`	Formalization of Finite State Machines with Data Path for the Verification of High-Level Synthesis. SBCCI Dominique Borrione, Julia Dushina, Laurence Pierre
1998	—	`conf`	Generation of Tests for the Localization of Single Gate Design Errors in Combinational Circuits using the Stuck-at Fault Model. SBCCI Raimund Ubar, Dominique Borrione
1997	—	`conf`	An approach to Verilog-VHDL interoperability for synchronous designs. CHARME Dominique Borrione, F. Vestman, H. Bouamama
1997	—	`conf`	Connection error location and correction in combinational circuits. ED&TC Ayman M. Wahba, Dominique Borrione
1996	J	`jnl`	A method for automatic design error location and correction in combinational logic circuits. J. Electron. Test. Ayman M. Wahba, Dominique Borrione
1996	—	`conf`	Automatic diagnosis may replace simulation for correcting simple design errors. EURO-DAC Ayman M. Wahba, Dominique Borrione
1996	B	`conf`	HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment. FMCAD Dominique Borrione, H. Bouamama, David Déharbe, C. Le Faou, Ayman M. Wahba
1995	J	`jnl`	Denotational Semantics of a Synchronous VHDL Subset. Formal Methods Syst. Des. Dominique Borrione, Ashraf M. Salem
1995	—	`conf`	Design error diagnosis in sequential circuits. CHARME Ayman M. Wahba, Dominique Borrione
1995	—	`conf`	Semantics of a verification-oriented subset of VHDL. CHARME David Déharbe, Dominique Borrione
1994	—	`conf`	A process algebra interpretation of a verification oriented overlanguage of VHDL. EURO-DAC Catherine Bayol, Bernard Soulas, Dominique Borrione, Fulvio Corno, Paolo Prinetto
1992	J	`jnl`	Formal Verification of VHDL Descriptions in the Prevail Environment. IEEE Des. Test Comput. Dominique Borrione, Laurence V. Pierre, Ashraf M. Salem
1992	J	`jnl`	Three Decades of HDLs: Part II, Conlan Through Verilog. IEEE Des. Test Comput. Dominique Borrione, Robert Piloty, Dwight D. Hill, Karl J. Lieberherr, Philip Moorby
1989	—	`conf`	Zero-Defect Designs, Why and How: Formal Verification vs. Automated Synthesis. IFIP Congress Dominique Borrione, Paolo Prinetto
1988	C	`conf`	A functional approach to formal hardware verification: the MTI experience. ICCD Dominique Borrione, Paolo Camurati, J. L. Paillet, Paolo Prinetto
1983	—	`book`	CONLAN Report Robert Piloty, Dominique Borrione, Mario Barbacci, Donald L. Dietmeyer, Fredrick J. Hill, Patrick Skelly
1982	A*	`conf`	The conlan project: Status and future plans. DAC Robert Piloty, Dominique Borrione
1981	—	`book`	Langages de description de systèmes logiques : propositions pour une méthode formelle de définition. Dominique Borrione
1980	—	`conf`	An Overview of CONLAN: A Formal Construction Method for Hardware Description Language. IFIP Congress Robert Piloty, Mario Barbacci, Dominique Borrione, Donald L. Dietmeyer, Fredrick J. Hill, Patrick Skelly
1980	—	`conf`	CONLAN: a formal construction method for hardware description languages: basic principles. AFIPS National Computer Conference Robert Piloty, Mario Barbacci, Dominique Borrione, Donald L. Dietmeyer, Fredrick J. Hill, Patrick Skelly
1980	—	`conf`	CONLAN: a formal construction method for hardware description languages: language application. AFIPS National Computer Conference Robert Piloty, Mario Barbacci, Dominique Borrione, Donald L. Dietmeyer, Fredrick J. Hill, Patrick Skelly
1980	—	`conf`	CONLAN: a formal construction method for hardware description languages: language derivation. AFIPS National Computer Conference Robert Piloty, Mario Barbacci, Dominique Borrione, Donald L. Dietmeyer, Fredrick J. Hill, Patrick Skelly
1976	—	`—`	LASCAR : un langage pour la simulation et l'évaluation des architectures d'ordinateurs. Dominique Borrione