Moreno Falaschi | 23 Nov 13:33 2014
Picon

PPDP 2015 -- First call for papers

[Apologies for multiple copies]

============= First  Call for papers =========================================

		   17th International Symposium on
	  Principles and Practice of Declarative Programming
			      PPDP 2015

		    Siena, Italy, July 14-16, 2015
		    (co-located with LOPSTR 2015)

		  http://costa.ls.fi.upm.es/ppdp15
				   
======================================================================

		  SUBMISSION DEADLINE: 20 MARCH, 2015

PPDP  2015  is a  forum  that  brings  together researchers  from  the
declarative  programming communities, including  those working  in the
logic,  constraint  and  functional  programming paradigms,  but  also
embracing languages, database  languages, and knowledge representation
languages. The  goal is  to stimulate research  in the use  of logical
formalisms  and  methods  for  specifying, performing,  and  analyzing
computations,   including   mechanisms   for   mobility,   modularity,
concurrency,  object-orientation,  security,  verification and  static
analysis. Papers related to the use of declarative paradigms and tools
in industry and education are especially solicited. Topics of interest
include, but are not limited to

* Functional programming
(Continue reading)

Stefan Wehr | 20 Nov 17:37 2014
Picon

Call for Participation: BOB 2015 in Berlin

Hi everyone,

the BOB conference is taking place soon, featuring two Haskell related
tutorials!

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

BOB 2015 Conference

"What happens if we simply use what's best?"

January 23. 2015
Berlin, Germany

http://bobkonf.de/2015/

Program: http://bobkonf.de/2015/programm.html
Registration: http://bobkonf.de/2015/registration.html

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

BOB is the conference for developers, architects and decision-makers
to explore technologies beyond the mainstream in software development,
and to find the best tools available to software developers today.
Our goal is for all participants of BOB to return home with new
insights that enable them to improve their own software development
experiences.

The program features 14 talks and 8 tutorials on current topics:

(Continue reading)

Daniel Santa Cruz | 20 Nov 05:27 2014
Picon

Haskell Weekly News: Issue 312

Welcome to issue 312 of the HWN, an issue covering crowd-sourced bits
of information about Haskell from around the web. This issue covers
from October 26 to November 15, 2014

Quotes of the Week

   * barsoap: There's no place for half measures in overkill.

