Jobs

This is a list of position notices that I receive through various channels. These positions require skills and background in my areas of teaching and research. The list is in reverse chronological order of my receiving them. The entries show the date I posted the announcement. If I learn that a position has been filled or is no longer available, I will include that information in this listing. More often, however, I don't learn the outcome, so being in this list is no guarantee that the job is still available.

Links to other jobs lists
SRI

Job Opportunities in Formal Verification at Intel
--------------------------------------------------------------

The Intel CPU Design Centers in Austin, Texas and Portland, Oregon have
several openings in their Formal Verification groups.   We are looking for
outstanding candidates with knowledge of formal methods and microprocessor
architecture and design.

Intel has developed a strong formal verification tradition with a large,
experienced FV team that has applied FV methods on several previous
projects, most notably the Pentium 4 in Oregon.  The Texas Development
Center is a new design center with the challenging goal to develop future
Intel microprocessors using the latest tools and methods.

The essence of the job is simple -increasing confidence in the CPU design
using formal verification.  The work involves defining a comprehensive test
plan for FV, writing it in a formal language, and proving the properties
using our model checkers and theorem proving tools.  The job involves very
close interaction with the design team, with other validation teams, and
with Intel's internal R&D groups that improve and develop FV tools.  Intel
already has a very strong selection of FV tools, but, to ensure continued
competitive results, it is an ongoing process to refine and enhance
methodologies and tools.  A part of the FV work is to contribute to this
cross-site effort.

Presently Intel is looking for several extraordinary FV candidates to
participate in the exciting challenge of ensuring the coming generations
microprocessors are correct.  The ideal candidate will have a combined
knowledge of formal methods (preferably model checking and/or STE techniques
as well as theorem proving), tools development, and a good understanding of
and knowledge about hardware design and micro architecture.

Interested candidates should send their CV, (preferably in both plain ASCII
text and Postscript), to either/both:

Flemming.L.Andersen@intel.com                   Tom.Schubert@intel.com
FV Manager, Texas Development Center    FV Manager, DPG Oregon
(512) 314-0394                                  (503) 712-3522

Vacancy: postdoc position (3 years)

Where:   University of Nijmegen
         The Netherlands

Project: EU-project OMEGA
         Correct Development of
         Real-Time Embedded Systems in UML

Tasks:   integrate formal techniques in UML-based
         development of real-time embedded systems,
         including compositional system verification
         and formal refinement using the
         interactive theorem prover PVS.

More info: http://www.cs.kun.nl/~hooman/omega-ad.html

                Leipzig University of Applied Sciences
                    Department of Computer Science

                          Research Assistant

                      Provably Correct Software

The Department of Computer Science at the Leipzig University of
Applied Sciences offers a research assistant position within the
project "Provably Correct Software".

THE AIM of the project is the application of formal methods to safety
critical software, in particular to the embedding of payment systems
in E-commerce applications. The project continues our previous
research on automatic deduction and its applications in software
verification. The project will co-operate with the KIV-group at the
University of Augsburg and the German AI-Research Centre (DFKI).

APPLICANTS should have at least a good honors degree in computer
science, mathematics or a related engineering discipline, with
relevant research experience being a significant advantage. A
background in the development and/or application of formal methods and
verification techniques is desirable, together with an interest in
applications to software specification and verification. However,
highly motivated and academically strong applicants interested in
getting into the field are also encouraged to apply.

THE POST, funded by the BMBF (Federal Ministry for Education and
Research), is available from December 1, 2001. It will be filled for a
period of up to 18 months.  Salary is according to the German scale
BAT IIa-O, which is, roughly(!), about 65000 DM brutto per year,
depending on age, qualification, etc.

LEIPZIG has half a million inhabitants and is located 200 km south of
Berlin in the centre of the expanding economic region
Leipzig-Halle-Dessau.  Cultural highlights are the Thomaner Choir and
the Gewandhaus Orchestra being in the tradition of J.S.Bach and of
Bartholdy and Nikisch respectively. A characteristic of the town is
its rich inheritence of architecture, an attractive and vivid city
centre as well as green areas along the rivers.  Lovely countrysides
including wine yards, lakes, forests, mountains etc. are within a
distance of about 100 km.

APPLICATIONS (including CV, references, statement of research
interests) should be send --- if possible in German --- to

        HTWK Leipzig
        Personaldezernat
        Postfach 300066
        D-04251 Leipzig, Germany

In parallel, a notification should be sent by E-mail to:

 Prof. Dr. Uwe Petermann   E-Mail: uwe@imn.htwk-leipzig.de
 Leipzig University        WWW: http://koralle.htwk-leipzig.de
 of Applied Sciences
 Dept. of Computer Science
 Postfach 300066
 D-04251 Leipzig           Phone: + (49) 341 30 766 256/488
 Germany                   Fax :  + (49) 341 30 766 381

RESEARCH POSITIONS IN EDINBURGH AND MUNICH 
* Four research positions available, LFCS Edinburgh and LMU Munich, on
  "Mobile Resource Guarantees" project.  This is a collaborative
  project which is building foundational and practical infrastructure
  for endowing mobile code with independently verifiable certificates
  as to its resource consumption, in the form of condensed formal
  proofs, generated from typing derivations in linear type systems for
  describing resource bounds of high-level code.  
* For information see http://www.lfcs.ed.ac.uk/mrg.  
* Closing date: 31 Oct 2001.

Rob Hale
Research Associate
rob@cmagroup.com
Career Marketing Associates
http://www.cmagroup.com
Staffing & Consulting Solutions Since 1968
---------------------
This is a current active position in the Boulder, Colorado area.

