points by westurner 7 years ago

Which universities teach formal methods?

- q=formal+verification https://www.class-central.com/search?q=formal+verification

- q=formal-methods https://www.class-central.com/search?q=formal+methods

Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?

Is there a certification for formal methods? Something like for engineer-status in other industries?

What are some examples of tools and [OER] resources for teaching and learning formal methods?

- JsCoq

- Jupyter kernel for Coq + nbgrader

- "Inconsistencies, rolling back edits, and keeping track of the document's global state" https://github.com/jupyter/jupyter/issues/333 (jsCoq + hott [+ IJavascript Jupyter kernel], STLC: Simply-Typed Lambda Calculus)

- TDD tests that run FV tools on the spec and the implementation

What are some examples of open source tools for formal verification (that can be integrated with CI to verify the spec AND the implementation)?

What are some examples of formally-proven open source projects?

- "Quark : A Web Browser with a Formally Verified Kernel" (2012) (Coq, Haskell) http://goto.ucsd.edu/quark/

What are some examples of projects using narrow and strong AI to generate perfectly verified software from bad specs that make the customers and stakeholders happy?

From reading though comments here, people don't use formal methods because: cost-prohibitive, inflexibile, perceived as incompatible with agile / iterative methods that are more likely to keep customers who don't know what formal methods are happy, lack of industry-appropriate regulation, and cognitive burden of often-incompatible shorthand notations.