[pl-seminar] [Fwd: Call for Interns]

[Thomas Reps <reps@xxxxxxxxxxx>]

-------- Original Message --------

Subject:	Call for Interns
Date:	Mon, 25 Feb 2008 11:27:38 -0500 (EST)
From:	Sagar Chaki <chaki@xxxxxxxxxxx>
To:	Thomas Reps <reps@xxxxxxxxxxx>
CC:	Arie Gurfinkel <arie@xxxxxxxxxxx>

Dear Tom

Hope this finds you well. The PACC Initiative at the SEI is looking for interns 
to work on a number of projects this summer. Please find a more detailed 
description below. Kindly circulate this amongst your students and anyone else 
who you think might be appropriate. We look forward to hearing from some of 
your exemplary students.

Best regards

-- Sagar

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

Call For Interns

The Predictable Assembly From Certifiable Code (PACC) initiative at the
Software Engineering Institute (SEI) is looking for Interns for the
Summer of 2008.

The PACC group works in the field of Automated Program Verification with
emphasis on software model-checking and static analysis. More
information is available at http://www.sei.cmu.edu/pacc and
http://www.sei.cmu.edu/pacc/comfort.html.

We are looking for interns to participate in (one or more) of the
following projects:

1. Abstract Interpretation and CEGAR-based Predicate Abstraction are two
competing techniques for analysis of software systems. We are developing
a framework for an effective and efficient combination of the two
techniques in a single analysis engine. The project will involve working
with us on designing and implementing new data structures, algorithms,
and developing benchmark suites.

2. Given ongoing advances in program verification technology, it is
important to regularly test the applicability of current technologies to
large scale, mature, and well designed projects such as Apache Web
Server or the Eclipse Platform. This project involves: (a) choosing a
suitable application domain, (b) identifying domain specific properties,
(c) evaluating applicability of existing tools (internal and external to
PACC), and (d) developing domain specific solutions when the tools are
not directly applicable.

3. One of the main missions of PACC is to advance the area of
evidence-based software certification. We have developed a novel
framework for generating certified executables. The key component in the
framework is a certifying model-checker: a model-checker that produces a
proof of correctness together with a yes/no result. We are looking for
an intern to collaborate with us on extending this work with particular
emphasis on efficiency, scalability and applicability to real-life programs.

Interested candidates should email their CV to pacc-intern@xxxxxxxxxxx.

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

-- 

------
Nothing has caused the human race more trouble than intelligence.

-- 
Thomas Reps
Professor
Computer Sciences Department
University of Wisconsin
1210 West Dayton Street
Madison, WI 53706
USA
<http://www.cs.wisc.edu/~reps>
(608) 262-2091 (direct)
(608) 262-6616 (secretary: Cathy Richard)
(608) 262-1204 (department)
(608) 262-9777 (fax)

On sabbatical leave, Aug. 2007 - Aug. 2008:

Office address:
Thomas Reps
Laboratoire LIAFA
Universite' Paris Diderot - Paris 7
175 rue du Chevaleret
Office 6A15
75013 Paris
France
E-mail: reps@xxxxxxxxxxx
Telephone: +33 (0)1.44.27.28.40 (Do not dial the (0) if you are outside France) 
Fax: +33 (0)1.44.27.68.49       (Do not dial the (0) if you are outside France) 

Mailing address: 
Thomas Reps
Laboratoire LIAFA
Universite' Paris Diderot - Paris 7
Case 7014
75205 Paris Cedex 13
France