Looking for a Sr Software Development Engineer to  participate in full
software lifecycle development for vehicle bus networks, to develop embedded
real-time software in 'C' for wireless data applications and support system
design and to verify test activities.

Requirements:
 5+ years of work experience in:
 *Firmware/Embedded
 *C
 *Microprocessor experience, preferably PIC
 *BSEE or BSCE
 -a strong knowledge of TCP/IP networking and wireless data communications
  is preferred but not required.

http://www.cs.stevens-tech.edu/Lab/SecureSystems_Lab/JoinUs.htm


                   Post-Doctoral Positions Available
                    Laboratory for Secure Systems 
                    Department of Computer Science
                   Stevens Institute of Technology

The Laboratory for Secure Systems at the Computer Science Department of
Stevens Institute of Technology invites applications for Post-doctoral
positions.

The Lab has been recently created, and its mission is to pioneer new
technologies for high-assurance and secure systems and prototype tools
that can provide guarantees that a system will not exhibit
unpredictable behavior in a hostile environment. Our objective is to
consolidate and organize research already under way at Stevens.

We are taking several approaches to language-based tools for
high-assurance, secure systems.  Language-based automated analysis can
be used to check components during development and also at the point
of deployment.  Such analyses can complement trust-based approaches to
security of mobile components and enhance performance by reducing
overhead of run-time checking. Language-based tools fit the
programming environments of professional practice, along side other
tools like test-generators and performance profilers.  Type-based
analyses can prevent leakage of privileged data even with dynamic
linking and replacement of libraries at run-time.  New abstractions
are being developed for fault-tolerant computation in wide area
networks.  Verification techniques can check correctness of
implementations of security protocols.

Much interest already exists in furthering the technologies, as
demonstrated by collaborations of the faculty amongst themselves, with
other academic institutions (e.g., with the Secure Internet Programming
Laboratory at Princeton, with the FLINT project at Yale, with the
University of Edinburgh), and with industrial partners (e.g., Lucent
Technologies).  Our work has current funding from industrial partners,
through multiple grants from the National Science Foundation and the
New Jersey Commission of Science and Technology.

Successful applicants will be enthusiastic team players with a strong
commitment to academic excellence. A PhD in Computer Science or
Applied Mathematics or equivalent education is required. Preference
will be given to applicants with experience in at least one of the
following areas:

   *Type theory
   *Static program analysis
   *Formal verification
   *Semantics of programming languages
   *Higher-order programming languages
   *Implementation of programming languages 

Post-docs will participate in state of the art research in
collaboration with other members of the Lab; they will produce
technical reports to document their findings, and participate in
building proof of concept software systems to experiment with research
advances.

The positions are initially for two years, renewable for a third year
upon performance and availability of funds. Positions are expected to
start with the new academic year in September 2001, but the starting
date is flexible.

Applicants should send a CV, a statement of research interests, and
arrange for three letters of recommendation to be sent to:

 Adriana Compagnoni 
 Department of Computer Science
 Stevens Institute of Technology
 Castle Point on Hudson
 Hoboken, NJ 07030
 U. S. A.
 e-mail: abc@cs.stevens-tech.edu

For more information contact 

 Adriana Compagnoni (abc@cs.stevens-tech.edu), 
 Dominic Duggan (dduggan@cs.stevens-tech.edu), or
 David Naumann (naumann@cs.stevens-tech.edu).

Stevens Institute of Technology is an Equal Opportunity Employer. 

