[TYPES/announce] 3 years research assistant position in TCS, LMU Munich

2010-11-03 Thread Martin Hofmann
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A position for a research assistant in a DFG project is
available.

Project title: Pointers as an abstract data type:
complexity-theoretic and programming-language aspects (PURPLE)

Investigators: Martin Hofmann and Ulrich Schöpp

Duration: 36 months

Start date: as soon as possible but not later than June 2011.

Remuneration: German scale 13 TV-L (38k-54k EUR according to age,
experience, family status)

Background: PhD in theoretical informatics with some topical overlap,
see project description. Candidates with an excellent Diploma or
Master in this area are also encouraged to apply; in this case
the project work may lead to a PhD.

Location: The project will be carried out at the Institute for
Informatics of Ludwig-Maximilians-Universität Munich, Germany.
LMU is an equal opportunities employer.

Applications should be sent by E-Mail to Sigrid Roden
ro...@tcs.ifi.lmu.de as a single PDF file containing in particular CV,
research statement, and the names of two potential referees. There is
no deadline. Applications will be assessed on an on-going basis until
the position is filled.

Questions about the position can be directed to the investigators
{mhofmann, schoe...@tcs.ifi.lmu.de.

Project description:

In programming languages and logics, graphs and similar data
structures are often treated as structured data rather than
bit-sequences or words. This means that elements of abstract data
structures are often accessed using pointers, which support only a
restricted set of operations, such as lookup, update and test for
equality. The concrete representation of pointers remains
hidden. Traditional computability and complexity theory, on the other
hand, rely on concrete representations of data.

In this project we want to explore the expressivity of abstract
pointer concepts in the sense of complexity theory. In particular we
aim at a separation of programming language versions of LOGSPACE and
PTIME. For example, we conjecture that the PTIME-complete problem of
Horn-satisfiability cannot be solved with a constant number of
abstract pointers, even in the presence of non-determinism or an
oracle for reachability.

Additionally, we want to contribute to the formal specification and
verification of programs with abstract pointers. For instance, we
would like to ascribe rigorous meaning to preconditions like `It makes
no guarantees as to the iteration order of the set ...' in the
specification of the HashSet class in java.util.

For further background reading, we refer to:

- Project proposal to Deutsche Forschungsgemeinschaft (DFG):
  http://www2.tcs.ifi.lmu.de/~schoepp/Docs/purple_antrag.pdf

- Martin Hofmann und Ulrich Schöpp. Pure Pointer Programs with
Iteration.  ACM Transactions on Computational Logic, 2010.

- Martin Hofmann und Ulrich Schöpp. Pointer Programs and Undirected
Reachability. Logic in Computer Science (LICS), 2009.  Extended
version: Electronic Colloquium on Computational Complexity (ECCC)
15(090), 2008








[TYPES/announce] MEMOCODE 2011 Call for Papers

2010-11-03 Thread Alain Girault

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


MEMOCODE 2011 Call for Papers

The ninth ACM-IEEE* International Conference on Formal Methods and
Models for Codesign (MEMOCODE 2011) will be held on July 11-13, 2011
in Microsoft Research Cambridge, UK.

http://www.memocode-conference.com



IMPORTANT DATES

Abstract submission deadline: February 25, 2011
Paper submission deadline:March 4, 2011
Notification of acceptance:   April 29, 2011
Final Version for Papers: May 13, 2011
Poster submission deadline:   May 13, 2011
Notification for Posters: May 27, 2011




The ninth MEMOCODE conference will attract researchers and
practitioners who create methods, tools, and architectures for the
design of hardware/software systems.  These systems face increasing
design complexity including tighter constraints on timing, power,
costs, and reliability. MEMOCODE seeks submissions that present novel
formal methods and design techniques addressing these issues to
create, refine, and verify hardware/software systems. We also invite
application-oriented papers, and especially encourage submissions that
highlight the design perspective of formal methods and models,
including success stories and demonstrations of hardware/software
codesign. Furthermore, we invite poster presentations describing
ongoing work with promising preliminary results.


Topics of interest for regular submissions include but are not limited
to
* system- and transaction-level modeling and verification, abstraction
  and refinement between different modeling levels, formal,
  semi-formal, and specification-driven verification,
* design and verification methods for composition of concurrent
  systems: multi-core platform architectures, systems-on-chip,
  networks-on-chip,
* formal methods and tools for hardware and software verification
  including theorem proving, decision procedures,
* non-traditional and domain-specific design languages for hardware
  and software, novel models of computation, and new design paradigms
  that unify hardware and software design,
* system-level estimation of performance and power in heterogeneous
  hardware/software architectures,
* applications and demonstrators of formal design methodologies and
  case studies of innovative system-level design flows,
* modeling and reuse of intellectual property at system-level, and
* design abstraction and high-level design demonstrating productivity
  and quality in generating and validating RTL and software.

PROCEEDINGS:

Conference proceedings will be published by the IEEE Computer Society.

SUBMISSION:

Submissions of research and experience papers will only be accepted
through the conference website. Papers must not exceed 10 pages and
must be formatted following IEEE Computer Society guidelines.
Submissions must be written in English, describe original work, and
not substantially overlap papers that have been published or are being
submitted to a journal or another conference with published
proceedings.  Poster submissions should consist of an abstract of at
most 250 words. The abstract will be distributed to the conference
attendants but will not be published. Note that the poster deadline is
different from the paper deadline.

SUBMISSION WEBSITE:

http://www.easychair.org/conferences/?conf=memocode2011



DESIGN CONTEST:

MEMOCODE will again have a design contest. The contest will start
March 1, 2011.  The deadline for submission is 31 March 2011 and the
notification of the results is on May 13, 2011. The conference will
sponsor at least two prize categories, each with a significant cash
award. We awarded a $1000 prize in each of the two categories in 2010.
Each team that submits a complete and working entry will be invited to
submit for review a 2-page abstract for the formal conference
proceedings and present a poster at the conference; winning teams will
be invited to contribute a 4-page short paper and present their work
at the conference.  Each team submitting a completed and working entry
will also receive a commemorative plaque with their name and results.
Please refer to the website for more information and updates.

DESIGN CONTEST WEBSITE: see conference webpage



SPONSORS:

Microsoft Research Cambridge, IEEE CEDA*, IEEE CAS*, ACM SIGBED*, and
ACM SIGDA*



ORGANIZATION COMMITTEE:

General and Finance Chair:  Satnam Singh  (MSR Cambridge)
Program Chairs: Barbara Jobstmann (CNRS/Verimag)
Michael Kishinevsky (Intel)
Design Contest Chair:   Derek Chiou (UT Austin)
Publication Chair:  Jens Brandt (TU Kaiserslautern)