[TYPES/announce] Post-doctoral research position at Nancy University on ICC

2011-09-06 Thread Jean-Yves Marion
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Post-doctoral position at Nancy University, INRIA-LORIA, France

on Implicit computational complexity (ICC)

Applications are now invited for a postdoctoral position on ICC. Candidates are 
expected to  contribute to research within the ANR project COMPLICE. The ideal 
candidate will have interest on type systems, logics, and complexity. The 
position is for one year. The start date is negotiable.

To be considered for this position, please send a CV, list of publications, a 
brief statement of interest, and the names of two references to Jean-Yves 
Marion (jean-yves.mar...@loria.fr). Further inquiries--for example, questions 
about specific project topics--are also welcome.

COMPLICE is a four-year project whose partner sites are ENS Lyon, Université 
Paris 13 and LORIA-Nancy.  The project's goal is to investigate the foundations 
and applications of implicit computational complexity (ICC), along the lines of 
semantics and logic, functional programming, program extraction from proofs, 
quantitative properties and ICC for concurrent systems.

http://www.loria.fr/
http://en.inria.fr/inria-research-centre/nancy-grand-est
http://www-lipn.univ-paris13.fr/complice/spip.php?auteur2


[TYPES/announce] CFP: International Symposium on Engineering Secure Software and Systems (ESSoS) -- deadline approaching!

2011-09-06 Thread Pieter Philippaerts
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Online submission for papers is now available through EasyChair, at
http://www.easychair.org/conferences/?conf=essos12
Abstracts should be submitted before September 18th, and papers before
September 25th!


Call For Papers

International Symposium on Engineering Secure Software and Systems (ESSoS)

  http://distrinet.cs.kuleuven.be/events/essos2012/

  February 16 - 17, 2012, Eindhoven, The Netherlands
  
In cooperation with ACM SIGSAC and SIGSOFT and (pending) IEEE CS (TCSE).

CONTEXT AND MOTIVATION

Trustworthy, secure software is a core ingredient of the modern world.
Unfortunately, the Internet is too. Hostile, networked environments, like
the Internet, can allow vulnerabilities in software to be exploited from
anywhere.  To address this, high-quality security building blocks (e.g.,
cryptographic components) are necessary, but insufficient. Indeed, the
construction of secure software is challenging because of the complexity of
modern applications, the growing sophistication of security requirements,
the multitude of available software technologies and the progress of attack
vectors. Clearly, a strong need exists for engineering techniques that scale
well and that demonstrably improve the software's security properties.


GOAL AND SETUP

The goal of this symposium, which will be the fourth in the series, is to
bring together researchers and practitioners to advance the states of the
art and practice in secure software engineering. Being one of the few
conference-level events dedicated to this topic, it explicitly aims to
bridge the software engineering and security engineering communities, and
promote cross-fertilization. The symposium will feature two days of
technical program, and is also open to proposals for both tutorials and
workshops. In addition to academic papers, the symposium encourages
submission of high-quality, informative experience papers about successes
and failures in security software engineering and the lessons learned.
Furthermore, the symposium also accepts short idea papers that crisply
describe a promising direction, approach, or insight.


TOPICS 

The Symposium seeks submissions on subjects related to its goals. This
includes a diversity of topics including (but not limited to):

- scalable techniques for threat modeling and analysis of vulnerabilities
- specification and management of security requirements and policies
- security architecture and design for software and systems
- model checking for security
- specification formalisms for security artifacts
- verification techniques for security properties
- systematic support for security best practices
- security testing
- security assurance cases
- programming paradigms, models and DLS's for security
- program rewriting techniques
- processes for the development of secure software and systems
- security-oriented software reconfiguration and evolution
- security measurement
- automated development
- trade-off between security and other non-functional requirements
- support for assurance, certification and accreditation


