How can I make a career in Formal Methods programming in USA?

Question

I've found that my (USA) professors recoil with a near-disgust when I ask them about how to pursue a career in Formal Methods programming.

They say, "Oh, that stuff! That stuff is anal. You don't need that European POS to get a job."

I'm sure I'll get a job without it, but Formal Methods interests me so much that I bet I'd like to make a career of it. I'd like to learn about Formal Methods at an American University and then work in that field here.

I've found that even professors at more important universities than mine don't seem to welcome Formal Methods. Almost all FM research project webpages are semi-abandoned and moldering. Europe is where the action seems to be for this.

Can anyone suggest a plan of attack, and along the way explain the antipathy to Formal Methods in the US?

I'm a sophomore at a public university in the South.

Answer 1

Andy,

(for all FYI:) from Wikipedia: http://en.wikipedia.org/wiki/Formal_methods

My sense is that a graduate degree would be useful in this field and that your employment opportunities would be limited to government, science and academia. NSA, NASA, some R&D etc.

The Formal Methods idea is probably too "ivory tower" to be useful in the general business environment. Those of us that work in the general fieldw probably tend to throw away any kind of "best practices" advice or methodology whenever a deadline is threatened. IMHO.

Answer 2

The folks I have heard of using formal methods were all on Ada jobs, and I believe they were all working on extreme stafety-cirtical jobs for the government (eg: Manned space flight).

So if you are interested in this, I'd highly suggest picking up Ada (so you can get it on your resume'), and applying to NASA and anyone you can find contracting with them.

I'd also suggest you apply to the vendors who support this market. For example, Praxis sells a special subset of Ada (called SPARK) that can be more easily formally analyzed.

---

If you are worried about fitting into a corporate environment, and you know exactly what you want to work on, I'd strongly consider staying in acedemia. There are universities specializing in research into formal methods, and they'd probably love to have graduate students (and one day perhaps more professors) with a passion for it. Once you get a PhD. and a professorship, you can work on whatever you want, as long as you can find someone out there willing to fund it.

Answer 3

One popular (lightweight) formal method from the US is Alloy, developed at MIT, so there is some action in America at important universities. Carnegie Mellon has a "Master of Software Engineering" that includes at least one FM course ("Models of Software Systems").

I suppose the antipathy in the US is the same as over here in Europe: they were oversold and many people still think of FMs as writing 300 pages of math before writing the first line of code. The best attack is using them and showing that they can be useful if used appropriately and realistically. I'd highly recommend Daniel Jackson's book on Alloy (even though it's not particularly strong on maths, "Using Z" was much more thorough in that regard).

Foreword & introduction from Jackson's book (online as sample chapters) and his article "Dependable Software by Design" give some good ideas on how to sell this stuff.

I'm using Alloy along with Z and CSP at work (although only for myself, I'm the only weird one who does this, although a few people got interested once they saw what I did with them). It saved me from some broken designs, so yes it works even beyond safety-critical systems if you learn to use it well and get a feeling for the level of abstraction that's best for your use case.

You'll have a hard time finding a job involving formal methods. Depends on how serious you are about it. If you're very serious, try companies specialising on safety-critical systems. However, the only job listings for writing formal specs I've ever seen were all masters thesis.

Or: get a regular job, apply some lightweight FM to your work and show off when you've got some interesting results (the analyzing and visualizing capabilities of Alloy really help here). I believe I'm having much more fun this way than if I'd be working in the safety-critical systems industry with ADA/SPARK.

If you'd rather like to stay in academia, have a look at dependently-typed programming languages or theorem provers. Basically, in a dependently-typed language you put the specification in the types that you would write down separately with "less hard" formal methods. So the compiler can verify that your program complies to the specification. There's a (very) lightweight form of programming with properties in types that you may be interested in if you like this stuff (look up "phantom types" or "index types").

Dependent types/theorem provers should be more popular in the US academia than the Z or CSP stuff I think. I've seen materials from a course on Coq (a theorem prover) at Harvard that are really good. And Tim Sheard at Portland has created Omega, which is kind of a strict Haskell dialect that is kind of in between functional programming and a full-blown dependently-typed language. Look at his two papers "Languages of the Future" and "Putting Curry-Howard to Work". I had the pleasure of attending his lecture and tutorials on Omega at a summer school here in Europe. He's great!

Answer 4

All good advanced programs in programming languages are starting to take formal methods very serious indeed. I taught at Harvard and Greg Morrisett is doing some interesting stuff there, but at the moment I think the very best places are Penn and CMU.

I also have a very high regard for Daniel Jackson's work on specification and model checking, including Alloy. Gerard Holzmann's work on SPIN and model checking is also superb. But if you are really interested in traditional formal methods (Hoare and Dijkstra and that lot) you may not be as satisfied with model checking as with what the languages people are calling "Mechanized Metatheory". Check out Stephanie Weirich or Benjamin Pierce at Penn (Pierce may have some lecture notes) or Frank Pfenning at CMU. Like Jackson and Morrisett these are all superb people well worth working with.

As to ultimate career goals, there are pockets of demand in industrial research (AT&T, Microsoft, Intel). There is also the aviation industry, and there is rocket science. (Holzmann is at the Jet Propulsion Laboratory.)

The US is not overrun with positions, but if you want one, you can find it.

Disclaimer: I started my CS career in formal methods, and while I may have moved on, I have not forgotten where I came from.

Answer 5

Honeywell has a division try them

Answer 6

@A5al Andy - I did a limited amount of FM studies in grad school (when pursuing a MS in CS.) In 15 years of practical, real world work, I've never used them. But that's because I've never worked on designing critical systems. But I do know that there are sectors that use them.

I'm currently working on the defense sector and while back on grad school (part-time) for a MS in Computer Engineering (with emphasis on systems engineering for the defense sector). Some of my professors have done actual work developing weapons and control systems. From what I understand, if you or I wanted to do work on FM outside of academia, you will have to work on companies that work in avionics, processor design, critical systems, nuclear systems, radars/communications, weapons, FTA, DoD, and the like.

But not only that, you will have to specialize probably by getting a Ph.D in CS (and a MS or some amount of grad studies - or work - in electronics, communications or computer engineering.)

The things that require formal methods are usually where multiple disciplines meet. That is, formal methods usually get employed not on systems engineering efforts, not just software engineering ones.

Looks like a Ph.D. in EE or CE with a strong background in software development has a better chance of working with formal methods in the defense/avionics industry. For example, as of today (05/23/2010), I've just found several openings in FM with Oracle, Qualcomm and other similar high-end software-hardware manufactures (unfortunately, almost all of them required a EE or Systems Engineering education.)

My advice is that you continue you continue your education in CS, specifically formal methods... and get a MS or additional grad education in Computer Engineering or Electrical... or a MS in systems engineering and a load of hardware courses.

One possibility is to look for jobs (hopefully in C/C++ and as close to the hardware as possible) with companies like BAE, Lockheed Martin, General Dynamics, Harris, Honeywell or with the DoD, MITRE, NSA, FTA, DOE, or Intel, AMD, Avaya, Ericsson, or Microsoft Research - look for defense, hardware design verification, avionics, aerospace, energy/nuclear and transportation.

Once you get that, continue your studies (usually, that type of company pays for it.) Of simply complete your FM studies and apply for jobs at those companies/industries.

In short, you have to 1) go beyond the MS in CS, 2) get a good education in EE/CE and systems engineering, and 3) look for jobs in the defense/energy/transportation sector or with big-shot companies that do a lot of work (or research) in hardware or critical systems.

Good luck.