`Travelled to:`

1 × Australia

1 × Austria

1 × Canada

1 × Denmark

1 × France

1 × Italy

1 × Poland

`Collaborated with:`

A.M.Moreira P.Fontaine S.Ranise R.Bonichon C.Tavares C.Ringeissen S.Merz B.W.Paleo T.Bouton D.C.B.d.Oliveira C.Hentz E.C.B.d.Matos J.B.S.Neto V.d.M.Jr.

`Talks about:`

smt (3) verifi (2) symbol (2) model (2) check (2) code (2) polymorph (1) trustabl (1) symmetri (1) fixpoint (1)

## Person: David Déharbe

### DBLP: D=eacute=harbe:David

### Contributed to:

### Wrote 7 papers:

- TAP-2015-MoreiraHDMNM #case study #code generation #testing #tool support #using #verification
- Verifying Code Generation Tools for the B-Method Using Tests: A Case Study (AMM, CH, DD, ECBdM, JBSN, VdMJ), pp. 76–91.
- SMT-2014-BonichonDT #morphism #polymorphism
- Extending SMT-LIB v2 with λ-Terms and Polymorphism (RB, DD, CT), pp. 53–62.
- CADE-2011-DeharbeFMP #problem #smt #symmetry
- Exploiting Symmetry in SMT Problems (DD, PF, SM, BWP), pp. 222–236.
- CADE-2009-BoutonODF #named #performance
- veriT: An Open, Trustable and Efficient SMT-Solver (TB, DCBdO, DD, PF), pp. 151–156.
- SEFM-2003-DeharbeR #debugging #proving #theorem proving #verification
- Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
- RTA-2002-DeharbeMR #logic #model checking
- Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae (DD, AMM, CR), pp. 207–221.
- FM-v1-1999-DeharbeM #fixpoint #model checking
- Symbolic Model Checking with Fewer Fixpoint Computations (DD, AMM), pp. 272–288.