David Déharbe
Personal
Software
Students
Publications
Lectures
Talks
Services
Links
|
(formal methods)
Software
I have been involved in the design, development and maintenance of several software-based products at CLEARSY.
Actively maintained
The SMT-solver
veriT
. I am no longer part of the development team.
Dormant
b2llvm:
a LLVM code generator for B.
Discontinued
b2llvm:
a LLVM code generator for B.
The
haRVey
theorem prover.
CV:
a model checker for VHDL.
Software developed by students under my supervision
Aspect-oriented design in SystemC.
BDDmeter:
dynamic visualization of BDDs.
BEval:
Atelier-B plug-in to discharge proof obligations
BSmart:
B-method based rigorous design of JavaCard components.
AGraphs:
Typed-graph data structure for representation of software artifacts.
