Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 25 May 1993 22:44:44 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09622; Tue, 25 May 93 14:33:21 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from crl.dec.com by ted.cs.uidaho.edu (16.6/1.34) id AA09617; Tue, 25 May 93 14:33:11 -0700 Received: by crl.dec.com; id AA00990; Tue, 25 May 93 17:32:54 -0400 Received: by easynet.crl.dec.com; id AA28947; Tue, 25 May 93 17:32:35 -0400 Message-Id: <9305252132.AA28947@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Tue, 25 May 93 17:32:53 EDT Date: Tue, 25 May 93 17:32:53 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@ted.cs.uidaho.edu, nqthm-users@cli.com, theorem-provers@mc.lcs.mit.edu, rewriting-list@hutch.loria.fr, larch-interest@src.dec.com Cc: leonard@ricks.enet.dec.com Apparently-To: larch-interest@src.dec.com, rewriting-list@hutch.loria.fr, theorem-provers@mc.lcs.mit.edu, nqthm-users@cli.com, info-hol@ted.cs.uidaho.edu Subject: Formal verification of Alpha AXP at Digital JOB OPENINGS --- FORMAL VERIFICATION OF ALPHA I'm leader of an advanced-development project to apply formal verification to Digital's Alpha AXP (TM) chips. We currently have job openings in Hudson, Massachusetts, in the Semiconductor Engineering Group. If you'd like a job extending formal verification technology and applying it to verify real-world processors, I'm the person to talk to. I'm interested both in people just finishing college and in people who have been working for some time. Here's what I'm looking for: REQUIREMENTS: o Demonstrated ability to describe (digital) systems and their required behaviors in a formal logic, and to use formal-verification tools to prove that the specified systems meet their specs o Demonstrated ability to learn rapidly, and to apply the learning to become very productive o Current or imminent legal permission to work in the US o Interest in working in Hudson, Massachusetts, starting sometime in the next 6 months ADDITIONAL STRENGTHS THAT COULD BE A BIG HELP: o Understanding of RISC CPU design structures (caches, buses, etc), or logic synthesis, or CPU modeling, or traditional design-verification methods, or interactive theorem proving (with nqthm or HOL, for example) o Experience clarifying a vague task, organizing and scheduling the work, and bringing a complex and long-term project to a successful completion o Experience at project leadership o Experience structuring, writing, and maintaining large specs or proofs o Enthusiasm for extending academic methods to handle industrial constraints WHAT TO DO: If such jobs sound appealing, and you meet the requirements, I'd very much like to talk to you. Please send me a note at: Leonard@ricks.enet.dec.com Remember that you *must* tell me whether you are legally permitted to work in the US. Tim Leonard Semiconductor Engineering Group Digital Equipment Corporation (P.S. That's my professional side. Personally, my feelings are: Digital, a seriously big company, has taken a hard look at where to invest crucial resources, and has decided to make formal verification in industry real. This is GREAT --- now let's do it!)