SUBMISSION AND FORMAT The proceedings of the symposium are published by
Springer-Verlag in the Lecture Notes in Computer Science Series
(http://www.springer.com/lncs). Submissions should follow the formatting
instructions of Springer LNCS. Submitted papers must present original,
non-published work of high quality. Online submission for papers is
available through EasyChair, at
http://www.easychair.org/conferences/?conf=essos12

Two types of papers will be accepted: 

Full papers (max 12 pages without bibliography/appendices) - May describe
original technical research with a solid foundation, such as formal analysis
or experimental results, with acceptance determined mostly based on novelty
and validation. Or, may describe case studies applying existing techniques
or analysis methods in industrial settings, with acceptance determined
mostly by the general applicability of techniques and the completeness of
the technical presentation details.

Idea papers (max 8 pages with bibliography) - May crisply describe a novel
idea that is both feasible and interesting, where the idea may range from a
variant of an existing technique all the way to a vision for the future of
security technology. Idea papers allow authors to introduce ideas to the
field and get feedback, while allowing for later publication of complete,
fully-developed results. Submissions will be judged primarily on novelty,
excitement, and exposition, but feasibility is required, and acceptance will
be unlikely without some basic, principled validation (e.g., extrapolation
from limited experiments or simple formal analysis).

Proposals for both tutorials and workshops are welcome.

IMPORTANT DATES

Abstract submission: September 18, 2011
Paper submission:

[TYPES/announce] CFP: PLPV'12 - Programming languages meets program verification

2011-09-06 Thread Nikhil Swamy
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

   PLPV 2012
     The Sixth ACM SIGPLAN Workshop 
Programming Languages meets Program Verification 

24th January, 2012
Philadelphia, USA
(Affiliated with POPL 2012)
http://research.microsoft.com/en-us/um/people/nswamy/plpv12


Overview  

The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification, by
bringing together experts from diverse areas like types, contracts,
interactive theorem proving, model checking and program analysis. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic or structural
properties of the programming language. Examples include dependently
typed programming languages, which leverage a language's type system
to specify and check richer than usual specifications or extended
static checking systems which incorporate contracts with either static
or dynamic contract checking.

We invite submissions on all aspects, both theoretical and practical,
of the integration of programming language and program verification
technology. To encourage cross-pollination between different
communities, we seek a broad scope for PLPV.  In particular,
submissions may have diverse foundations for verification (Type-based,
Hoare-logic-based, Abstract Interpretation-based, etc.), target
different kinds of programming languages (functional, imperative,
object-oriented, etc.), and apply to diverse kinds of program
properties (data structure invariants, security properties, temporal
protocols, resource constraints, etc.).



Important Dates:

Submission:    11th October,  2011  
Notification:  8th November,  2011  
Final Version: 15th November, 2011  
Workshop:  24th January,  2012  


Submissions 

We seek submissions of up to 12 pages related to the above
topics---shorter submissions are also welcome. Submissions may
describe new work, propose new challenge problems for language-based
verification techniques, or present a known idea in an elegant way
(i.e., a pearl).

Submissions should be prepared with SIGPLAN two-column conference
format (http://www.sigplan.org/authorInformation.htm). Submitted
papers must adhere to the SIGPLAN republication policy
(http://www.sigplan.org/republicationpolicy.htm). Concurrent
submissions to other workshops, conferences, journals, or similar
forums of publication are not allowed.

To submit a paper, access the submission site at 
http://www.easychair.org/conferences/?conf=plpv2012.


Publication 

Accepted papers will be published by the ACM and will appear in the
ACM Digital library.


Program Committee 

Amal Ahmed    Northeastern University 
Lennart Augustsson    Standard Chartered
Koen Claessen Chalmers (co-chair) 
Martin Giese  University of Oslo 
Daniel Licata Carnegie Mellon University 
Peter Müller ETH Zurich 
Aleksandar Nanevski   IMDEA 
Matthieu Sozeau   INRIA 
Nikhil Swamy  Microsoft Research (co-chair) 
David Walker  Princeton University 
Dana Xu   INRIA 


Previous PLPVs: http://plpv.org