Top Reddit Stories

   * Category Theory for Programmers: The Preface
     Domain: bartoszmilewski.com, Score: 141, Comments: 68
     Original: [1] http://goo.gl/nTaVM5
     On Reddit: [2] http://goo.gl/9cnWqN

   * Idris 0.9.15 released: partial evaluator, uniqueness types, library cleanups, and fancier docs.
     Domain: idris-lang.org, Score: 111, Comments: 55
     Original: [3] http://goo.gl/nL9Ptr
     On Reddit: [4] http://goo.gl/mkHVEl

   * HaskForce - The Haskell Plugin for IntelliJ IDEA
     Domain: carymrobbins.github.io, Score: 104, Comments: 34
     Original: [5] http://goo.gl/Oa0jBA
     On Reddit: [6] http://goo.gl/W2jrFW

   * Haskell for all: How to desugar Haskell code
     Domain: haskellforall.com, Score: 97, Comments: 50
     Original: [7] http://goo.gl/1ZfiyP
     On Reddit: [8] http://goo.gl/hK3xTo

   * Functional programming and condescension
     Domain: superginbaby.wordpress.com, Score: 87, Comments: 147
     Original: [9] http://goo.gl/erVkNx
     On Reddit: [10] http://goo.gl/ncQcxX

   * Quick Reminder to be Courteous
     Domain: self.haskell, Score: 85, Comments: 39
     Original: [11] http://goo.gl/pmEODB
     On Reddit: [12] http://goo.gl/pmEODB

   * Category Theory Applied to Functional Programming
     Domain: eafit.edu.co, Score: 84, Comments: 14
     Original: [13] http://goo.gl/ax59vm
     On Reddit: [14] http://goo.gl/xZYksD

   * New Book - Game Programming in Haskell
     Domain: leanpub.com, Score: 84, Comments: 31
     Original: [15] http://goo.gl/hAqaaU
     On Reddit: [16] http://goo.gl/XePpcJ

   * "hasql" is up to 2x and 7x faster than "postgresql-simple" and "HDBC"
     Domain: nikita-volkov.github.io, Score: 72, Comments: 22
     Original: [17] http://goo.gl/YwU4OQ
     On Reddit: [18] http://goo.gl/fnfFAC

   * Typing Haskell in Haskell (markdownified with syntax highlighting and updated links)
     Domain: gist.github.com, Score: 68, Comments: 3
     Original: [19] http://goo.gl/U6Jnvr
     On Reddit: [20] http://goo.gl/QeLcak

   * Using Haskell at Work
     Domain: self.haskell, Score: 66, Comments: 66
     Original: [21] http://goo.gl/265kRm
     On Reddit: [22] http://goo.gl/265kRm

   * Category: The Essence of Composition (First section of the Category Theory for Programmers)
     Domain: bartoszmilewski.com, Score: 60, Comments: 37
     Original: [23] http://goo.gl/pdwr4X
     On Reddit: [24] http://goo.gl/AtYhI3

   * PureScript 0.6 released, plus new website
     Domain: github.com, Score: 55, Comments: 23
     Original: [25] http://goo.gl/TSuiEM
     On Reddit: [26] http://goo.gl/ZRBCHz

   * Tomatoes are a subtype of vegetables
     Domain: blog.ezyang.com, Score: 53, Comments: 58
     Original: [27] http://goo.gl/1evzHU
     On Reddit: [28] http://goo.gl/qiiwSS

   * The Guts of a Spineless Machine
     Domain: jozefg.bitbucket.org, Score: 49, Comments: 11
     Original: [29] http://goo.gl/KxW1iq
     On Reddit: [30] http://goo.gl/CNQbwk

   * A Large Scale Study of Programming Languages and Code Quality in Github
     Domain: macbeth.cs.ucdavis.edu, Score: 47, Comments: 48
     Original: [31] http://goo.gl/TEoSBV
     On Reddit: [32] http://goo.gl/18UfCM

   * ghci-ng - GHCi plus extra goodies
     Domain: github.com, Score: 45, Comments: 14
     Original: [33] http://goo.gl/g6VMiK
     On Reddit: [34] http://goo.gl/5Mg7n8

Top StackOverflow Questions

   * Haskell's type checker is allowing a very wrong type replacement, and the program still compiles
     votes: 68, answers: 2
     Read on SO: [35] http://goo.gl/ikcCmv

   * Subsumption in polymorphic types
     votes: 29, answers: 1
     Read on SO: [36] http://goo.gl/clKuju

   * Rewriting as a practical optimization technique in GHC: Is it really needed?
     votes: 23, answers: 3
     Read on SO: [37] http://goo.gl/MNNuhW

   * Is there an unsigned integer type that will warn about negative literals?
     votes: 21, answers: 1
     Read on SO: [38] http://goo.gl/SmRO3t

   * How can I make GHCI release memory
     votes: 19, answers: 1
     Read on SO: [39] http://goo.gl/U3qroZ

   * How much of Pascal's triangle does this evaluate?
     votes: 15, answers: 1
     Read on SO: [40] http://goo.gl/PsaQ3X

   * Why is super-compilation not implemented more prevalent?
     votes: 14, answers: 3
     Read on SO: [41] http://goo.gl/MFNsrE

Until next time,
[42]+Daniel Santa Cruz

References


_______________________________________________
Haskell mailing list
Haskell <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Jeremy Gibbons | 17 Nov 15:06 2014
Picon
Picon

Up to 15 fully-funded doctoral studentships in CS at Oxford

Dear all,

My department has just received a big award from Google, which will mostly be spent on DPhil student scholarships. The topic is open to anything the dept works in, but I would particularly welcome strong students in functional programming. Please pass this around to anyone you think might be interested, or ask me if you'd like to know more. Thanks!

   *

