[Eecs_bscs] CS 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. 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 4900/5900 Software Verification course (soon to be renumbered 4201/5201) 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 ARC 159
  *   F lab 3:05-4pm in Stocker 192
  *   Instructor: Gordon Stewart
  *   Last Year's Website, which is representative of the material we'll cover: http://ace.cs.ohio.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 use 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; opening a new office in Dayton), 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_bscs/attachments/20170411/c1306a80/attachment.html>