Research positions in formal methods at Kestrel Institute

[apologies for multiple copies]
Career Opportunities at Kestrel Institute
in Palo Alto, California (http://www.kestrel.edu)

Kestrel has openings and is hiring and interviewing now.  We have
several openings in R&D for senior researchers as well as recent

About Kestrel Technology
Kestrel's focus is on advancing the state-of-the-art in software
development.  We are interested in highly automated design methods
that emphasize correctness, performance, scalability, productivity,
ease of use, and security.  These capabilities arise from the
articulation and incorporation of precise software design knowledge
and principles.

Areas of Interest
Toward the goal of advancing the state-of-the-art in software
development, Kestrel is interested in formal and mechanized support

  * Specification of software systems
  * Refinement / transformation of specifications
  * Design evolution
  * Code generation

We are interested in a variety of technologies as they apply to the
development of the next generation of software development

  * Algebraic specification
  * Algorithm design, software generators
  * Analysis techniques and slicing for programs and specifications
  * Category theory, mathematical logic
  * Constraint solving
  * Datatype refinement
  * Formal methods
  * Inference
     - First-order
     - Higher-order
     - Rewriting
     - Decision procedures
  * Program synthesis and optimization techniques
  * Program transformation
  * Refinement to high-performance parallel and sequential architectures
  * Semantics and type theory
  * Software architectures
  * User interface design
  * Visualization

Recent projects
Kestrel's recent projects include (among others):

  * Development of the theory and tools for the design and automated
    synthesis of high performance scheduling and planning algorithms for
    transportation, logistics, power plant maintenance, and manufacturing;

  * Synthesis of very fast parallel algorithms; 

  * High performance knowledge bases;

  * Security of network software;

  * Synthesis of data base integration software; 

  * Methods for evolving software and managing software changes and

  * Improving software analysis and testing using automated reasoning

  * On-the-fly software visualization; 

  * Specification, synthesis, verification and simulation of reactive

We are now hiring for several positions, and need people with
backgrounds ranging from Experienced Researchers to Recent Graduates.

We are interested in project staff as well as potential project
leaders.  We look for some (but not necessarily all) of these

1. Researchers - Ph.D. Level

   * Experience in program synthesis or related fields
   * Broad knowledge of formal methods and/or Knowledge-based methods
   * Deep knowledge of one or more formal methods areas
   * Excellent implementation skills
   * Excellent verbal communication and writing skills
   * Ability to perform original research and publish
   * Interest in developing working applications for end-users
   * Experience with automated proof systems
   * Ability to lead and manage projects
   * Skills in documentation and teaching

2. Researchers and Implementors at the MS Level

   * MS in Computer Science or equivalent
     (exceptional BS graduates will be considered)
   * Strong implementation and software engineering skills
   * Ability to work with applications of advanced mathematical concepts 
     to software engineering    
   * Documentation, support, training skills

3. Application Developers

   Our Application Developers may also be researchers and implementors
   who have interest in developing working applications based on our
   technologies.  Activities include documentation, support, contact
   with customers, and training.

   Our current applications include synthesis of very fast scheduling
   algorithms, parallel algorithms, secure software, very large knowledge
   bases, and several others.

The Best Of The Research And Commercial Worlds
  From Theory to Practical Applications
Kestrel provides opportunities for involvement in technology
transition, including equity interest in startup companies.  For
example, Kestrel licensed technology to Reasoning Inc, a company
active in Reengineering and Year 2000 Solutions.  
(See http://www.reasoning.com)

Kestrel is funded through government grants, as well as contracts with
private companies.  In order to prove the feasibility of our ideas,
and to transfer our theories to the real world, our research often
involves implementing working prototype systems and tranferring these
prototypes to commercial enterprises for development of products.

Kestrel Institute itself is an independent, non-profit research
institute, but is also affiliated with Kestrel Development
Corporation, a for-profit corporation.  Kestrel also licenses software
to other commercial enterprises.

Inquiries and Job Applications
Please send a resume or curriculum vitae, a statement of research
interests, a description of previous work, or questions (in any
combination). You may send these in ASCII, MS Word, or Postscript.

We are also interested in recent papers.  When sending email, we
prefer you to send pointers to papers (citations or URLs) rather than
the papers themselves.

If you do not yet have all of your materials assembled, we would
appreciate receiving what you do have (the URL for your web page, for
We strive to find world-class people and welcome qualified applicants
from outside the US.  Good English language skills are required.

Send email to: careers@kestrel.edu
or regular mail to 

	Kestrel Institute
	3260 Hillview Ave
	Palo Alto, CA  94304

or fax to (in USA) 415-424-1807

More information about Kestrel, and recent papers, can be found at


or by calling (in USA) 415-493-6871 (ask for Carol Lei).