Following a generous donation by Google, the Department of Computer Science at the University of Oxford is delighted to invite applications for up to 15 fully-funded DPhil (Oxford'ss PhD) studentships tenable from 1st October 2015. 


The University of Oxford is consistently ranked amongst the very best Computer Science departments in the world, for both teaching and research. We are committed to attracting the world's most talented students and working with them to continue the success of the department.

The topics for the studentships are open, but should relate to the interests of one of the Department's research areas: Algorithms, Artificial Intelligence, Automated Verification, Computational Biology, Foundations, Logic & Structures, Information Systems, Machine Learning, Multi-Agent Systems, Programming Languages, Security, Semantics and Software Engineering.  We also encourage applications in cross disciplinary areas such as Linguistics, Biology, Medicine and Quantum Foundations & Quantum Computation.

The studentships are for three years and are open to students of any nationality.  Each studentship will cover university and college fees with a stipend of at least £13,863 per year. Applicants are normally expected to have, or be predicted to achieve, a first-class or a strong upper second-class grade in either (i) a four-year undergraduate degree (with integrated masters) in a relevant subject (or equivalent international qualifications), or (ii) a three-year BSc/BA degree followed by excellent (distinction) performance in a master's degree in a relevant subject.

Applicants must obtain the support of a potential supervisor in the Department prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications. Informal enquiries may be addressed to Julie.sheppard <at> cs.ox.ac.uk and for more information please see our webpages (http://www.cs.ox.ac.uk/).

Please apply online here  quoting 15-STUD-CS-01 in the studentship reference box:

Closing date for applications:  9th January 2015

Jeremy.Gibbons <at> cs.ox.ac.uk
Oxford University Department of Computer Science,
Wolfson Building, Parks Road, Oxford OX1 3QD, UK.
+44 1865 283521



_______________________________________________
Haskell mailing list
Haskell <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Aleksy Schubert | 10 Nov 22:53 2014
Picon
Picon

RDP 2015 Last Call for Workshops

[apologies for cross posting]

-----------------------------------------------------------------------
RDP 2015 Last Call for Workshops
(Rewriting, Deduction, and Programming, June-July 2015, Warsaw, Poland)
-----------------------------------------------------------------------

RDP 2015 is the eighth edition of the International Conference on
Rewriting, Deduction, and Programming, consisting of two main
conferences

* RTA (Rewriting Techniques and Applications)
* TLCA (Typed Lambda Calculi and Applications)

Previous RDPs were held in 2003 in Valencia (Spain), 2004 in Aachen
(Germany), 2005 in Nara (Japan), 2007 in Paris (France), 2009 in
Brasilia (Brasil), 2011 in Novi Sad (Serbia), 2013 in Eindhoven (The
Netherlands).

We solicit proposals for satellite workshops of RDP 2015 that are
related in topics to one or both of the RDP conferences.

We plan the workshops to proceed for up to 2 days (possibilities of
longer workshops should be discussed with the organisers). It is
tradition at RDP that attendance to workshops is open to participants
of parallel events, similar to the way FLoC workshops are run. There
will be one day (Sunday, June 28, 2015) reserved for workshops only,
however, it will also be possible to run workshops on the other days
in parallel to one of the main conferences.

RDP will provide the possibility to print workshop proceedings,
details of the procedure will be posted later by the local organising
committee. RDP will not be able to reimburse invited workshop speakers
for travel or living expenses, though it may be possible to waive part
of the registration fees for invited speakers. The priority of RDP
will be to keep registration fees for the conferences and workshops
low.

If you want to organise a workshop, please send the following
information to rdp15 <at> mimuw.edu.pl:

* Workshop title and description of the topic
* Names and affiliations of the organisers
* Pointers to descriptions of previous editions of the workshop, if any
* Proposed workshop duration (from one day to two days)
* Proposed format and agenda (for example, paper presentations,
   tutorials, demo sessions, etc.)
* Plans for invited speakers or special sessions (round-table
   discussion, tutorials, etc.)
* Estimate of the audience size
* Procedures for selecting papers and participants
* Plans for the publication of proceedings (informal proceedings
   distributed to participants, electronic journal, proceedings with
   separate selection process, etc.)
* Other potential organisational issues

IMPORTANT DATES

Submission of workshop proposals:   November 18, 2014 (Tuesday)
Notification date:                  November 26, 2014 (Wednesday)
Workshop dates:                     June 28-July 3, 2014 (Sunday-Friday)

CONTACT INFORMATION

Questions regarding workshop proposals should be sent to
rdp15 <at> mimuw.edu.pl.

RDP 2015 MAIN ORGANISER
Aleksy Schubert http://www.mimuw.edu.pl/~alx/
Faculty of Mathematics, Informatics and Mechanics
University of Warsaw
David Van Horn | 7 Nov 17:45 2014

ICFP 2015: Call for Papers

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

 20th ACM SIGPLAN International Conference on Functional Programming

 ICFP 2015

 Vancouver, Canada, August 31 - September 2, 2015

 http://www.icfpconference.org/icfp2015

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

Important Dates
~~~~~~~~~~~~~~~

   Submissions due:  Friday, February 27 2015, 23:59 UTC-11
   Author response:  Tuesday, April 21, 2015
                     through Thursday, 23 April, 2015
      Notification:  Friday, May 1, 2015
    Final copy due:  Friday, June 12, 2015

Scope
~~~~~

ICFP 2015 seeks original papers on the art and science of functional
programming.  Submissions are invited on all topics from principles to
practice, from foundations to features, and from abstraction to
application.  The scope includes all languages that encourage
functional programming, including both purely applicative and
imperative languages, as well as languages with objects, concurrency,
or parallelism.  Topics of interest include (but are not limited to):

* Language Design: concurrency, parallelism, and distribution; modules;
  components and composition; metaprogramming; type systems;
  interoperability; domain-specific languages; and relations to
  imperative, object-oriented, or logic programming.

* Implementation: abstract machines; virtual machines; interpretation;
  compilation; compile-time and run-time optimization; garbage
  collection and memory management; multi-threading; exploiting
  parallel hardware; interfaces to foreign functions, services,
  components, or low-level machine resources.

* Software-Development Techniques: algorithms and data structures;
  design patterns; specification; verification; validation; proof
  assistants; debugging; testing; tracing; profiling.

* Foundations: formal semantics; lambda calculus; rewriting; type
  theory; monads; continuations; control; state; effects; program
  verification; dependent types.

* Analysis and Transformation: control-flow; data-flow; abstract
  interpretation; partial evaluation; program calculation.

* Applications: symbolic computing; formal-methods tools; artificial
  intelligence; systems programming; distributed-systems and web
  programming; hardware design; databases; XML processing;
  scientific and numerical computing; graphical user interfaces;
  multimedia and 3D graphics programming; scripting; system
  administration; security.

* Education: teaching introductory programming; parallel programming;
  mathematical proof; algebra.

* Functional Pearls: elegant, instructive, and fun essays on
  functional programming.

* Experience Reports: short papers that provide evidence that
  functional programming really works or describe obstacles that have
  kept it from working.

If you are concerned about the appropriateness of some topic, do not
hesitate to contact the program chair.

Abbreviated instructions for authors
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* By Friday, 27 February 2015, 23:59 UTC-11 (anywhere in the world),
  submit a full paper of at most 12 pages (6 pages for an Experience
  Report) in standard ACM conference format, including bibliography,
  figures, and appendices.

The deadlines will be strictly enforced and papers exceeding the page
limits will be summarily rejected.

* Authors have the option to attach supplementary material to a submission,
  on the understanding that reviewers may choose not to look at it.

* Each submission must adhere to SIGPLAN's republication policy, as
  explained on the web at

      http://www.sigplan.org/Resources/Policies/Republication

* Authors of resubmitted (but previously rejected) papers have the
  option to attach an annotated copy of the reviews of their previous
  submission(s), explaining how they have addressed these previous
  reviews in the present submission.  If a reviewer identifies
  him/herself as a reviewer of this previous submission and wishes to
  see how his/her comments have been addressed, the program chair will
  communicate to this reviewer the annotated copy of his/her previous
  review.  Otherwise, no reviewer will read the annotated copies of
  the previous reviews.

Overall, a submission will be evaluated according to its relevance,
correctness, significance, originality, and clarity.  It should
explain its contributions in both general and technical terms, clearly
identifying what has been accomplished, explaining why it is
significant, and comparing it with previous work.  The technical
content should be accessible to a broad audience.  Functional Pearls
and Experience Reports are separate categories of papers that need not
report original research results and must be marked as such at the
time of submission.  Detailed guidelines on both categories are on the
conference web site.

Proceedings will be published by ACM Press.  Authors of accepted
submissions will have a choice of one of three ways to manage their
publication rights.  These choices are described at

    http://authors.acm.org/main.html

Presentations will be videotaped and released online if the presenter
consents.  The proceedings will be freely available for download from
the ACM Digital Library from one week before the start of the
conference until two weeks after the conference.

Formatting: Submissions must be in PDF format printable in black and
white on US Letter sized paper and interpretable by
Ghostscript. Papers must adhere to the standard ACM conference format:
two columns, nine-point font on a ten-point baseline, with columns
20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc
(0.33in).  A suitable document template for LaTeX is available at

    http://www.acm.org/sigs/sigplan/authorInformation.htm

Submission: Submissions will be accepted on the web using a link
that will be posted at

    http://icfpconference.org/icfp2015/

Improved versions of a paper may be submitted at any point before
the submission deadline using the same web interface.

Author response: Authors will have a 72-hour period, starting at 0:00
UTC on Tuesday, 21 April 2015, to read reviews and respond to them.

ACM Author-Izer is a unique service that enables ACM authors to
generate and post links on either their home page or institutional
repository for visitors to download the definitive version of their
articles from the ACM Digital Library at no charge. Downloads through
Author-Izer links are captured in official ACM statistics, improving
the accuracy of usage and impact measurements. Consistently linking
the definitive version of ACM article should reduce user confusion
over article versioning. After your article has been published and
assigned to your ACM Author Profile page, please visit

    http://www.acm.org/publications/acm-author-izer-service

to learn how to create your links for free downloads from the ACM DL.

Publication date: The official publication date of accepted papers
is the date the proceedings are made available in the ACM Digital
Library. This date may be up to two weeks prior to the first day
of the conference. The official publication date affects the deadline
for any patent filings related to published work.

General Chair:
  Kathleen Fisher        Tufts University (USA)

Program Chair:
  John Reppy            University of Chicago (USA)

Program Committee:
  Amal Ahmed                    Northeastern University (USA)
  Jean-Philippe Bernardy        Chalmers University of Technology (Sweden)
  Matthias Blume                Google (USA)
  William Byrd                  University of Utah (USA)
  Andy Gill                     University of Kansas (USA)
  Neal Glew                     Google (USA)
  Fritz Henglein                University of Copenhagen (Denmark)
  Gabriele Keller               University of New South Wales and
NICTA (Australia)
  Andrew Kennedy                Microsoft Research Cambridge (UK)
  Neelakantan Krishnaswami      Birmingham University (UK)
  Daan Leijen                   Microsoft Research Redmond (USA)
  Keiko Nakata                  Institute of Cybernetics at Tallinn
University of Technology (Estonia)
  Mike Rainey                   INRIA Rocquencourt (France)
  Andreas Rossberg              Google (Germany)
  Manuel Serrano                INRIA Sophia Antipolis (France)
  Simon Thompson                University of Kent (UK)
  David Van Horn                University of Maryland (USA)
  Stephanie Weirich             University of Pennsylvania (USA)
Klaus Havelund | 3 Nov 19:37 2014
Picon

NFM 2015 - deadline extension: Nov 18

CALL FOR PAPERS

*** Deadline extension: Nov 18, 2014 ***

The 7th NASA Formal Methods Symposium

http://www.NASAFormalMethods.org/nfm2015

27 – 29 April 2015
Pasadena, California, USA

THEME

The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.

TOPICS

Topics of interest include, but are not limited to:

  • Model checking
  • Theorem proving
  • SAT and SMT solving
  • Symbolic execution
  • Static analysis
  • Runtime verification
  • Program refinement
  • Compositional verification
  • Modeling and specification formalisms
  • Model-based development
  • Model-based testing
  • Requirement engineering
  • Formal approaches to fault tolerance
  • Security and intrusion detection
  • Applications of formal methods to aerospace systems
  • Applications of formal methods to cyber-physical systems
  • Applications of formal methods to human-machine interaction analysis

INVITED SPEAKERS

Dino Distefano
Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.

Viktor Kuncak
Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.

Rob Manning
Chief Engineer at NASA/JPL.

IMPORTANT DATES

Paper Submission (*** deadline extended one week ***): 18 Nov 2014
Paper Notifications: 12 Jan 2015
Camera-ready Papers: 9 Feb 2015
Symposium: 27 – 29 April 2015

LOCATION AND COST

The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.

SUBMISSION DETAILS

There are two categories of submissions:

  1. Regular papers describing fully developed work and complete results (15 pages)
  2. Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results (6 pages)

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer’s Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.

PC CHAIRS

Klaus Havelund, NASA Jet Propulsion Laboratory, USA
Gerard Holzmann, NASA Jet Propulsion Laboratory, USA
Rajeev Joshi, NASA Jet Propulsion Laboratory, USA

PUBLICITY SUPPORT

Ylies Falcone, Université Joseph Fourier, France

PROGRAMME COMMITTEE

Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Yvonne Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK

STEERING COMMITTEE

Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

_______________________________________________
Haskell mailing list
Haskell <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Hendrik Tews | 28 Oct 16:19 2014

Job announcement: formal methods engineer and scientific developer at FireEye

Dear all,

[My excuses if see this email more than once]

the FireEye R&D center in Dresden, Germany, seeks outstanding
formal-methods experts and scientific programmers to join
FireEye's formal methods team in Dresden, Germany. Applicants
should have a background in logical reasoning, (formal) software
verification and functional programming. Please visit
http://FireEye.com/careers for the concrete job descriptions.

If you are interested or have questions, please contact me or
Roland Carter <roland.carter <at> FireEye.com> or visit
http://FireEye.com for more information about FireEye.

FireEye is a next generation security company that provides the
industry's leading threat protection technology. The formal
methods team at FireEye works on the (formal) verification of a
non-trivial piece of the software stack of one of FireEye's
future products. Dresden is one the most beautiful cities in
Germany with unique cultural attractions. The FireEye office is
in the heart of the city, next to the famous historical center.

Bye,

Hendrik Tews

Formal Methods Engineering Manager at FireEye Germany
Head of FireEye Research & Development Dresden

phone: +49 351 8503 4745
WWW  : http://www.askra.de
This email and any attachments thereto may contain private, confidential, and/or privileged material
for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any
attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please
contact the sender immediately and permanently delete the original and any copies of this email and any
attachments thereto.
Klaus Havelund | 26 Oct 15:40 2014
Picon

NFM 2015 - final call for papers



CALL FOR PAPERS

The 7th NASA Formal Methods Symposium

http://www.NASAFormalMethods.org/nfm2015

27 – 29 April 2015
Pasadena, California, USA

Paper Submission: *** 10 Nov 2014 ***


THEME

The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.


TOPICS

Topics of interest include, but are not limited to:

Model checking
Theorem proving
SAT and SMT solving
Symbolic execution
Static analysis
Runtime verification
Program refinement
Compositional verification
Modeling and specification formalisms
Model-based development
Model-based testing
Requirement engineering
Formal approaches to fault tolerance
Security and intrusion detection
Applications of formal methods to aerospace systems
Applications of formal methods to cyber-physical systems
Applications of formal methods to human-machine interaction analysis


INVITED SPEAKERS

Dino Distefano
Software Engineer at Facebook, California, USA and Professor at Queen Mary University of London, UK.

Viktor Kuncak
Leads Lab for Automated Reasoning and Analysis at EPFL, Lausanne, Switzerland.

Rob Manning
Chief Engineer at NASA/JPL.


IMPORTANT DATES

Paper Submission: 10 Nov 2014
Paper Notifications: 12 Jan 2015
Camera-ready Papers: 9 Feb 2015
Symposium:   27 – 29 April 2015


LOCATION AND COST

The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.


SUBMISSION DETAILS

There are two categories of submissions:

- Regular papers describing fully developed work and complete results (15 pages)
- Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results  
 (6 pages)

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer’s Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.


PC CHAIRS

Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Rajeev Joshi, NASA Jet Propulsion Laboratory


PROGRAMME COMMITTEE

Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Yvonne Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK


STEERING COMMITTEE

Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

---
_______________________________________________
Haskell mailing list
Haskell <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Liu Yang (Asst Prof | 23 Oct 08:30 2014
Picon

Multiple Postdoc Positions on Formal Methods for Cyber Security

Title: Multiple Postdoc Positions on Formal Methods for Cyber Security http://www.ntu.edu.sg/home/yangliu/securify.html

Nanyang Technological University and
Singapore University of Technology and Design

Highly motivated applicants are sought to work on developing and applying verification techniques for
infinite state systems in the project on Building Security Verified System.
The project aims to fully verify the execution stack of a cyber-physical system:
i.e., hardware, operating system, system libraries and applications, using model checking and theorem
proving technologies.
The postdocs will work with the PAT formal methods research group (www.patroot.com) and other
researchers at NTU and SUTD in Singapore.

They will also have the opportunity to travel overseas to collaborate with partners of the project,
including ETH Zurich, Oxford University, Royal Holloway University of London, University of
Luxembourg, Hong Kong University of Science and Technology.

Positions for Research Fellow and Senior Research Fellow are available for the following topics:

1. Hardware Verification.
   The preferred candidates are those with experience in one or more of the following areas:
      - Formal methods, model checking, theorem proving.
      - Temporal logics, Higher order logic.
      - Functional programming.
      - Hardware design, especially SPARK/LEON architecture
    Contact: Liu Yang (yangliu <at> ntu.edu.sg), Alwen Tiu (atiu <at> ntu.edu.sg)

2. Microkernel Verification
   The preferred candidates are those with experience in one or more of the following areas:
      - Formal methods, theorem proving.
      - Temporal logics, Higher order logic.
      - Functional programming.
      - Operating System Design.
   Contact: Liu Yang (yangliu <at> ntu.edu.sg)

3. Software Model Checking for Security
   The preferred candidates are those with experience in one or more of the following areas:
      - Formal methods, model checking.
      - Temporal logics.
      - SMT solvers.
      - Formal languages and automata.
   Contact: Jun Sun (sunjun <at> sutd.edu.sg) and Yang Liu (yangliu <at> ntu.edu.sg)

4. Runtime security verification
   The preferred candidates are those with experience in one or more of the following areas:
            - Temporal and modal logics
            - First-order theorem proving
            - Runtime verification
            - Preferably also backgrounds in operating system and network security
   Contact: Alwen Tiu (atiu <at> ntu.edu.sg)

5. Compositional Verification of Security.
   The preferred candidates are those with experience in one or more of the following areas:
      - Formal methods, model checking.
      - Assume-Guarantee Reasoning.
      - Temporal Logics.
      - Formal languages and automata.

   Contact: Yang Liu (yangliu <at> ntu.edu.sg) and Jun Sun (sunjun <at> sutd.edu.sg)

6. System Security.
   The preferred candidates are those with experience in one or more of the following areas:
      - Binary security and analysis, especially LLVM.
      - Malware and vulnerabilities.
      - Mobile platform security.
      - Embedded system security.
      - Cloud security.

   Contact: Yang Liu (yangliu <at> ntu.edu.sg)

7. Secure Code Generation.
   The preferred candidates are those with experience in one or more of the following areas:
      - Formal methods, model checking, theorem proving.
      - Temporal logics, Higher order logic.
      - Model driven development.

   Contact: Yang Liu (yangliu <at> ntu.edu.sg)

The position involves conducting basic research, developing tools, working as part of a research team,
travelling, and giving presentations. The working language is English.

Apart from specific requirements to each topic candidate general requirements are:
- A PhD in Computer Science or related areas is required.
- Strong background in logic and discrete math.
- Strong programming skills.
- An established research record.

The term is currently one to three years starting as early as January 2015 till all positions are filled.
The salary range is 4000 SGD - 6000 SGD per month for Research Fellows and
6000 - 8000 SGD per month for Senior Research Fellows.
Yearly bonus is 1 to 3 month salary based on the performance.
Singapore's tax is around 3%-5% of the annual salary.
1USD = 1.25 SGD.

Candidates interested in a particular topic or topics should contact the contact person(s) listed in the
respective topics above for more details.

General inquiries can be directed at either Yang Liu, Jun Sun and Alwen Tiu.

________________________________
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or
privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or
disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Tom Schrijvers | 21 Oct 10:14 2014
Picon

Postdoc Position in Functional and Constraint Programming at KU Leuven

Postdoctoral position in Functional and Constraint Programming at KU Leuven

The Declarative Languages and Artificial Intelligence (DTAI) group of KU Leuven (Belgium) invites applicants for a postdoctoral position in the area of functional and constraint programming. The position revolves around domain-specific languages (DSLs) embedded in Haskell for constraint programming. It is part of the EU project GRACeFUL whose overarching theme is tools for collective decision making. The KU Leuven part of the project is under the direction of prof. Tom Schrijvers.

To apply you must hold a recent PhD (or be about to graduate) related to either functional or constraint programming. Experience in both areas is an advantage.

You will work closely with prof. Schrijvers and his PhD students at KU Leuven, as well as with the GRACeFUL project partners across Europe.

The position is for 3 years. The salary is competitive and the starting date negotiable (but no later than February 1). Moreover, KU Leuven's policy of equal opportunities and diversity applies to this position.




--
prof. dr. ir. Tom Schrijvers

Research Professor
KU Leuven
Department of Computer Science

Celestijnenlaan 200A
3001 Leuven
Belgium
Phone: +32 16 327 830
_______________________________________________
Haskell mailing list
Haskell <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Gmane