Laboratory for Secure Systems
(http://www.cs.stevens-tech.edu/Lab/SecureSystems_Lab/)
Computer Science Department 
(http://www.cs.stevens-tech.edu/)

Two Postdoc Positions in the Computational and Applied Logic Group
------------------------------------------------------------------

Institute for Logic, Language and Computation
Universiteit van Amsterdam


The Computational and Applied Logic Group at the University of Amsterdam is
searching for highly motivated candidates with a PhD in computer science,
computational linguistics, or a related discipline, for two postdoc
positions, one in each of the following research areas:

 o computational logic (with an emphasis on implementation and evaluation
   of automated reasoning systems)

 o natural language processing (with an emphasis on logic-based approaches
   to information retrieval tasks such as question-answering, navigation, 
   and summarization)

Applicants should have a demonstrated capacity or potential to conduct
research in computational logic and/or natural language processing. 
Desirable criteria for both positions are: relevant industrial experience;
a record of project-based work; ability to supervise and inspire PhD
students.

These positions are funded by the Netherlands Organization for Scientific
Research and the University of Amsterdam, as part of the `Pionier' project
`Computing with Meaning.'  This is an interdisciplinary project aimed at
identifying and using meaningful information in natural language texts. 
The project will experiment with computational logic architectures that can
handle linguistic information structures at various levels of detail; this
involves new systems of flexible logics and algorithms, suitably combined. 
The project has a generous equipment and travel budget.  Please consult
http://www.science.uva.nl/~mdr/Projects/ComputingwithMeaning/ for more
information about the project.

Both positions are renewable for up to four years.  While both positions
are research positions, candidates are expected to play an active role in
supervising PhD students.  In addition, candidates may be asked to assist
with courses related to their research areas.  The salary will be between
5416 Guilders and 7128 Guilders, gross per month.  Knowledge of Dutch is
not a prerequisite, and candidates can be of any nationality.  The starting
date should be between September 1, 2001 and January 1, 2002.

Anyone interested in these positions is invited to contact Maarten de Rijke
at mdr@science.uva.nl.  Applicants should submit a full resume including a
list of publications, a statement of research interests, and the names and
email addresses of at least three references to the same address by July
15, 2001.

Research interests within the Computational and Applied Logic group range
from automated reasoning, constraint programming, satisfability checking,
and formal verification to digital libraries, information retrieval,
computational semantics, and knowledge engineering.  The group is strongly
internationally oriented, and currently consists of 15 people; it is
expected to grow substantially over the next year.  Further details on the
group can be found at http://www.science.uva.nl/~mdr/CALG/.

--
-- 
Maarten de Rijke  |  Computational and Applied Logic Group  |  ILLC
U of Amsterdam | Plantage Muidergracht 24 | 1018 TV Amsterdam  | NL
Phone: +31 20 525 6511 / +31 6 28 194 881   |  Fax: +31 20 525 5101
E-mail: mdr@science.uva.nl  |  URL: http://www.science.uva.nl/~mdr/

 Announcing Postdoc Positions at the CLIP group
 ----------------------------------------------
 School of Computer Science
 Technical University of Madrid


The CLIP (Computational Logic, Implementation and Parallelism) group
(http://clip.dia.fi.upm.es) at the School of Computer Science of
Technical University of Madrid is searching for candidates for
postdoctoral research positions in the research areas in which the
group is involved.  A PhD in Computer Science or related areas is
required.

These are research positions (no teaching is compulsory, although it
is allowed) and renewable for up to 5 years.  The initial salary is
28.548 Euros/year plus an initial budget of 5.707 Euros for travel and
other expenses during the first year.  Knowledge of Spanish is not a
prerequisite for application and candidates can be of any
nationality. The working language at the CLIP group for research is
English.

The number of positions available depends on the quality of the
applicants. The positions are co-funded by the Spanish Ministry of
Science and Technology and the Technical University of Madrid within
the "Ramon y Cajal" program. 

Interested applicants should send their C.V. and a description of
their research interests to the CLIP group
(clip-staff@clip.dia.fi.upm.es) by

** June 15 **

Selection will follow a two step process which is described in more
detail at http://clip.dia.fi.upm.es/Job_Openings/RyC.html

More details on the CLIP group, publications, projects, and research
areas of interest can be found at http://clip.dia.fi.upm.es (see
e.g. the group description at
http://www.clip.dia.fi.upm.es/clip_desc_bysys/clip_desc_bysys.html 
and the listing of research topics and publications at
http://clip.dia.fi.upm.es/clippubsbytopic/clippubsbytopic.html).

-- 
       =============================================================
       |     German Puebla     |      Facultad de Informatica      |
       |   german@fi.upm.es    | Universidad Politecnica de Madrid |
       | Phone +34-91-336-7449 | http://clip.dia.fi.upm.es/~german |
       =============================================================

University of Southampton

Department of Electronics and Computer Science


Research Fellows in Computer Science R/609

Closing date: 15 June 2001

The Department of Electronics and Computer Science (ECS) at Southampton
University is one of the largest and most successful departments in UK with
acknowledged international research excellence in both Electronics (5*
rated) and Computer Science (5 rated).  ECS is a lively, diverse,
research-led department with around 200 academic and research staff.

The Declarative Systems and Software Engineering Research Group is one of
nine research groups in ECS.  This Group wishes to make three new
appointments of Research Fellows to work on research projects in Critical
Systems and Systems Integration.  Appointments will be full time and will be
for two or three years. Salary will be in the range of £16775 to £25213 per
annum, according to age, qualifications and experience.

The projects are 'Automated Validation of Business Critical Systems' and
'Reasoning about Information Consistency'.  Candidates should have a PhD, or
equivalent experience, and research skills in Software Engineering,
Distributed Systems, Formal Methods or Systems Integration.

Further Particulars of the posts are available at
http://www.ecs.soton.ac.uk/~ph/vacancies/.

Application forms and job description may be obtained from the Personnel
Department, University of Southampton, Highfield, Southampton S017 1BJ; Tel:
023 8059 2750; email: recruit@soton.ac.uk or minicom: 023 80595595.  To be
returned not later than 15 June 2001.   Please quote reference.R/609..

Date: Wed, 23 May 2001 15:55:56 +0200 (MET DST)
From: olaf@ifi.uio.no
Subject: Open POSITIONS in FORMAL METHODS at University of Oslo

There are several positions (FULL PROFESSOR, ASSOCIATE
PROFESSOR, and PhD FELLOWSHIP) in Formal Methods at
University of Oslo, Department of Informatics, Norway.
See www.ifi.uio.no/~pma/ and in particular
http://www.ifi.uio.no/~pma/stillinger/positions.shtml

Professor Olaf Owe

Department of Electronics and Computer Science
University of Southampton

Lecturer in Formal Methods (Ref R689)

The Department of Electronics and Computer Science at Southampton is one of
the largest Departments in the UK. It has acknowledged international
research excellence in Electronics and Electrical Engineering (RAE rated 5*)
and Computer Science (RAE rated 5) and in teaching the QAA rating is 24/24
for Electrical and Electronic Engineering and Excellent for Computer
Science. Information about the Department can be found at
http://www.ecs.soton.ac.uk/.

The Department wishes to appoint a Lecturer in Formal Methods.  Research in
this area is based in the Declarative Systems and Software Engineering
Group, which holds several major research grants on Formal Methods for
business-critical systems and on model-checking and is a partner in a major
EU-funded project on industrialisation of Formal Methods. Applicants should
have a background in Formal Methods with experience of formal specification,
refinement, verification, theorem proving, model checking or method
integration. For further information, contact Professor Michael Butler,
+44(0)23 8059 2435, mjb@ecs.soton.ac.uk, also visit
http://www.ecs.soton.ac.uk/~mjb/.

Further particulars.

Salary scales: Lecturer: \24318,731 to \24330,967 per annum

Application forms may be obtained from the Personnel Department (R),
University of Southampton, Highfield, Southampton, SO17 1BJ, Tel: 023 805
92750, e-mail: recruit@soton.ac.uk or minicom: 023 8059 5595. Applications
to arrive no later than 22 June 2001. Please quote reference number R689.

UNIVERSITE LIBRE DE BRUXELLES
Faculte des Sciences
Departement d'Informatique

FACULTY POSITION AVAILABLE

We invite applications for 3 full-time faculty positions at the level of

tenure-track "Charge de Cours" (first professorial level) to begin
from October, 2001.

see also http://www.ulb.ac.be/di/
_______________________________________________________________________

The Universite Libre de Bruxelles is opening  three full-time
tenure-track academic positions in its Computer Science Department, in
the Faculty of Sciences.
The responsabilities of the new professors include teaching (typically
at most 150 hours per year), research including supervision of PhD and
Master students and some comittment to the administrative life of the
institution. Preference will be given to candidates with research
achievements in one or several of the areas relating to the following
fields :

                                 Algorithms
                                 Software Engineeiring
                                 Formal Methods and Verification
                                 Stochastic modeling
                                 Security
                                 Distributed Systems

Still, other areas of competence will also be considered based on the
quality of the research achievements of  the candidate.  The candidates
will be evaluated on their capacity to either reinforce existing
research lines within the Department or to create new ones, and produce
a high level teaching.  The candidates must have a  PhD thesis in a
subject related to Computer Science, have a strong international
publication record and show capacity for teaching (in french, a working
knowlegde of french or at least a commitment to acquire it within a
reasonable period is expected).

People  from outside of the Universit\351 Libre de Bruxelles, will first be
given a probationary period of three years, after that period, the
position will become permanent.

                      TOOL SUPPORT FOR LOGICAL CALCULI
                       Research Assistant/PhD Vacancy
                         Technical University Munich

The theorem proving group (http://www4.in.tum.de/~kleing/group/group.html) at
the Technical University Munich is looking for a research assistant to join a
DFG-funded project focussing on the development and application of the
theorem prover Isabelle (http://isabelle.in.tum.de).  The position offers
exciting opportunities for scientifically challenging research leading to a
PhD. The appointment is initially for 2 years with an optional extension.

We seek a candidate with a strong background in at least one of the following
areas

- theorem proving
- logic
- semantics of programming languages
- functional/logic programming
- specification languages

who should like to work on the boundary between theory and practice.
Depending on the candidates interests and abilities, the work can focus an
either of the following areas:

- logical calculi for the development of (object oriented) programs
- structuring mechanisms for large theories
- tool support for automated reasoning


Informal inquiries and formal applications should be addressed to
nipkow@in.tum.de (http://www.in.tum.de/~nipkow).

         Department of Computing & Electrical Engineering
                      Heriot-Watt  University
                      Edinburgh, Scotland, UK
                          

  "Automatic Guidance for the Formal Verification of High Integrity Ada"

                   Research Associate/Fellow Position


Applications are invited for a Research Assistant/Research Fellow post
available under EPSRC grant GR/R24081 -- Critical Systems Programme.

The aim of this project is to investigate techniques for automating the
formal verification of software for critical systems. In particular we 
will focus upon Spark, a subset of the Ada programming language developed 
by Praxis Critical Systems (see http://www.praxis-cs.co.uk). Spark has a 
proven track record in the production of software for critical systems 
within the finance, aerospace, rail and telecommunications markets. 
Formal verification of software written in Spark is supported by the 
Spade interactive Proof Checker. In this project we will investigate the 
role that Proof Planning can play within the formal verification of 
Spark software. Proof planning is an AI technique that exploits high-level 
proof patterns in guiding the search for proofs. As well as increasing 
automation, proof planning has a proven track record in enhancing the level 
at which users can interact during proof search. The time is now ripe to 
test the capabilities of proof planning on "industrial strength" problems, 
this collaborative project with Praxis will enable us to achieve this goal. 
For more details of the proposal see http://www.cee.hw.ac.uk/~air/clam-spark/.

The post requires a computer scientist with a PhD or comparable research
experience.  Ideally, the appointed candidate will be an expert in theorem
prover design and implementation, applied formal methods, or high integrity
software development. 

The post is for 3 years, the aim is to start the project in October 2001,
but the actual start date is open to negotiation. The appointment will be 
on the RA1A Scale (18,731-20,465 pounds p.a.) with an annual increment. 
While the project is based at Heriot-Watt University in Edinburgh, site 
visits to Praxis in Bath will be required during the project period. 

The Department of Computing and Electrical Engineering at Heriot-Watt 
University received a 4B in the 1996 Research Assessment Exercise in the 
Computer Science unit of assessment. It is housed in a modern building, 
with excellent computer and infrastructural facilities. The Dependable 
Systems Group is a dynamic research group whose strengths lie in the areas 
of theorem proving; formal verification and synthesis; design and 
implementation of parallel and distributed functional languages; performance 
modelling and simulation of parallel and distributed systems. The Dependable 
Systems Group has very strong links with the Mathematical Reasoning Group 
within the Division of Informatics at the University of Edinburgh. These 
links will provide an important source of interaction during the project.

The city of Edinburgh offers many attractions including theatres, art 
galleries, sports facilities and restaurants. Known as the `festival city', 
it annually hosts the world's largest International Arts Festival. The 
spectacular scenery of the Scottish Highlands and Islands are within 
easy reach.

Written applications should be sent to 

        Dr Andrew Ireland, 
        Department of Computing & Electrical Engineering, 
        Heriot-Watt University, 
        Riccarton, Edinburgh
        Scotland, UK
        EH14 4AS  

to arrive no later than 31 March 2001.  Your application should include 
a covering letter outlining your qualifications for the position, a 
Curriculum Vitae, a complete list of publications, and the names and 
addresses of two academic referees.  Informal inquiries are also welcome, 
these should also be sent to Andrew Ireland - a.ireland@hw.ac.uk.

                    THE UNIVERSITY OF BIRMINGHAM 
                     SCHOOL OF COMPUTER SCIENCE
                    Postdoctoral Research Fellow


Applications are invited for a Postdoctoral Research Fellow to work on
the project `The Feature Construct in Programming and Specification
Languages', funded by EPSRC and British Telecom, coordinated by Dr.
Mark Ryan and Dr. Marta Kwiatkowska.  Applicants should have a PhD in
Computer Science and ideally have some knowledge of one or more of the
following areas: model checking, temporal logic, and/or program
semantics.  The successful applicant may be expected to contribute to
teaching in the School up to a maximum of two hours per week on
average.  More information about the project, the research group and
the School can be obtained from the URLs:

    www.cs.bham.ac.uk/~mdr/fc
    www.cs.bham.ac.uk

The starting salary will be up to 19,482 pounds per year. The post is
for three years from 1 April 2001 or as soon as possible
thereafter. 

Application forms and further particulars available from:

The Director of Personnel Services
The University of Birmingham
Edgbaston, Birmingham, B15 2TT
tel: + 44 (0)121 414 6486 (24 hours)
email: h.h.luong@bham.ac.uk
Application forms are available from the WWW, at

www.bham.ac.uk/personnel/app.htm


Please quote reference S35522/01.  The closing date for applications
is Monday 19th March 2001. Late applications will be considered if the
selection process has not advanced too far.

Informal enquiries are welcome, and should be addressed to:
Mark Ryan, tel:  +44 (0)121 414 7361, email: M.D.Ryan@cs.bham.ac.uk.

The University of Birmingham is working towards equal opportunities.

    Job opportunity
    *  Model checking
    *  flexible balance of theory/applications, to suit applicant
    *  good research environment
    *  ability more important than relevant experience
    *  informal enquiries welcome


                    THE UNIVERSITY OF BIRMINGHAM 
                     SCHOOL OF COMPUTER SCIENCE
                    Postdoctoral Research Fellow


Applications are invited for a Postdoctoral Research Fellow to work on
the project `The Feature Construct in Programming and Specification
Languages', funded by EPSRC and British Telecom, coordinated by Dr.
Mark Ryan and Dr. Marta Kwiatkowska.  Applicants should have a PhD in
Computer Science and ideally have knowledge of one or more of the
following areas: model checking, temporal logic, and/or program
semantics.  The successful applicant may be expected to contribute to
teaching in the School up to a maximum of two hours per week on
average.  More information about the project, the research group and
the School can be obtained from the URLs:

    www.cs.bham.ac.uk/~mdr/fc
    www.cs.bham.ac.uk


The starting salary will be up to 19,482 pounds per year. The post is
for three years from 1 April 2001 or as soon as possible
thereafter. 

Application forms and further particulars available from:

The Director of Personnel Services
The University of Birmingham
Edgbaston, Birmingham, B15 2TT
tel: + 44 (0)121 414 6486 (24 hours)
email: h.h.luong@bham.ac.uk
Application forms are available from the WWW, at
www.bham.ac.uk/personnel/app.htm

Please quote reference S35522/01.  The closing date for applications
is Friday 9th March 2001. Late applications will be considered if the
selection process has not advanced too far.

Informal enquiries are welcome, and should be addressed to:
Mark Ryan, tel:  +44 (0)121 414 7361, email: M.D.Ryan@cs.bham.ac.uk.

The University of Birmingham is working towards equal opportunities.

From: Hatheway James-R3185C 

Motorola is looking for several exceptional candidates to join our Formal
Methods / Formal Verification (FM/FV) group at Motorola's Somerset Design
Center in Austin, Texas.  The Somerset FM/FV group will apply and develop
new methods for designing and verifying PowerPC microprocessors and
processor components.  Our goal is to contribute to a very high standard of
design in all phases of product development by putting formal methods and
formal verification into practice.

Formal methods / formal verification responsibilities will include
constructing formal models and specifications of PowerPC processors and
processor components using state-of-the-art formal verification techniques
such as equivalence checking, model-checking, symbolic trajectory
evaluation, theorem proving, and symbolic simulation to ensure that
RTL-level designs implement these specifications.

Individuals must demonstrate technical leadership in working with multiple
groups to help define Motorola's future FM/FV strategy and the necessary
tools to implement it.  Candidates must be able to interface with all
disciplines of chip design, including system architects, logic designers,
and verification engineers.

The Somerset Design Center has a strong history of applying formal methods /
formal verification techniques, and the FM/FV group has the unique
opportunity to impact the very way that Motorola goes about designing and
verifying microprocessors.

If you are looking for an exciting position putting formal methods and
formal verification into practice, and if you are seeking a position in
which you will have a significant impact on design and verification
practices, I urge you to consider applying for this position.

The ideal candidate will have a strong background in formal methods / formal
verification, hardware design, and computer architecture. Background in the
following fields would be an asset: microprocessor design and verification,
model-checking, theorem proving, symbolic trajectory evaluation, software
development in ML or C/C++, hardware description languages such as Verilog
or VHDL.  Two to ten years' experience in the industrial application of
formal methods / formal verification would be preferred, but we also welcome
applications from outstanding candidates with relevant advanced degrees, but
less industrial experience.

Summer internships are also available for students who would like to augment
their studies with some practical experience.

If you are interested, please contact James Hatheway at r3185c@email.mot.com
or 1-800-531-5183 ext. 4082.

Thank you!

James Hatheway
Recruiter
Motorola Global Talent Supply Team
Austin, Texas
(512) 996-4082
(800) 531-5183 x4082
r3185c@email.mot.com
2-way pager:  877 576 0768 or 8775760768@skytel.com

From: Till Mossakowski 

The following two research assistant positions
are available at the University of Bremen, Germany.

The Bremen Institute of Safe Systems in the Center for Computing
Technologies at the University of Bremen hosts the research projects

"Multi-logic systems as a basis for heterogeneous specification
and development" (MULTIPLE)

and

"Algebraic specification + functional programming =
environment for formal software development" (HasCASL)

funded by the Deutsche Forschungsgemeinschaft (DFG).


Within the framework of each of these projects, one position in the
working group of Prof. Dr. Krieg-Br\374ckner is to be immediately
filled for at least  two years (additional option for another two
years),
subject to availability of funds:

Research Assistant
Verg. Gr. IIa BAT (full time)

In addition to successful university studies in computer science,
experience and skills in functional programming (e.g. Haskell, ML)
are expected. Familiarity with at least one of formal specification
methods (like  CoFI/CASL), theorem proving or category theory is
desirable.

Applicants with a PhD are welcome. However, there will also be the
oppurtunity to prepare a PhD thesis in connection with the research
project.

In case of essentially equal qualification in the subject and personal
suitability, severely handicapped applicants will be preferred. The
University of Bremen intends to increase the share of women in
scientific activities and does therefore strongly encourage women to
apply for these positions.

More detailed information about the projects can be found under
http://www.tzi.de/cofi/projects/multiple.html
http://www.tzi.de/cofi/projects/hascasl.html

 Please address your application with the usual documents and the reference number A164/00 (MULTIPLE) resp. A165/00 (HasCASL)
before 01.02.2001 to:

UNIVERSIT\304T BREMEN
Prof. Dr. B. Krieg-Br\374ckner
Fachbereich 3
Postfach 33 04 40
28334 Bremen
e-Mail:  cofi@tzi.de
--
Till Mossakowski                Phone: +49-421-218-4683, monday:
+49-4252-1859
Dept. of Computer Science       Fax:   +49-421-218-3054
University of Bremen            EMail: till@tzi.de
P.O.Box 330440, D-28334 Bremen  WWW:   http://www.tzi.de/~till

From: Andy Moran 
Reply-To: James Hook , Andy Moran 
Organization: Oregon Graduate Institute

			     POST-DOCS AVAILABLE

		       Pacific Software Research Center

	      Oregon Graduate Institute of Science & Technology

The Pacific Software Research Center (PacSoft) explores declarative techniques
for dramatically improving the software development process.  The Center is
composed of faculty (Mark Jones, John Launchbury, James Hook, Richard
Kieburtz, Tim Sheard, Andrew Tolmach, and Michael Gordon (*)), graduate
students and professional staff, and currently numbers over a dozen full-time
technical people.

The Center has active research programs in compiler technology for
functional languages, software-enabled control, meta-programming and the use
of design automation tools for software generation, specification, semantics
and implementation of domain specific languages (including domain analysis),
automatic program optimization using fusion and partial evaluation, the
specification of microprocessor microarchitectures using functional
languages, and the use of formal methods for specification, analysis and
verification.  In addition the Center runs an active visitor program which
attracts high quality researchers from around the world.

POST-DOCS AVAILABLE

PacSoft has immediate openings for postdoctoral researchers to work on the
Programatica project.  Programatica is an environment for the simultaneous
development of systems and formal models of systems that leverages functional
programming, theorem proving, and other applied formal methods.  The primary
application area of Programatica is modeling information assurance properties.

The Programatica approach is best summarized as "programming as if properties
mattered".  The aim is to support the development of high-assurance programs
(that is, programs that satisfy desirable formal properties and are proven to
do so) without overwhelming the developer with proof minutiae.  By varying the
degree of validation applied to properties (all the way from simple assertion
through to model checking and full-blown theorem proving), a Programatica
developer will be able to concentrate on those properties crucial to their
system (such as separation axioms for secure systems).

Candidates are sought with expertise in the application and implementation of
theorem proving technology, applications of higher-order, typed functional
languages, or other areas related to information assurance and applied formal
methods.

To apply, please send a CV with a brief description of your research
accomplishments and interests, including the names of at least three
references. Send applications to:

	Position #CSE 8-3-00
	Personnel Office
	Oregon Graduate Institute of Science and Technology
	20000 NW Walker Rd.
	Beaverton, Oregon 97006

Email submissions of the same materials may be sent to jobs@admin.ogi.edu.
Include position number in the subject line.

OGI is an Equal Opportunity Employer and particularly welcomes applications
from qualified women, minorities, and individuals with disabilities.
Appointment is subject to the availability of funding.

Questions (but please no application materials!) may be directed to
Professor James Hook, email: hook@cse.ogi.edu, phone: 503-748-1169.
Information about the Pacific Software Research Center and the Programatica
project can be found on the world wide web at the URL:

	
	http://www.cse.ogi.edu/PacSoft/
        

(*) Visiting from Cambridge University.

From: Eduardo Gimenez 
Organization: Trusted Logic
Subject: Smart Cards and Program Verification : Employment Opportunities

========================================================================
    Employment Opportunities on Smart Cards and Program Verification
========================================================================

Created in January 1999, TRUSTED LOGIC (www.trusted-logic.fr) is a
fast growing company. It now counts 30 persons and is looking for 
more people with a good background in formal methods to join its team.

At TRUSTED LOGIC, we combine an intimate knowledge of embedded
software major challenges and an expertise in state-of-the-art formal
methods analysis. Such a double competence allows us to offer
efficient and secure solutions for smart cards and terminals.

We are proud to number the main actors in the smart card and in the
embedded software industry among our customers (Sun Microsystems Inc.,
VISA International, Bull, Schlumberger, Gemplus, Oberthur, etc.). Our
team also prepares proprietary innovative and advanced components for
secure embedded systems. 

Several positions are immediately available for security development 
engineers and/or people with former experience in Computer Science 
research.

QUALIFICATIONS REQUIRED:

-  A good qualification in at least ONE of the following key
   competence list:

  + formal program verification (theorem proving, static analysis, 
    model-checking, etc);
  + security evaluation (Common Criteria, ITSEC, etc),
  + semi-formal methods in software engineering (UML, etc),
  + advanced systems components development (type-checkers, compilers,
    virtual machines, etc)
  + secure applets development (Java, Multos, C, C++)

*PLUS* a strong motivation to acquire skills and to invest in new fields.

- Experience in the use of a proof environment (like for example Coq, 
  HOL, Isabelle or PVS) and/or in the the JavaCard programming
  language would be a plus. 

- Self-managed, rigorous and a good ability to work in a team.

EXPERIENCE:

- At least a Master or Engineering degree in Computer Science or a
  related field, or equivalent experience.
- Junior (0 to 2 years experience) and Senior (3 or more years
  experience) applications will be considered.

LANGUAGES: A good level of written and spoken English or French.

CONTRACT: Temporary and permanent positions are both available.

LOCATION: Positions are located in France, either in Versailles, close
           to Paris, or in the Nice area, on the French Riviera.

APPLICATIONS: 

- by e-mail to contact@trusted-logic.fr. Please, put your résumé (CV) 
  and cover letter in plain text in the body of the mail (no attached 
  file will be considered); 

 - by post to : 
       TRUSTED LOGIC
       5, rue du Bailliage
       78000 Versailles (France) 

============================================================================

CWI (Center for Mathematics and Computer Science) in Amsterdam 
and TU/e (Eindhoven University of Technology) in Eindhoven
are looking for:

        2 PhD-researchers  (4 years)

for the following joint research project:

Integrating Techniques for the Verification of Distributed Systems
==================================================================

The goal of the project is the comparison and development of
algorithms for the automatic verification of large formulae (in the
boolean/arithmetic realm).  We also strive for efficient
implementations of such algorithms, in order to test their
effectiveness on benchmark formulae. These formulae arise from our
continuous investigations in the symbolic verification of distributed
systems.

More specifically, we expect promising results by comparing and
combining existing techniques, such as resolution, binary decision
diagrams and term rewriting.

One of the candidates will work at CWI (Amsterdam) in the group
"Specification and Analysis of Embedded Systems", the other at TU/e
(Eindhoven) in the group "Embedded Systems". These groups have
a strong collaboration, and have their merits in theoretical
results as well as industrial applications on distributed systems.

For more information, please find the research proposal on
http://www.cwi.nl/~vdpol/itvds.ps, or contact:
Prof. Dr. Ir. J.F. Groote TU/e    jfg@win.tue.nl       +31 (0)40 247 4416
Dr. W. Fokkink          CWI   Wan.Fokkink@cwi.nl       +31 (0)20 592 4104
Dr. J.C. van de Pol     CWI   Jaco.van.de.Pol@cwi.nl   +31 (0)20 592 4137
Dr. H. Zantema          TU/e  hansz@cwi.nl 

If you are interested in this challenging project, and (nearly)
finished your study in computer science, mathematics or logic,
please react soon, by sending your CV, including an abstract
of your master's thesis and a list of marks, to the project leader 
Dr. J.C. van de Pol, CWI, Postbus 94079, 1090 GB Amsterdam, 
or (preferably) by E-mail to Jaco.van.de.Pol@cwi.nl.

Date: Fri, 06 Oct 2000 15:12:50 +0200
From: Laurent Thery 

A one-year postdoc grant is available at INRIA within
the cooperative action AOC. This action regroups three
research teams of INRIA (french national research institute)
interested in mechanically deriving properties of arithmetic 
operators and algorithms. 

We are looking for a candidate that either is familiar
with computer arithmetics (in particular floating point
arithmetic) or has some strong knowledge in formal methods
(especially theorem proving).

For more information and application , please contact:

Laurent Thery    
Email: Laurent.Thery@sophia.inria.fr
Phone: (33) 4 92 38 78 16 
Address:
Projet Lemme INRIA - Sophia Antipolis,
2004, route des Lucioles - B.P. 93 
06902 Sophia Antipolis Cedex France 


Link: http://www-sop.inria.fr/lemme/AOC/index.html.en

From: "Andersen, Flemming L" 
Subject: Job opportunities at Intel TDC - Austin
Date: Thu, 5 Oct 2000 15:24:35 -0700 
==========================================================================
Job opportunities at Intel TDC - Austin
-------------------------------------------------------
The Intel Texas Development Center (TDC) in Austin is looking for
outstanding candidates to join its Formal Verification group.

Intel has applied formal verification (FV) methods on several of its
previous projects and the company has a strong FV tradition and large group
of highly skilled FV people.  The Texas Development Center is a new center
of excellence with the challenging goal to improve existing tools and
methodologies used both for processor development as well as validation and
verification.

The TDC FV group will apply and develop new methods to create new ways of
verifying microprocessors correct.  Its first challenge is to apply these
techniques on one of the latest processor designs currently being developed
here in Austin.  The goal for the FV group is to contribute to and help
secure a very high standard of the design in all phases of the development.

Intel already has a very strong selection of FV tools, but, to ensure
continued competitive results, it is an ongoing process to refine and
enhance methodologies and tools.  A part of the TDC FV work is to contribute
to this across site effort.

Presently Intel is looking for several extraordinary FV candidates to
participate in the exciting challenge of ensuring the coming generations
microprocessors correct.  The ideal candidate will have a combined knowledge
of formal methods (preferably model checking and/or STE techniques), tools
development, and a good understanding of hardware design and micro
architecture.

If you are interested, please contact: Flemming.L.Andersen@intel.com or
call: (512) 314-0394

PS. If you call from abroad: The Austin timezone is Greenwich standard time
-6 hours

Flemming Andersen

SRI INTERNATIONAL, CAMBRIDGE, UK
--------------------------------

Formal Methods Researchers
--------------------------

SRI International has an immediate need for post-doc researchers in formal
verification to work at its Cambridge Computer Science Research Centre in
the UK.  The initial requirement is on a three-year project to apply formal
techniques in the construction of intrusion tolerant systems
(
(http://dtsn.darpa.mil/iso/programtemp.asp?mode=346) and in particular to
investigate proof-based methods for on-the-fly intrusion detection.
Applicants with a background in automatic verification or model-checking
would be especially welcome.  Experience of fault tolerance or security
would be useful but not essential.

SRI International (http://www.sri.com) is one of the world's largest
independent nonprofit research institutes with an enviable reputation in
computer science.  Our Cambridge laboratory (http://www.cam.sri.com) is
currently expanding. It specialises in the areas of formal methods,
information assurance and natural language processing and has several
government and commercially-funded research projects in these areas.

All positions are to be filled as soon as possible.  Salaries and other
terms depend on experience and circumstances, but will be very competitive.
SRI also offers relocation and a comprehensive benefits package, including
royalty and equity sharing.

Applications, including CV, should be sent to careers@cam.sri.com. Informal
enquiries can be directed to Dr. Roger Hale (roger.hale@cam.sri.com).

Date: Mon, 25 Sep 2000 14:57:00 +0200
From: Bart Jacobs 

Several PhD and postdoc positions are available in the area
of formal methods for object-oriented languages, at the University
of Nijmegen, The Netherlands.

The emphasis lies on using proof tools (esp. PVS) for Java(Card)
program verification.

More information at the URL:
	
	http://www.cs.kun.nl/~bart/LOOP/vacancies.html
        
Best regards,
Bart Jacobs.

Sender: nipkow@informatik.tu-muenchen.de
Subject: Research Assistant/PhD Vacancy
Date:   Wed, 13 Sep 2000 10:23:22 +0000

                        THEOREM PROVING FOR JAVA CARD
                       Research Assistant/PhD Vacancy
                         Technical University Munich

The theorem proving group at the Technical University Munich is looking for a
research assistant to join an EU-funded collaborative project focussing on
the specification and verification of Java implementations for smart cards.
The position offers exciting opportunities for scientifically challenging and
industrially relevant research leading to a PhD.

We seek a candidate with a strong background in one of the following areas

- theorem proving
- logic
- semantics of programming languages
- functional/logic programming

who should like to work on the boundary between theory and practice.
The appointment is initially for 33 months with a possible renewal.
Starting date is negotiable within the next 6 months.

Informal inquiries about the position may be addressed to nipkow@in.tum.de
(www.in.tum.de/~nipkow). Formal applications should be sent by e-mail or to
the following address:

  Prof. Tobias Nipkow
  Institut fuer Informatik
  Technische Universitaet Muenchen
  Arcisstraße 21
  D-80290 Muenchen
  Germany

They should include a curriculum vitae, a copy of your master's thesis, and
the names of two personal references. Please ask your references to send
their letters directly to nipkow@in.tum.de.

From wolfstal@il.ibm.com
Date: Sat, 9 Sep 2000 15:38:54 +0300
Subject: IBM/Israel: Open Positions in Formal Methods & CAD



See
http://www.haifa.il.ibm.com/info/jobs_verification-technologies-developer.html

The hiring department is described at
http://www.haifa.il.ibm.com/projects/verification/RB_Homepage/

To apply, please send your resume to wolfstal@il.ibm.com,
and/or call me at +972 4 8296277 for more details.

-Yaron Wolfsthal

Date: Fri, 08 Sep 2000 11:04:57 +0200
Organization: Dept. of CS, Chalmers, Sweden
Subject: Professorship in Software Engineering 

Our sister department, the dept of Computer Engineering is announcing
a chair in Software Engineering. From their description:

   "The professorship will deal with methods and techniques 
    for the development of software, and also in industrial settings. 
    This includes theories and applied methods for specification, 
    verification and validation of functional characteristics 
    along with issues pertaining to quality, dependability, 
    security and safety. 
    Issues related to production, maintenance and management of 
    software systems are also of interest." 


The full description can be found from their homepage


http://www.ce.chalmers.se/MenyE/


Sincerely,

Bengt Nordstrom