[Eecs_phd] 4900 Software Verification

[Hunter, Tiffany]

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~



Dear EECS undergrads and grads:

Companies like Facebook, Twitter, and Jane Street are now using functional languages (Haskell, Scala, OCaml) to implement critical systems. The Internet ( https://medium.com/@jugoncalves/functional-programming-should-be-your-1-priority-for-2015-47dd4641d6b9 ) thinks you should learn a functional language too!

Why? Because functional programming languages can make it easier to reason about the programs you write, which often leads to simpler, more maintainable software -- and fewer bugs!

Taking my new 4900/5900 Software Verification course (class# 13964) is a great way to get a jump-start on functional programming (FP), especially if you haven't seen FP before. We'll be spending the first few weeks of the course learning FP in the incredibly expressive functional programming language Coq. Relevant logistical details:

  *   M/W lecture 3:05-4pm in Irvine 114
  *   F lab 3:05-4pm in Stocker 192
  *   Instructor: Gordon Stewart
  *   Website: http://oucsace.cs.ohiou.edu/~gstewart/courses/5900-16/
  *   Counts as a technical elective!
In later parts of the course, we'll use Coq to verify both simple functional programs and imperative programs, learning the relevant verification techniques along the way. When I say "verify," I mean we'll be using features of the Coq system to prove that our programs are correct -- i.e., they have no bugs.

These sorts of verification techniques are useful in high-assurance domains like avionics and cars. Already, companies like Rockwell Collins, Galois (Portland, OR), and FireEye are using related methods to build real software systems -- and industry demand for people who know software verification tools like Coq is only growing.

So consider taking the course -- and I look forward to seeing many of you in the fall!

Sincerely,

Gordon Stewart
Asst. Professor, EECS
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://listserv.ohio.edu/pipermail/eecs_phd/attachments/20160321/6f30bc83/attachment.html