[libre-riscv-dev] Eliminate Any Make [was: Avoiding CMake]

Hendrik Boom hendrik at topoi.pooq.com
Thu Feb 20 18:11:37 GMT 2020


On Thu, Feb 20, 2020 at 02:17:28PM +0000, Scheming Pony wrote:
> > I'm curious about the formal verification. I gather you're talking
> > about real software that runs on hardware, not a hardware description.
> > What language and tools did you use to make this feasible? Or is that a
> > confidential trade secret?
> 
> We didn't do "formal verification" in the sense of axioms and proofs and stuff.  The formality we did was DO-178B (Catastrophic), and also an attempt at certication of an Ada compiler.
> 
> I avoid secrets, almost completely now.  It was part of an academic research project, on my no longer maintained CV, and an FAA regulated certication process.  If you read all this stuff, you know as much as I do, I guess...
> 
> References:
> 
> https://dl.acm.org/profile/81100171503 (Dr. "V-dot" Santhanam AKA "the boss".)
> https://dl.acm.org/doi/10.1145/1066404.589460 (Paywalled, sorry.)

thanks.  The abstraact is informative.
And I happen to have access to the ACM digital library.  But I'll 
have to try and remember or recover my password first ...

-- hendrik

> 
> Regards.
> 
> -- sjm
> 
> > -- hendrik
> 
> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev



More information about the libre-riscv-dev mailing list