[TYPES/announce] CCC 2019; extended deadline

[Spreen, Dieter, Prof. Dr.]

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


Continuity, Computability, Constructivity – From Logic to Algorithms
 (CCC 2019)
 Ljubljana (Slovenia), 2-6 September 2019
Extended deadline
https://www.fmf.uni-lj.si/~simpson/ccc2019


CCC is a workshop series that brings together researchers applying logical 
methods to the development of algorithms, with a particular focus on 
computation with infinite data, where issues of continuity, computability and 
constructivity play major roles. Specific topics include exact real number 
computation, computable analysis, effective descriptive set theory, 
constructive analysis, and related areas. The overall aim is to apply logical 
methods in these disciplines to provide a sound foundation for obtaining exact 
and provably correct algorithms for computations with real numbers and other 
continuous data, which are of increasing importance in safety critical 
applications and scientific computation.

The workshop will take place in Ljubljana, Slovenia. Previous workshops have 
been held in Cologne 2009, Trier 2012, Gregynog 2013, Ljubljana 2014, Kochel 
2015, Nancy 2017, and Faro 2018.

The workshop is open to all participants.


Scope: The workshop specifically invites contributions in the areas of

  *   Exact real number computation,
  *   Correctness of algorithms on infinite data,
  *   Computable analysis,
  *   Complexity of real numbers, real-valued functions, etc.
  *   Effective descriptive set theory,
  *   Domain theory,
  *   Constructive analysis,
  *   Category-theoretic approaches to computation on infinite data,
  *   Weihrauch degrees,
  *   And related areas.

Invited Speakers:


  *   Hannes Diener (Christchurch, New Zealand)
  *   Fabian Immler (Pittsburgh, USA)
  *   Florian Steinberg (Paris, France)
  *   Thomas Streicher (Darmstadt, Germany)
  *   Holger Thies (Fukuoka, Japan)


Tutorial Speaker:


  *   Helmut Schwichtenberg (Munich, Germany)


Submission:

Extended abstracts (1-2 pages) of original work are welcome.


Deadline:
 15 July 2019

Upload your submission via EasyChair:

 https://easychair.org/conferences/?conf=ccc2019


Programme Committee:

  *   Francesco Ciraulo (Padua)
  *   Akitoshi Kawamura (Fukuoka)
  *   Alex Simpson (Ljubljana) (co-chair)
  *   Dieter Spreen (Siegen) (co-chair)
  *   Chuangjie Xu (Munich).

Organizing Committee:

  *   Alex Simpson (Ljubljana)
  *   Niels Voorneveld (Ljubljana)

[TYPES/announce] PhD Position in logic and formal verification

[Ana Borges]

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

