David Déharbe

73 papers A 2B 6C 7Misc 2Journal 17Unranked 37

Year	Rank	Type	Title / Venue / Authors
2022	—	`conf`	Assigning Safe Executed Systems to Meanings. RSSRail Lilian Burdy, David Déharbe, Denis Sabatier
2022	—	`ed.`	Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022. SMT David Déharbe, Antti E. J. Hyvärinen
2020	J	`jnl`	Applying a Formal Method in Industry: a 25-Year Trajectory. CoRR Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin
2020	C	`conf`	Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B. ABZ Héctor Ruíz Barradas, Lilian Burdy, David Déharbe
2020	J	`jnl`	Low Cost High Integrity Platform. CoRR Thierry Lecomte, David Déharbe, Denis Sabatier, Étienne Prun, Patrick Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, Sylvain Conchon
2020	J	`jnl`	The CLEARSY Safety Platform: 5 Years of Research, Development and Deployment. CoRR Thierry Lecomte, David Déharbe, Paulin Fournier, Marcel Oliveira
2020	J	`jnl`	The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. Thierry Lecomte, David Déharbe, Paulin Fournier, Marcel Oliveira
2019	—	`conf`	B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. RSSRail Dalay Israel de Almeida Pereira, David Déharbe, Matthieu Perin, Philippe Bon
2019	—	`conf`	BTestBox: A Tool for Testing B Translators and Coverage of B Models. TAP@FM Diego de Azevedo Oliveira, Valério Medeiros Jr., David Déharbe, Martin A. Musicante
2019	B	`conf`	Property-Driven Software Analysis - (Extended Abstract). FM Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez
2019	J	`jnl`	The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
2018	C	`conf`	Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B. ABZ Lilian Burdy, David Déharbe
2017	—	`conf`	Applying a Formal Method in Industry: A 25-Year Trajectory. SBMF Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin
2017	—	`conf`	Safety Analysis of a CBTC System: A Rigorous Approach with Event-B. RSSRail Mathieu Comptier, David Déharbe, Julien Molinero Perez, Louis Mussat, Pierre Thibaut, Denis Sabatier
2016	—	`conf`	Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa". F-IDE@FM Lilian Burdy, David Déharbe, Étienne Prun
2015	—	`conf`	Software Component Design with the B Method - A Formalization in Isabelle/HOL. FACS David Déharbe, Stephan Merz
2015	—	`conf`	Verifying Code Generation Tools for the B-Method Using Tests: A Case Study. TAP@STAF Anamaria Martins Moreira, Cleverton Hentz, David Déharbe, Ernesto Cid Brasil de Matos, João Batista de Souza Neto, Valério de Medeiros Jr.
2014	—	`conf`	Extending SMT-LIB v2 with λ-Terms and Polymorphism. SMT Richard Bonichon, David Déharbe, Cláudia Tavares
2014	J	`jnl`	Integrating SMT solvers in Rodin. Sci. Comput. Program. David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
2014	—	`conf`	LLVM-Based Code Generation for B. SBMF Richard Bonichon, David Déharbe, Thierry Lecomte, Valério Medeiros Jr.
2014	J	`jnl`	The 2014 SMT Competition. J. Satisf. Boolean Model. Comput. David R. Cok, David Déharbe, Tjark Weber
2013	—	`conf`	BEval: A Plug-in to Extend Atelier B with Current Verification Technologies. LAFM Valério Medeiros Júnior, David Déharbe
2013	B	`conf`	Computing prime implicants. FMCAD David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
2013	J	`jnl`	Integration of SMT-solvers in B and Event-B development environments. Sci. Comput. Program. David Déharbe
2012	—	`conf`	An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF Haniel Barbosa, David Déharbe
2012	J	`jnl`	Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2012	C	`conf`	Formal Verification of PLC Programs Using the B Method. ABZ Haniel Barbosa, David Déharbe
2012	C	`conf`	SMT Solvers for Rodin. ABZ David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
2012	J	`jnl`	Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010. Theor. Comput. Sci. Ana Cavalcanti, David Déharbe
2011	—	`conf`	B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. SBMF Marcel Vinícius Medeiros Oliveira, David Déharbe, Luís C. D. S. Cruz
2011	A	`conf`	Exploiting Symmetry in SMT Problems. CADE David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
2011	—	`conf`	Quantifier Inference Rules for SMT proofs. PxTP David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
2010	—	`conf`	Applying the B Method for the Rigorous Development of Smart Card Applications. ASM Bruno Emerson Gurgel Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes
2010	—	`conf`	Automatic Verification for a Class of Proof Obligations with SMT-Solvers. ASM David Déharbe
2010	—	`conf`	GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine
2010	C	`ed.`	Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings ICTAC Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, Jim Woodcock
2009	—	`conf`	Formal Modelling of a Microcontroller Instruction Set in B. SBMF Valério Medeiros Júnior, David Déharbe
2009	—	`conf`	Formalizing FreeRTOS: First Steps. SBMF David Déharbe, Stephenson Galvão, Anamaria Martins Moreira
2009	J	`jnl`	Refining interfaces: the case of the B method CoRR David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
2009	J	`jnl`	Satisfiability solving for software verification. Int. J. Softw. Tools Technol. Transf. David Déharbe, Silvio Ranise
2009	A	`conf`	veriT: An Open, Trustable and Efficient SMT-Solver. CADE Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2008	J	`jnl`	A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework. J. Braz. Comput. Soc. David Déharbe, Silvio Ranise, Jorgiano Vidal
2008	C	`conf`	BSmart: A Tool for the Development of Java Card Applications with the B Method. ABZ David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
2008	—	`conf`	Combining Decision Procedures by (Model-)Equality Propagation. SBMF Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2008	—	`conf`	Verified Compilation and the B Method: A Proposal and a First Appraisal. SBMF Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Martins Moreira, Valério Medeiros Júnior
2006	J	`jnl`	AGraphs: Definition, implementation and tools. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. David Déharbe, Anamaria Martins Moreira, Demóstenes Sena
2006	—	`conf`	Aspect-oriented design in systemC: implementation and applications. SBCCI David Déharbe, Sérgio Medeiros
2006	B	`conf`	Automation of Java Card component development using the B method. ICECCS David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
2006	C	`conf`	Decision Procedures for the Formal Analysis of Software. ICTAC David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
2005	—	`conf`	Developing Java Card Applications with B. SBMF Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira, David Déharbe
2005	—	`conf`	Distributing the Workload in a Lazy Theorem-Prover. SBMF David Déharbe, Silvio Ranise, Jorgiano Vidal
2004	Misc	`conf`	Abstraction-Driven Verification of Array Programs. AISC David Déharbe, Abdessamad Imine, Silvio Ranise
2004	—	`conf`	Explicit-Symbolic Modelling for Formal Verification. SBMF Umberto Souza da Costa, Sérgio Vale Aguiar Campos, Newton Vieira, David Déharbe
2004	J	`jnl`	Manipulating algebraic specifications with term-based and graph-based representations. J. Log. Algebraic Methods Program. Anamaria Martins Moreira, Christophe Ringeissen, David Déharbe, Gleydson Lima
2004	J	`jnl`	Scalable Automated Proving and Debugging of Set-Based Specifications. J. Braz. Comput. Soc. Jean-François Couchot, David Déharbe, Alain Giorgetti, Silvio Ranise
2004	—	`conf`	Techniques for Temporal Logic Model Checking. PSSE David Déharbe
2003	—	`ch.`	A Tutorial Introduction to Symbolic Model Checking. Logic for Concurrency and Synchronisation David Déharbe
2003	—	`conf`	Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. FTP Silvio Ranise, David Déharbe
2003	B	`conf`	Light-Weight Theorem Proving for Debugging and Verifying Units of Code. SEFM David Déharbe, Silvio Ranise
2003	—	`conf`	Proving and Debugging Set-Based Specifications. WMF Jean-François Couchot, Frédéric Dadeau, David Déharbe, Alain Giorgetti, Silvio Ranise
2002	—	`conf`	FERUS: Um Ambiente de Desenvolvimento de Especificações CASL. SBES Gleydson Lima, Anamaria Martins Moreira, David Déharbe, David Ricardo Do Vale Pereira, Demóstenes Sena, Jorgiano Vidal
2002	—	`conf`	Improving Static Ordering of BDDs for Reachability Analysis. IWLS Jorgiano Vidal, David Déharbe, Dominique Borrione
2002	—	`conf`	Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. RTA David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen
2001	—	`conf`	BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs. SBES Sérgio Queiroz de Medeiros, David Déharbe
2001	—	`conf`	Optimizing BDD-Based Verification Analysing Variable Dependencies. SBCCI David Déharbe, Jorgiano Márcio Bruno Vidal
2000	J	`jnl`	Introdução a Métodos Formais: Especificação, Semântica e Verificação de Sistemas Concorrentes. RITA David Déharbe, Anamaria Martins Moreira, Leila Ribeiro, Vanderlei Moraes Rodrigues
2000	Misc	`conf`	Variable Ordering of BDDs with Parallel Genetic Algorithms. PDPTA Umberto Souza da Costa, David Déharbe, Anamaria Martins Moreira
1999	—	`conf`	Symbolic Model Checking with Fewer Fixpoint Computations. World Congress on Formal Methods David Déharbe, Anamaria Martins Moreira
1998	—	`conf`	Formal Verification of VHDL ¾ The Model Checker CV. SBCCI David Déharbe, Subash Shankar, Edmund M. Clarke
1998	B	`conf`	Model Checking VHDL with CV. FMCAD David Déharbe, Subash Shankar, Edmund M. Clarke
1997	—	`conf`	Using induction and BDDs to model check invariants. CHARME David Déharbe, Anamaria Martins Moreira
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	—	`conf`	Semantics of a verification-oriented subset of VHDL. CHARME David Déharbe, Dominique Borrione