[TYPES/announce] VeTSS PhD School and FMATS, MSR Cambridge, September 24th-25th

[Gardner, Philippa A]

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

Hello everyone,

It is my pleasure to invite you to the 6th Workshop on Formal Methods and Tools 
for Security (FMATS), that will take place in Microsoft Research Cambridge, on 
24th-25th September, organised and supported by VeTSS, the UK Research 
Institute in Verified Trustworthy Software Systems, and Microsoft Research 
Cambridge. The goal of this workshop to bring together verification, systems 
and security experts interested in formal analysis, industrialists interested 
in software validation, and government scientists interested in reliable 
software systems, and to introduce them to the current generation of UK PhD 
students and postdocs.

The workshop will consist of two days of talks given from world-leading experts 
from academia (Cambridge, Imperial College London, Inria Paris, University 
College London, Purdue, etc.), industry (Adelard, Galois, Google, Data61, 
etc.), and funding bodies (NSF). The full programme is available 
HERE.

Registration is free of charge, with complimentary tea/coffee, lunches and a 
lovely dinner at Westminster College. You can find more information about the 
workshop and register 
HERE.
 The deadline for registration is September 20th.

We particularly encourage PhD students and postdocs to attend, as there will be 
plenty of opportunities to interact with  academics and industrialists from the 
UK and worldwide. There will be a poster session where they can present their 
work, and also a slot during the workshop itself for them to briefly introduce 
themselves to all of the participants. Finally, there’s a small number of 
travel grants available, for which they can apply via the above link.

Best wishes,
Philippa Gardner

[TYPES/announce] Postdoc opening at the University of Pennsylvania

[Benjamin C. Pierce]

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

The University of Pennsylvania's Accountable Protocol Customization (APC) 
project is a new multi-disciplinary effort funded by the Office of Naval 
Research (ONR) as part of its Total Platform Cyber Protection (TPCP) program. 
The goal is to develop tools and reasoning principles for protocol 
customization aimed at software de-bloating, by identifying lean protocol 
subsets that are sufficient to meet the functional and security needs of 
relevant clients and servers while preserving backward compatibility. 
Customization can also support protocol dialects that modify the original 
protocol standard in settings  where backward compatibility is not a strict 
requirement. A central project theme is ensuring that customization is 
“accountable” — i.e. carefully vetting properties of customized protocols by 
tightly coupling protocol customization operations with rigorous formal 
analysis and machine-checked proofs in the Coq proof assistant.  A particular 
target area is modern web protocols such as HTTP2 and TLS. 

Our APC project, in collaboration with Carnegie-Mellon University and Stanford 
University, brings together researchers with expertise in formal methods, 
programming languages, distributed systems, and network security. 

The APC team at Penn has funding for one post-doctoral researcher. This is a 
one-year position, based in Philadelphia, with the option of a second year 
subject to mutual agreement and funding availability. The postdoc will have the 
freedom to lead individual projects as well as working with a strong team of 
researchers including Ph.D., Masters, and undergraduate students.

We seek applicants with expertise in at least one, preferably two or more, of 
the following areas: formal methods, programming languages, distributed 
systems, and network security. Applicants should email their CV and a research 
statement to Dr. Boon Thau Loo (boon...@seas.upenn.edu 
) and also ask two or three references to email 
letters of recommendation to Dr. Loo.

For more information, please feel free to contact any of the APC Principal 
Investigators: 
Boon Thau Loo (boon...@seas.upenn.edu )
Benjamin C. Pierce (bcpie...@seas.upenn.edu)
Andre Scedrov (sced...@seas.upenn.edu)
Steve Zdancewic (ste...@seas.upenn.edu) 

[TYPES/announce] Open Engineer Position in ProofInUse joint laboratory

[Claude Marché]

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


  [Feel free to redistribute this announcement/Apologizes for multiple 
copies]


The Joint Laboratory ProofInUse (https://www.adacore.com/proofinuse) 
hires an experienced R engineer (M/F) in the domain of Formal Methods 
for Software Engineering:


 https://jobs.inria.fr/public/classic/en/offres/2018-01034

ProofInUse originates from the sharing of resources and knowledge 
between the Toccata research team (http://toccata.lri.fr/), specializing 
in techniques for deductive program verification and the SME AdaCore, a 
software publisher, specializing in providing software development tools 
for critical systems. The SME TrustInSoft (https://trust-in-soft.com/), 
specialized in advanced static analysis techniques for safety and 
security of C/C++ source code, recently joined the ProofInUse Laboratory.


The purpose of ProofInUse is to increase significantly the number of 
customers of the SPARK 2014 and the TrustInSoft Analyzer technologies, 
by popularizing the use of formal proof techniques. This popularization 
requires the resolution of several scientific and technological 
challenges. A first axis of work is to design and implement a new 
plug-in for deductive verification in the TrustInSoft Analyzer, making 
use of the Why3 intermediate (https://why3.lri.fr/) tool for 
verification condition generation, along the guidelines and design 
choices previously adopted for SPARK, that include strong restrictions 
on the analyzed code regarding the possibility of aliasing in data 
structures. This new plug-in must support new techniques for analyzing 
bit-level and floating-point codes, as well as new facilities for 
providing counterexamples when proofs fail. A second axis of work is to 
leverage the former non-aliasing restrictions, via an alias analysis 
based on a Rust-style sharing control and borrowing. A third axis is to 
actively participate to the development of a formally proved C/C++ 
software library.


The recruited engineer will work in close collaboration with the 
ProofInUse Research and Development team, to address both the scientific 
and the technological challenges presented above. It is expected that 
the engineer contributes both to advancing the academic knowledge in 
ProofInUse context and to the transfer of this knowledge into the 
software products distributed by AdaCore and TrustInSoft. The engineer 
will participate actively to the production of scientific publications, 
and to the software development of the Why3 tool and the TrustInSoft 
Analyzer.


We expect from the candidate some experience with Formal Methods for 
Software Engineering in a broad sense, typically the candidate should 
have defended a PhD in the domain of Formal Methods. More specifically, 
a plus would be some experience in formal logic and proof techniques, in 
automated deduction, in Satisfiability Modulo Theory solvers, in Model 
Checking or in Abstract Interpretation techniques.


The candidate should have a fair experience in software development, a 
plus would be the knowledge of functional programming, and the knowledge 
of the programming languages OCaml, C/C++ and/or Rust.


The candidate should be able to write and speak in English fluently.

The job will take place both on Toccata's lab site in building 650 of 
University Paris-Sud in Orsay, and at TrustInSoft's site in Paris, France.


The position is to be filled as soon as possible starting from Nov 1st 
2018, for a duration of 36 months.


Apply by sending a CV and a motivation letter to the e-mail contact 
addresses below, and/or via the URL given at the top of this message.


Contact/Information: claude.mar...@inria.fr, 
benjamin.mon...@trustinsoft.com, yannick@adacore.com