The University of Barcelona offers a PhD position in collaboration with the
Catalan industrial sector. The industrial component of the PhD revolves
around the development and verification of legal software in Coq within
Formal Vindications SL (http://formalvindications.com/). This work will be
complemented with the formalization of parts of logic/mathematics. The
group where this project will be embedded works on ordinal analysis via
modal logic and reflection principles; we expect collaboration with the
main group to arise, but we are open to alternative proposals. The PhD
student will be part of a large and active research group. Currently, the
group is lead by Joost J. Joosten and consists of three researchers who
have over two years of experience with proof assistants, type-theory and
pure and applied proof theory. There are three fellow PhD students working
on related topics. Furthermore, the project counts with three junior
scientific staff members, a senior Coq developer and a versatile
programmer. The group is embedded into various research projects, including
European, National and Regional funds. The general logic landscape of the
Barcelona metropolitan area is rich and diverse and counts with groups and
specialists in areas like algebraic logic, computability theory, formal
linguistics, model theory, and set theory.

We offer a three-year position in the PhD program in Mathematics and
Computer Science which is located in the very center of Barcelona. If after
three years the PhD has not been finished, but there is realistic
expectations that it will be finished soon, the company will consider
continuing the position in its major characteristics. Apart from the usual
PhD trajectory, the candidates will participate in cutting edge
formalization developments in an industrial setting. The travel allowances
can exceed 2200€ per year and the gross salary varies between 18K and 22K
per year depending on how much financial support this project receives from
the Catalan authorities.

We are looking for candidates with a background in theoretical computer
science and/or mathematical logic. It is a strict requirement to have
finished a relevant Master with an average undergraduate and master score
of at least 6.5 out of 10. Apart from the required knowledge of Coq and
Ocaml, other IT skills are recommended, especially knowledge/experience
with other functional programming languages. Previous commercial work
experience is a plus and working proficiency in English is a must.

Interested candidates should make their first statement of interest through
the official AGAUR site, where they can fill in a pre-application. A direct
link to it is:
http://doctoratsindustrials.gencat.cat/files/file/attachment/7019/072_DI_FV_UB_PE6_PE1_20190701.pdf


After a first selection, candidates will be asked to file their application
package no later than September 5. The application package should contain:

(+) CV;
(+) Motivation letter;
(+) Transcript of obtained academic results in the relevant master and
undergraduate;
(+) Email addresses of three references to whom we might refer in case we
consider this desirable.

Further information about the position can be obtained by writing an email
to Aleix Solé at vacanc...@formalvindications.com.

[TYPES/announce] [TAPAS 2019] 2nd Call for Papers (extended deadline): 10th Workshop on Tools for Automatic Program Analysis

[David Delmas]

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


*[apologies for crossposting]*

online version: https://easychair.org/cfp/tapas2019




   10th Workshop on Tools for Automatic Program Analysis (TAPAS 2019)

8 October 2019, Porto, Portugal.

A satellite workshop of SAS 2019 . 
Part of the 3rd World Congress on Formal Methods 
.



   Important Dates

 * Submission deadline: 4 July *18 **July2019(extended)*
 * Notification of acceptance: 2 August *15August*
 * Final version due: 31 August *8 September*
 * Workshop: 8 October
 * Post-proceedings due: 15 November (tentative)


   Publication

Revised versions of selected papers will be published after the workshop 
by Springer in a volume of its Lecture Notes in Computer Science (LNCS) 
, which will collect contributions to some 
workshops and symposia co-located with FM 2019 
.


The workshop will also have informal proceedings, posted on its web page.


   Objectives

In recent years, a wide range of static analysis tools have emerged, 
some of which are currently in industrial use or are well beyond the 
advanced prototype level. Many impressive practical results have been 
obtained, which allow complex properties to be proven or checked in a 
fully or semi-automatic way, even in the context of complex software 
developments. In parallel, the techniques to design and implement static 
analysis tools have improved significantly, and much effort is being put 
into engineering the tools.


This workshop is intended to promote discussions and exchange experience 
between users of static analysis tools and specialists in all areas of 
program analysis design and implementation.



   Scope

The technical program of TAPAS 2019 
 will consist of invited lectures, 
together with presentations based on submitted papers or abstracts.


Submissions can cover any aspect of program analysis tools including, 
but not limited to the following:


 * design and implementation of static analysis tools (including
   practical techniques used for obtaining precision and performance)
 * components of static analysis tools (front-ends, abstract domains, etc.)
 * integration of static analyzers (in proof assistants, test
   generation tools, IDEs, etc.)
 * reusable software infrastructure (analysis algorithms and frameworks)
 * experience reports on the use of static analyzers (both research
   prototypes and industrial tools)

This workshop welcomes work in progress, overviews of more extensive 
work, programmatic or position papers and tool presentations.



   Submission Guidelines

TAPAS 2019  welcomes the following 
categories of submissions:


 * Regular papers (12-15+ pages)
 * Short papers (6-8+ pages)
 * Extended abstracts (2 pages)

Please use the LNCS style 
, 
and submit via the TAPAS 2019 author interface of EasyChair 
.



   Program Committee

 * David Delmas , Airbus and Sorbonne
   Université, France (chair)
 * Fausto Spoto , Università di
   Verona, Italy
 * Caterina Urban , Inria, France
 * Franck Vedrine, CEA LIST, France
 * Jules Villard , Facebook, UK
 * Jingling Xue , University of
   New South Wales, Australia
 * Tomofumi Yuki , Inria,
   France
 * Sarah Zennou, Airbus, France

[TYPES/announce] UNSW Sydney Seeking a Postdoc in Programming Languages and Verification

[Christine Rizkallah]

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

If only there were a place where I could prove theorems, change the world, and 
have
fun while doing it...

Sounds too good to exist?

In the Trustworthy Systems team at UNSW and Data61 that's what we do for a 
living. We
are the creators of seL4, the world's first fully formally verified operating 
system
kernel with extreme performance and strong security & correctness proofs. Our 
highly
international team is located on the UNSW campus, close to the beautiful 
beaches of
sunny Sydney, Australia, one of the world's most liveable cities.

We are offering a two-year postdoctoral researcher position that would allow 
you to join
us in Sydney, move things forward, and have a global impact.

Cogent is a language we designed that co-generates code and proofs in order to 
ease
the verification of systems components around seL4. Potential topics include 
designing
and implementing new domain-specific programming languages extending Cogent, 
writing
formal specifications and proofs in Isabelle/HOL, developing formally verified
infrastructure for building secure systems on top of seL4, contributing to 
improved
proof automation and reasoning techniques, and applying formal proof to 
real-world
systems and tools.

To apply you should have (or be about to obtain) a PhD degree in Computer 
Science,
Mathematics, or similar.

You should also possess a significant subset of the following skills:
- functional programming in a language like Haskell, ML, or OCaml
- first-order or higher-order formal logic
- basic experience in C
- ability and desire to quickly learn new techniques
- ability and desire to work in a larger team

If you additionally have experience

- in software verification with an interactive theorem prover such as
  Isabelle/HOL, HOL4, Coq, or Agda, and/or
- with programming languages and verified or certifying compilers

you should definitely apply!


You will work with a unique world-leading combination of OS and formal methods
experts, students at undergraduate and PhD level, engineers, and researchers 
from
5 continents, speaking over 15 languages.

Trustworthy Systems is a fun, creative, and welcoming workplace with flexible
hours & work arrangements.

We value diversity in all forms and welcome applications from people of all 
ages,
including people with disabilities, and those who identify as LGBTIQ. See
https://ts.data61.csiro.au/diversity/  
for more information.


For applying, use the following link:
http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fellow-computer-programming
 


-Salary range depending on experience and qualifications: 
  $95,449 - $102,091 (AUD) + 17% superannuation (retirement funds)
- 2-year fixed term contract
- the start date is negotiable
- flexible hours and work arrangements

This round of applications closes on the 13th of July 2019, 11:50pm AEST.


For any questions on this position, please contact Christine Rizkallah 
mailto:c.rizkal...@unsw.edu.au>>

The seL4 code and proof, and the Cogent project, are open source.
Check them out at https://seL4.systems  and 
https://ts.data61.csiro.au/projects/TS/cogent.pml 


More information about the Trustworthy Systems team at
https://ts.data61.csiro.au 

Still studying? We also have internship opportunities!
https://ts.data61.csiro.au/students/ 

smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Postdoc position at National University of Singapore on Program Synthesis

[Sergey, Ilya]

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

Hello all,

I invite candidates for a postdoc position, which is available in my group at 
Yale-NUS College and School of Computing of National University of Singapore. 
The position is for two years, funded by Singapore MOE Tier 1 grant "Scalable 
Deductive Synthesis of Thread-Safe Concurrency".

As the project name implies, we will be working on synthesising 
correct-by-construction concurrent programs. I am looking for motivated 
candidates with a strong, internationally competitive research track record. 
Particularly relevant is research expertise in:
- formal verification using program logics
- concurrent programming and concurrent data structures
- SMT and decision procedures

A tentative starting date is 1 October 2019, but the appointment can start 
earlier if the position is filled. The successful candidate is expected to work 
with me and external collaborators (specifically, Prof. Nadia Polikarpova from 
UC San Diego), as well as to help advising students and interns on the project 
topic, but can also allocate some part of their time for the projects of their 
interest.

The NUS School of Computing is one of the world-leading departments in the 
areas of programming languages, software engineering, distributed systems, 
security and privacy. It provides a diverse and welcoming environment, and the 
researchers from different groups at SoC frequently collaborate on joint 
projects of mutual interest.

Official advert: https://www.yale-nus.edu.sg/careers/postdoctoral-fellow-2/

Do not hesitate to get in touch with me if you are interested!

Kind regards,
Ilya




Important: This email is confidential and may be privileged. If you are not the 
intended recipient, please delete it and notify us immediately; you should not 
copy or use it for any purpose, nor disclose its contents to any other person. 
Thank you.