[Cad] Formally Verifying a B-Rep kernel

[Andrew Zukoski]

David,

Interesting idea! I can think of two challenges; one is the sheer scale of
most kernel codebases (eg, the ACIS binaries are around 100 mb). The other
is that writing the specification for a kernel would itself be a
significant task and at least at first glance would have to make heavy use
of rich, dependent types. The state of a geometric program that has 'gone
wrong' seems much harder to encode than a null pointer dereference.

I wonder if there is a way to scope down the surface area that would need
to be formally verified to still have a significant impact on the
development of a rich kernel. At least a few folks are investigating this:
http://www.researchgate.net/publication/221610369_A_Formally_Verified_Geometric_Modelling_Core
, but I'm not aware of any broad uptake or reusable components that have
been verified.

Andrew


On Sun, Nov 8, 2015 at 5:13 PM, David Kaufman <davidgilkaufman at gmail.com>
wrote:

> My understanding from our discussion last week is that writing a B-Rep
> kernel is difficult primarily because there are tons of edge cases for
> how objects can intersect each other and it's really hard to get them
> all correct/test for all of them. If this is the main challenge then my
> intuition is that it would be best solved by building a formally
> verified b-rep kernel (and that perhaps it would take much less time to
> write that way). Do any of you know if anyone has tried to write a
> formally verified b-rep kernel or why not?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/cad-rg/attachments/20151108/e5c3450b/attachment.html