[TYPES/announce] Postdoc Position in Formal Verification of Cyber-Physical Systems

2024-03-25 Thread Hazem Torfah
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The group for Safe and Trustworthy Autonomous Reasoning at Chalmers University 
is looking for candidates interested in conducting independent research in the 
area of formal analysis of autonomous cyber-physical systems (ACPS). The 
candidate will work on developing a new generation of design and verification 
techniques, rooted in formal methods, to enable and support the development of 
assured ACPS. Topics of interest are (but are not limited to): compositional 
contract-based design, specification formalism for expressing properties of 
ACPS, statistical verification, and runtime verification under uncertainty.

This position is funded by the Wallenberg AI, Autonomous Systems, and Software 
Program (WASP 
https://urldefense.com/v3/__https://wasp-sweden.org/__;!!IBzWLUs!SFoj_UDcs-9bO1QusW4oue17NGOr7VteYUBZDlGkNur53j6-BZmV8AHjbDzdWJQPB6H5sFIwAX_pwCEtRw8EgZVk2Jnbinv8vw$
 ). WASP is Sweden’s largest individual research program and provides unique 
opportunities for achieving international research excellence with industrial 
relevance.

More information can be found under the following link: 
https://urldefense.com/v3/__https://www.chalmers.se/en/about-chalmers/work-with-us/vacancies/?rmpage=job=11984=UK__;!!IBzWLUs!SFoj_UDcs-9bO1QusW4oue17NGOr7VteYUBZDlGkNur53j6-BZmV8AHjbDzdWJQPB6H5sFIwAX_pwCEtRw8EgZVk2Jmmntkfew$
 


--
Hazem Torfah
Assistant Professor
Computing Science Division
Chalmers University of Technology
EDIT building | Floor 6V Office 6476
412 96 Gothenburg, Sweden
haze...@chalmers.se




[TYPES/announce] Postdoc position at the University of Strathclyde

2024-03-14 Thread Fredrik Nordvall Forsberg

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

Dear colleagues,

We are looking to recruit a postdoctoral researcher to work with us at 
the University of Strathclyde (Glasgow, Scotland) on our EPSRC grant 
EP/Y000455/1 A Correct-by-Construction Approach to Approximate 
Computation. This research is aiming at combining techniques from 
logics, model theory, type theory, category theory, continuous 
mathematics and AI for developing the foundations of approximate 
(quantitative) computation and apply this to programming and learning 
paradigms.


More details about the project can be found here:
https://urldefense.com/v3/__https://personal.cis.strath.ac.uk/r.mardare/projects.htm__;!!IBzWLUs!RiokSpppU_An_WT-q1sU4VeHGIUbiaiyEwEkL4k3JUTsxTpIBL9CGx61Y1mgdZ_G90eiNonQTbi566W3D3b6i89xxk5c2ONiGqLcJH3qYi0s0A$ 


The call for this position, with a deadline of 31 March, can be found here:
https://urldefense.com/v3/__https://strathvacancies.engageats.co.uk/Vacancies/W/5820/0/421067/15019/research-fellow-599328__;!!IBzWLUs!RiokSpppU_An_WT-q1sU4VeHGIUbiaiyEwEkL4k3JUTsxTpIBL9CGx61Y1mgdZ_G90eiNonQTbi566W3D3b6i89xxk5c2ONiGqLcJH1il_zxuw$ 


Kind regards,
Radu Mardare
Neil Ghani
Fredrik Nordvall Forsberg



[TYPES/announce] Postdoc position, Logic and Semantics Group in Tallinn

2023-08-11 Thread Tarmo Uustalu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Logic and Semantics Group at the Tallinn University of Technology
is seeking an aspiring talented and hard-working young scientist to
fill a departmentally funded postdoc position.

The group, currently consisting of 7 faculty and 4 PhD students,
specializes in functional programming, type theory, mathematical
semantics of programming languages, proof theory, constructive
mathematics, proof assistants, formalization of mathematics and
programming theory. Consult our webpage to get a picture of our work.

https://urldefense.com/v3/__https://cs.ioc.ee/lsg/__;!!IBzWLUs!WvwWcJ7pmSBbYocQxBbSvQBpUPrxujXbY28Vi3aRN_v5evMvqbk9dnOECnljtQQrPGhftW9J66utiw4BP9t5ppj_ga6e$
 

The group belongs to the High-Assurance Software Lab of the Department
of Software Science at the School of IT.

https://urldefense.com/v3/__https://cs.taltech.ee/__;!!IBzWLUs!WvwWcJ7pmSBbYocQxBbSvQBpUPrxujXbY28Vi3aRN_v5evMvqbk9dnOECnljtQQrPGhftW9J66utiw4BP9t5pl8fJYct$
 

The position is for 2 years; the start date is negotiable, preferrably
between 1 Nov 2023 and 1 Feb 2024.

The monthly gross salary will be 2500-3200 EUR depending on the
previous experience of the successful candidate. The deal includes
coverage by the national health insurance system, a paid annual leave
etc. A salary rate like this ensures a high standard of living in
Estonia.

Send your statement of purpose (cover letter), CV and research
statement to Tarmo Uustalu, ta...@cs.ioc.ee, and Niccolò Veltri,
nicc...@cs.ioc.ee, as soon as possible, but latest by 10 September
2023. We will assess applications as they arrive. With questions about
the research topics of the group, the research environment, the
conditions of the contract or living in Estonia, do not hesitate to
ask.


[TYPES/announce] Postdoc position in SE/PL for AI (modular deep learning, robust AI)

2023-06-24 Thread Rajan, Hridesh [COM S]
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoctoral position in SE/PL for AI
(Focus on modular deep learning, robust/dependable AI)

Iowa State University's Department of Computer Science is seeking applications 
for a postdoctoral position in the Laboratory for Software Design 
(https://urldefense.com/v3/__https://design.cs.iastate.edu__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBfB6w4Qwg$
 ). This two-year position, which may begin as early as July 2023, involves 
conducting research in the areas of Programming Languages (PL) and Software 
Engineering (SE), with a specific emphasis on SE/PL techniques for AI/ML 
systems. Our recent research has focused on decomposing deep learning models 
into modules for reuse and replacement [1-3] and on more modular techniques for 
verifying/reasoning about properties of deep learning models [4-5].

The successful candidate will contribute to the ongoing modular deep learning 
and Dependable Data Driven Discovery (D4) projects, aimed at improving the 
trustworthiness and quality of AI-enabled systems. The role includes creating 
and maintaining a robust research program, developing collaborative research, 
publishing in top-tier venues, mentoring graduate students, and contributing to 
ISU's professional and institutional service. Candidates with a background in 
SE/PL for AI/ML systems will be given preference.

The role also offers the chance to contribute to both undergraduate and 
graduate education. To apply 
https://urldefense.com/v3/__https://isu.wd1.myworkdayjobs.com/IowaStateJobs/job/Ames-IA/Postdoc-Research-Associate---Computer-Science_R12072__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBc8cqmGyA$
 . The guaranteed consideration date is July 16, 2023.

Could you please assist by sharing this information with potential candidates 
you deem suitable for the position? Thanks for your help. 

Best wishes,
Hridesh
 
Dr. Hridesh Rajan
Kingland Professor and Department Chair
Department of Computer Science
Iowa State University of Science and Technology
https://urldefense.com/v3/__https://www.cs.iastate.edu/hridesh__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBf9JY5hvw$
  

[1] Rangeet Pan, and Hridesh Rajan, "On Decomposing a Deep Neural Network into 
Modules," ESEC/FSE’2020: The 28th ACM Joint European Software Engineering 
Conference and Symposium on the Foundations of Software Engineering (Nov. 
2020). 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ESEC-FSE-20b/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBfbufF5EA$
 

[2] Rangeet Pan and Hridesh Rajan, "Decomposing Convolutional Neural Networks 
into Reusable and Replaceable Modules," ICSE’22: The 44th International 
Conference on Software Engineering (May 2022). 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ICSE-22b/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBerO0vUBA$
 

[3] Sayem Mohammad Imtiaz, Fraol Batole, Astha Singh, Rangeet Pan, Breno Dantas 
Cruz, and Hridesh Rajan, "Decomposing a Recurrent Neural Network into Modules 
for Enabling Reusability and Replacement," ICSE’23: The 45th International 
Conference on Software Engineering, May, 2023. 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ICSE-23b/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBf3QL6GAg$
 

[4] Sumon Biswas and Hridesh Rajan, "Fairify: Fairness Verification of Neural 
Networks," ICSE’23: The 45th International Conference on Software Engineering, 
May, 2023. 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ICSE-23a/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBcF8ZQ54g$
 

[5] Usman Gohar, Sumon Biswas, and Hridesh Rajan, "Towards Understanding 
Fairness and its Composition in Ensemble Machine Learning," ICSE’23: The 45th 
International Conference on Software Engineering, May, 2023. 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ICSE-23c/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBdnoe5Tvg$
 

[6] Sumon Biswas and Hridesh Rajan, "Fair Preprocessing: Towards Understanding 
Compositional Fairness of Data Transformers in Machine Learning Pipeline," 
ESEC/FSE’2021: The 29th ACM Joint European Software Engineering Conference and 
Symposium on the Foundations of Software Engineering, August, 2021. 
https://urldefense.com/v3/__https://design.cs.iastate.edu/papers/ESEC-FSE-21/__;!!IBzWLUs!Vh535WVrdds45NJ40T-N-iFY63U2H66s_7tHBMKoNPlNYFydl_0lOXzs4bxdO-Z9Lu2zmuIXiCPBQhKeawxHUUr5aBcMUFcCtA$
 



[TYPES/announce] Postdoc position in automata and concurrency theory at the University of Warsaw

2023-05-18 Thread Sławomir Lasota
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We invite applications of motivated and research-focused individuals to
carry out research on mathematical models of concurrent systems as part
of the NCN project "Frontiers of automatic analysis of concurrent systems".
The project aims at advancing theoretical foundations at the borderline
between automata theory, concurrency and formal verification.

The successful candidate will be hosted by the automata theory group
at the University of Warsaw, offering:

- a vibrant working atmosphere,
- exciting and challenging research problems,
- competitive salary,
- collaborations worldwide.

**
- Application deadline: May 25, 2023
- Starting date: flexible
- Duration: one year, possible extension to another year
- Principal investigator: Slawomir Lasota  
(https://urldefense.com/v3/__http://www.mimuw.edu.pl/*sl__;fg!!IBzWLUs!S4XLjs3gkFcYkQ3PSrdNZaHGAp4ZtdvOy0saU95hcu5Y23A8l_anoTyRGRYHrXRj_2nqYyeOktcv08Hmc7VT-PQlTbKSPNWbYQ$
 )
- Contact: s...@mimuw.edu.pl
**

The ideal candidate is expected to have:

- PhD degree or equivalent in computer science or math
- solid background in formal methods or automata theory
- excellent publication record
- strong motivation for research work in foundations of computer science
- advanced skills in written and spoken English.

For details of application and recruitment procedure, please contact
Sławomir Lasota at s...@mimuw.edu.pl


[TYPES/announce] Postdoc position on design and/or verification of distributed systems at the University of Birmingham, UK

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

Dear all,

We would like to invite applications for an up to 3 years fully-funded
postdoctoral position within the School of Computer Science at the
University of Birmingham (see below for details on how to apply).

The successful candidate will contribute to an EPSRC-funded project aiming
at designing and formally verifying distributed systems, in particular
Byzantine fault-tolerant distributed systems as used for example in
blockchain technology.

The environment:


The School of Computer Science has large and thriving Theory and Security
research groups. Among our research interests related to this project are
for example:
   - Formal verification
   - Proof assistants
   - Model checking
   - Blockchain Technology
   - Security & Privacy

Both groups are very active, organising regular seminars, informal
meetings, and actively participating in many events such as the Midlands
Graduate School or the Cyber Security PhD Winter School. For more
information see
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3Xr3nfQpA$
 
and
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/centre-for-cyber-security-and-privacy/index.aspx__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3XSKLSctQ$
 
.

How to apply:
-

Interested people are encouraged to contact me by email (v.ra...@bham.ac.uk)
to discuss their research interests and details of the positions. Further
information on how to apply is available here:
https://urldefense.com/v3/__https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/521/?utm_medium=jobshare__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3U_X8mBgg$
 

Best,
Vincent Rahli

-- 
https://urldefense.com/v3/__https://vrahli.github.io/__;!!IBzWLUs!Wt5sZQhaDkOtNQgCh84c3HnWmTFwBYXaMToH36fe2RrEyJoMM-Y8h6n1Z8NaxCalsb-Lepu_Rc4fhLrFfUwEmYt79-kMO3Xx2mKSMg$
 


[TYPES/announce] Postdoc position on Formal Verification for Zero-Trust IoT Systems at Kyoto University

2023-03-01 Thread Atsushi Igarashi
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are seeking a postdoc researcher, who works at Kyoto University,
Japan for a project "Zero-Trust IoT Systems by Collaboration of Formal
Verification and System Software" by Japan Science and Technology
Agency.  This is a great opportunity for programming language
researchers who wish to pursue novel real-world applications.

We'd appreciate you spreading the word to interested candidates.


* Project Description

The project aims at the construction of formally verified secure IoT
systems that follow the concept of "zero trust architecture", dubbed
ZT-IoT systems.  It consists of four research teams, and one of the
teams is led by Atsushi Igarashi, Kyoto University, investigating
applications of formal verification or programming language techniques
to the construction of secure IoT systems: more concretely, the design
and theory of security policy engines for ZT-IoT systems, including
the design of a language to describe security policies and policy
enforcement algorithms and the techniques for verifying policy
enforcement algorithms against given security policies.  Other team
members are Kohei Suenaga and Masaki Waga at Kyoto University.  
The team closely collaborates with another team, led by Taro Sekiyama,
National Institute of Informatics, Japan (NII), together with Ichiro
Hasuo and Shin-ya Katsumata at NII.

The appointment can start as early as May 2023 (the starting date is
negotiable).  The contract will initially run until the end of March
2024, with the possibility of annual renewal until the end of the
project, which is March 2027 at maximum.  The salary will be about
360,000–550,000 JPY/month.

Applicants should have a Ph.D. in computer science or related fields, and
have a strong background in formal verification and/or programming
language theory.  Due to the project's nature, they are required to have
strong interests in applying theory to practice; they should also be
(self-)motivated, dedicated, and able to work both independently and
collaboratively.  Strong communication skills in oral and written English
are required.


* Workplace

Kyoto University, Kyoto, Japan.

(Living costs in Japan are not very high nowadays.  An estimate is found here
https://urldefense.com/v3/__https://www.numbeo.com/cost-of-living/in/Kyoto__;!!IBzWLUs!RZqosDtp4fKwCflk3IWqWczBNvdhApfQEp9FN69OPcnJVccw86R-k5hllnI5Ae1xdn3s9q60aTOFQAZKrDSWTKF7qN6L5FPagwEO4XIgOg$
 .)


* Applications and inquiries

Inquiries can be sent to application-zt-iot [at] fos.kuis.kyoto-u.ac.jp,
with the subject CREST Job Inquiry.  Feel free to ask us any questions on
relevance, topics, compensation, etc.  We will reply when we see enough
relevance.

Applications should be made electronically via the following JREC-IN
Portal websites.

https://urldefense.com/v3/__https://jrecin.jst.go.jp/seek/SeekJorDetail?fn=3=D123010461_jor=0__;!!IBzWLUs!RZqosDtp4fKwCflk3IWqWczBNvdhApfQEp9FN69OPcnJVccw86R-k5hllnI5Ae1xdn3s9q60aTOFQAZKrDSWTKF7qN6L5FPagwFcTzOomw$
 


Please upload a pdf, including

- your brief CV,
- short description of research interests (can be very informal and short),
- the list of papers (a dblp or Google scholar link will do, for example),
- a couple of representative papers (in pdf), and
- (preferably) the contact of two references.

We will contact you for further material and an interview, provided that we
find sufficient relevance in your application.  Starting dates are
negotiable.  The positions will remain open until filled.

Best,
Atsushi Igarashi


[TYPES/announce] Postdoc position at Kyoto University, Japan

2023-03-01 Thread Kohei SUENAGA
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

(Sorry for cross posting.)

We are currently looking for a postdoctoral researcher to work on the
"CyPhAI: Formal Analysis and Design of AI-intensive Cyber-Physical
Systems" project funded by JST in Kyoto, Japan. The successful
candidate will be collaborating with us on establishing
mathematically-solid methodologies to model, verify, test, monitor,
and control a cyber-physical system in which AI plays a crucial role.
This project involves working closely with a team in Tokyo led by
Masako Kishida (NII) and a team in France led by Thao Dang (CNRS). The
detail of the call can be found here:
https://urldefense.com/v3/__https://www.kyoto-u.ac.jp/sites/default/files/acceptance_teacher/2023-02/20230208_0858_e-f67e82e5e49b6b9c49c3eaa70e2bf5a4.pdf__;!!IBzWLUs!QUeqOFxyvhc7vUCd7LIHTzOlABQ_46gYcaOkpZMuhj-QQX640MmDSOPIO21A6zJgJj_PvuWQBEY9pxWg43oNabB5iq8IlJ9uiv4BZgszbuEUkg$
 

The expected research topics include testing and verifying AI-CPS
using machine learning [3,6,7], secure monitoring techniques using
homomorphic encryption [5], application of model checking and program
logics for AI-CPS [2,4], and interpretability of machine-learned
components AI-CPS [1,8], among others.

The initial contract will run until the end of March 2024, with the
possibility of annual renewal at maximum until March 2026. We welcome
researchers on topics not listed above. If you are interested in this
position, please follow the link to the detailed call for applications
provided below. If you have any questions, please don't hesitate to
contact us!

[1] Yuhki Hatakeyama, Hiroki Sakuma, Yoshinori Konishi, Kohei Suenaga:
Visualizing Color-Wise Saliency of Black-Box Image Classification
Models. ACCV (3) 2020: 189-205
[2] Kohei Suenaga, Takuya Ishizawa:
Generalized Property-Directed Reachability for Hybrid Systems. VMCAI
2020: 293-313
[3] Junya Shijubo, Masaki Waga, Kohei Suenaga:
Efficient Black-Box Checking via Model Checking with Strengthened
Specifications. RV 2021: 100-120
[4] Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga:
Formalizing Statistical Beliefs in Hypothesis Testing Using Program
Logic. KR 2021: 411-421
[5] Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki
Waga, Kohei Suenaga:
Oblivious Online Monitoring for Safety LTL Specification via Fully
Homomorphic Encryption. CAV (1) 2022: 447-468
[6] Amit Gurung, Masaki Waga, Kohei Suenaga:
Learning nonlinear hybrid automata from input-output time-series data.
CoRR abs/2301.03915 (2023)
[7] Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert, Stefan
Klikovits, Toru Takisaka, Ichiro Hasuo:
Dynamic Shielding for Reinforcement Learning in Black-Box
Environments. ATVA 2022: 25-41
[8] Atsushi Kikuchi, Kotaro Uchida, Masaki Waga, Kohei Suenaga:
BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for
Image- and Video-Classification Models. CoRR abs/2210.17130 (2022)

-- 
Kohei Suenaga (末永幸平), Ph.D
Associate professor (准教授)
Graduate School of Informatics, Kyoto University
(京都大学情報学研究科)
ksuen...@gmail.com
https://urldefense.com/v3/__http://www.fos.kuis.kyoto-u.ac.jp/*ksuenaga/__;fg!!IBzWLUs!QUeqOFxyvhc7vUCd7LIHTzOlABQ_46gYcaOkpZMuhj-QQX640MmDSOPIO21A6zJgJj_PvuWQBEY9pxWg43oNabB5iq8IlJ9uiv4BZgsK9maEPQ$
 


[TYPES/announce] Postdoc position on design and/or verification of distributed systems at the University of Birmingham

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

Dear all,

We would like to invite applications for an up to 3 years fully-funded
postdoctoral position within the School of Computer Science at the
University of Birmingham (see below for details on how to apply).

The successful candidate will contribute to an EPSRC-funded project aiming
at designing and formally verifying distributed systems, in particular
Byzantine fault-tolerant distributed systems as used for example in
blockchain technology.

The start date is flexible, ideally April 2023.

The environment:


The School of Computer Science has large and thriving Theory and Security
research groups. Among our research interests related to this project are
for example:
   - Formal verification
   - Proof assistants
   - Model checking
   - Blockchain Technology
   - Security & Privacy

Both groups are very active, organising regular seminars, informal
meetings, and actively participating in many events such as the Midlands
Graduate School or the Cyber Security PhD Winter School. For more
information see
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx__;!!IBzWLUs!SSgJ1Dw0cckQWAKG8L5LQFSNyaJHo0uSzOg8cQDtC4hJs3hivj0uDkoTLKFv5wduk8PF_1ZP1LtwNRQzoJ3djV2EgndTqDVdipbdZg$
 
and
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/centre-for-cyber-security-and-privacy/index.aspx__;!!IBzWLUs!SSgJ1Dw0cckQWAKG8L5LQFSNyaJHo0uSzOg8cQDtC4hJs3hivj0uDkoTLKFv5wduk8PF_1ZP1LtwNRQzoJ3djV2EgndTqDWOyOH0SA$
 
.

How to apply:
-

Interested people are encouraged to contact me by email (v.ra...@bham.ac.uk)
to discuss their research interests and details of the positions. Further
information on how to apply is available here:
https://urldefense.com/v3/__https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/521/?utm_medium=jobshare__;!!IBzWLUs!SSgJ1Dw0cckQWAKG8L5LQFSNyaJHo0uSzOg8cQDtC4hJs3hivj0uDkoTLKFv5wduk8PF_1ZP1LtwNRQzoJ3djV2EgndTqDXKLFqEIA$
 

Best,
Vincent Rahli

-- 
https://urldefense.com/v3/__https://vrahli.github.io/__;!!IBzWLUs!SSgJ1Dw0cckQWAKG8L5LQFSNyaJHo0uSzOg8cQDtC4hJs3hivj0uDkoTLKFv5wduk8PF_1ZP1LtwNRQzoJ3djV2EgndTqDXsfAlIZA$
 


[TYPES/announce] Postdoc position in verification and automata learning at MPI-SWS, in association with Cornell and Oxford

2022-11-22 Thread James Worrell
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A postdoctoral position in automated verification and automata learning is
open at the Max Planck Institute for Software Systems in Saarbrücken,
Germany, in the group of Prof. Joël Ouaknine. The project is a joint
collaboration with Prof. Alexandra Silva (Cornell University) and Prof.
James Worrell (Oxford University). The post is based in Saabrücken, but the
successful candidate will have the opportunity occasionally to travel to
Cornell (Ithaca, USA) and Oxford (UK).

Active automata learning has become an important technique in model-based
verification, as it enables the automated inference of models. There is a
gap between the existing learning algorithms and the expressive models that
have been used in e.g. probabilistic model checking. The goal of this
project is two-fold: on the one hand, we want to design active learning
algorithms for probabilistic automata and study the limits of learnability;
on the other hand, we want to explore their use in practical scenarios,
including randomised routing.

Qualifications:

-- A PhD awarded (or nearing completion) in Computer Science, Mathematics,
or a closely related discipline.

-- Knowledge and publications across some areas of: logic in computer
science, formal verification, automata theory, programming language theory,
probabilistic systems, learning, randomised algorithms, concurrency theory,
program synthesis.

This position is available on a full time basis for one year in the first
instance, with the possibility of renewal(s).

For informal enquiries, please contact Prof. Joël Ouaknine .


[TYPES/announce] Postdoc Position on Hardware Verification via Model Learning, Royal Holloway University of London -- Application deadline 7 Dec 2022

2022-11-14 Thread Sammartino, Matteo
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

- Application deadline: Midnight, 7 Dec 2022
- Salary: £37,467
- Duration: until November 2023

Applications are invited for the post of Post-Doctoral Research Assistant in 
the Computer Science Department at Royal Holloway, University of London.

The post holder will have an exciting opportunity to work on the EPSRC-funded 
"Verification of Hardware Concurrency via Model Learning" (CLeVer) project
(EP/S028641/1), led by Prof. Alexandra Silva (UCL/Cornell) and Matteo 
Sammartino (RHUL), in collaboration with ARM, world-leading designer of 
multi-core chips.

For an informal discussion about the post, please contact Dr. Matteo Sammartino 
on matteo.sammart...@rhul.ac.uk.

# Brief description of the project

Digital devices are increasingly complex, therefore there is a pressing need to 
automate the assessment of their correctness. Formal verification provides 
highly effective techniques to assess the correctness of systems. However, 
formal models are usually built by humans, and as such can be error-prone and 
inaccurate.

The project aims to develop a novel verification framework for hardware, which 
combines learning, testing and model-checking. Not all models are suitable for 
this purpose and hence specific classes of models will need to be developed, 
depending on the task at hand. Subsequently, learning and verification 
techniques for these classes need to be devised and tested in realistic case 
studies. We have an industrial partner, ARM, that will provide valuable 
guidance on the design and development of the aforementioned tasks.

# The ideal candidate

We are looking for candidates with a PhD in one of the following areas: 
model-based testing and verification, model learning, automated analysis of 
hardware systems. Experience in multiple areas will be valued. Candidates 
ideally should also have strong programming skills.

# Where to apply

https://urldefense.com/v3/__https://jobs.royalholloway.ac.uk/0922-411-R__;!!IBzWLUs!Ql4x98AHBGBXp8EftOjO8vr9oTKppmjfsdYpqCJyeLkaUYZbajCRXcVw1LdY-wgIUroTgr7fZ4Oeq9LVpCtQ5NwmmyKAU69TUSdFpOq5C3-D$
  


Best wishes,

   Matteo Sammartino


==
Matteo Sammartino, Lecturer
Royal Holloway University of London
Department of Computer Science
Tel.: (+44) (0) 1784 44 3690
Office: 2-07, Bedford Building
https://urldefense.com/v3/__https://matteosammartino.com/__;!!IBzWLUs!Ql4x98AHBGBXp8EftOjO8vr9oTKppmjfsdYpqCJyeLkaUYZbajCRXcVw1LdY-wgIUroTgr7fZ4Oeq9LVpCtQ5NwmmyKAU69TUSdFpA87nBfj$
  


This email, its contents and any attachments are intended solely for the 
addressee and may contain confidential information. In certain circumstances, 
it may also be subject to legal privilege. Any unauthorised use, disclosure, or 
copying is not permitted. If you have received this email in error, please 
notify us and immediately and permanently delete it. Any views or opinions 
expressed in personal emails are solely those of the author and do not 
necessarily represent those of Royal Holloway, University of London. It is your 
responsibility to ensure that this email and any attachments are virus free.


[TYPES/announce] Postdoc position in automata and concurrency theory, at the University of Warsaw

2022-11-07 Thread Sławomir Lasota
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We invite applications of motivated and research-focused individuals to
carry out research on Petri nets and their extensions as part of the NCN
project "Data-enriched models of computation". The project aims at
advancing theoretical foundations at the borderline  between automata
theory, concurrency and formal verification. The successful candidate
will be hosted by the automata theory group at the University of Warsaw,
offering a vibrant working atmosphere, and exciting and challenging
research problems.

**
- Application deadline: November 30, 2022
- Starting date: flexible
- Duration: one year, possible extension to another year
- Principal investigator: Slawomir Lasota  
(https://urldefense.com/v3/__http://www.mimuw.edu.pl/*sl__;fg!!IBzWLUs!Teyogg7Xi7WiQvgI177N8amJu29J6mt7iUfhFa5eIgg7cjoBRFFDfPKjLQmW7vXJV6WdpQ_pb3RJ2vwIv1akIHwe9uuYicML7w$
  )
- Contact: s...@mimuw.edu.pl
**

Further details: 
https://urldefense.com/v3/__https://www.mimuw.edu.pl/*sl/2022-postdoc-recr.txt__;fg!!IBzWLUs!Teyogg7Xi7WiQvgI177N8amJu29J6mt7iUfhFa5eIgg7cjoBRFFDfPKjLQmW7vXJV6WdpQ_pb3RJ2vwIv1akIHwe9uv7MAn2JA$
  


[TYPES/announce] Postdoc position at the University of Birmingham

2022-10-30 Thread vincent rahli
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

We would like to invite applications for an up to 3 years fully-funded
postdoctoral position within the School of Computer Science at the
University of Birmingham (see below for details on how to apply).

The successful candidate will contribute to an EPSRC-funded project aiming
at designing and formally verifying distributed systems, in particular
Byzantine fault-tolerant distributed systems as used for example in
blockchain technology.

The start date is flexible, ideally early 2023.

The environment:


The School of Computer Science has large and thriving Theory and Security
research groups. Among our research interests related to this project are
for example:
   - Formal verification
   - Proof assistants
   - Model checking
   - Blockchain Technology
   - Security & Privacy

Both groups are very active, organising regular seminars, informal
meetings, and actively participating in many events such as the Midlands
Graduate School or the Cyber Security PhD Winter School. For more
information see
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/activity/computer-science/theory-of-computation/index.aspx__;!!IBzWLUs!SsBU8jzeb7Ri4jp5CtqTIN-gUh5ws5PVmfdk_l008d-sSn-OAbC6X35XnpcZQBwfeWKn5IupCrxw49Qta1V1t0iMoeJe913wK6jJcw$
  
and
https://urldefense.com/v3/__https://www.birmingham.ac.uk/research/centre-for-cyber-security-and-privacy/index.aspx__;!!IBzWLUs!SsBU8jzeb7Ri4jp5CtqTIN-gUh5ws5PVmfdk_l008d-sSn-OAbC6X35XnpcZQBwfeWKn5IupCrxw49Qta1V1t0iMoeJe9101EC3pIg$
  
.

How to apply:
-

Interested people are encouraged to contact me by email (v.ra...@bham.ac.uk)
to discuss their research interests and details of the positions. Further
information on how to apply is available here:
https://urldefense.com/v3/__https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/521/?utm_medium=jobshare__;!!IBzWLUs!SsBU8jzeb7Ri4jp5CtqTIN-gUh5ws5PVmfdk_l008d-sSn-OAbC6X35XnpcZQBwfeWKn5IupCrxw49Qta1V1t0iMoeJe9128nRwokA$
  

Best,
Vincent Rahli

-- 
https://urldefense.com/v3/__https://vrahli.github.io/__;!!IBzWLUs!SsBU8jzeb7Ri4jp5CtqTIN-gUh5ws5PVmfdk_l008d-sSn-OAbC6X35XnpcZQBwfeWKn5IupCrxw49Qta1V1t0iMoeJe9118X27sDQ$
  


[TYPES/announce] Postdoc position (6 years) at the Security and Privacy group, TU Wien

2022-10-04 Thread Maffei, Matteo
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

TU Wien is Austria's largest institution of research and higher education in 
the fields of technology and natural sciences. With over 26,000 students and 
more than 4000 scientists, research, teaching and learning dedicated to the 
advancement of science and technology have been conducted here for more than 
200 years, guided by the motto "Technology for People". As a driver of 
innovation, TU Wien fosters close collaboration with business and industry and 
contributes to the prosperity of society.
The Institute of Logic and Computation, research unit Security and Privacy, at 
TU Wien offers a position as a university assistant (post-doc) limited to 6 
years for 40 hours/week. Expected start: November 2022
Tasks:

  *   Deep interest in scientific problems and the motivation for independent 
and goal-oriented research
  *   Independent teaching or participation in teaching and supervision of 
students
  *   Ability to develop methods, concepts, as well as their realization and 
evaluation and the willingness to contribute in interdisciplinary scientific 
projects
  *   Participation in organizational and administrative tasks of the research 
division and the faculty

Your profile:

  *   Completion of an appropriate doctorate and in-depth knowledge of the 
subject area
  *   An outstanding publication record in top security and privacy conferences
  *   Research background in one of the following topics: formal methods for 
security and privacy, blockchain technologies, intersection between machine 
learning and security or privacy, or web security
  *   Experience in teaching and publication activities as well as interest and 
pleasure in research and working with students
  *   Organisational and analytical skills as well as a structured way of 
working
  *   Excellent skills in English communication and writing, knowledge of 
German (level B2) or willingness to learn it in the first year.

We offer:

  *   Continuing personal and professional education and flexible working hours
  *   Central location of workplace with very good accessibility (U1/U4 
Karlsplatz)
  *   A creative environment in one of the most liveable cities in the world
  *   A highly competitive salary (B1 scale, 56.861,70 EUR per year before tax)
  *   Additional benefits for employees can be found at the following link: 
Fringe-Benefit Catalogue of TU 
Wien
  *   An international and interdisciplinary research environment: the Security 
and Privacy research unit 
(https://urldefense.com/v3/__https://secpriv.wien__;!!IBzWLUs!SvPQr1OZoU1RRA3LigsMVUxZ3xa47mAchnIsQUUXE82u81Rnw2OhRHTU4A4iQfsN-BQy_oXOOKB4whJ0vLwRH46awM5KXiTlVk_a9PE8RYE$
  
) works on various aspects of security and privacy (e.g., system security, 
web security, mobile security, IoT security, formal methods, machine learning, 
cryptography, and blockchain), researchers come from all over the world and 
frequently interact with each other on interdisciplinary research projects, the 
working language in the research unit is English.

TU Wien is committed to increasing the proportion of women in particular in 
leadership positions. Female applicants are explicitly encouraged to apply. 
Preference will be given to women when equally qualified, unless reasons 
specific to a male applicant tilt the balance in his favour.

People with special needs are equally encouraged to apply. In case of any 
questions, please contact the confidant for disabled persons at the university, 
Mr. Gerhard Neustätter.
Entry level salary is determined by the pay grade B1 of the Austrian collective 
agreement for university staff. This is a minimum of currently EUR 
4,061.50/month gross, 14 times/year for 40 hours/week. Relevant working 
experiences may increase the monthly income.

We look forward to receiving your application until 10.11.2022. Applications 
are only processed online: 
https://urldefense.com/v3/__https://jobs.tuwien.ac.at/Job/194015__;!!IBzWLUs!SvPQr1OZoU1RRA3LigsMVUxZ3xa47mAchnIsQUUXE82u81Rnw2OhRHTU4A4iQfsN-BQy_oXOOKB4whJ0vLwRH46awM5KXiTlVk_adw27RcA$
  
For formal inquiries, please contact Univ.-Prof. Dr. Matteo Maffei.


[TYPES/announce] Postdoc Position on Hardware Verification via Model Learning, Royal Holloway University of London -- Application deadline 15 Oct 2022

2022-09-17 Thread Sammartino, Matteo
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

- Application deadline: Midnight, 15 Oct 2022
- Salary: £37,467
- Duration: until November 2023

Applications are invited for the post of Post-Doctoral Research Assistant in 
the Computer Science Department at Royal Holloway, University of London.

The post holder will have an exciting opportunity to work on the EPSRC-funded 
"Verification of Hardware Concurrency via Model Learning" (CLeVer) project
(EP/S028641/1), led by Prof. Alexandra Silva (UCL/Cornell) and Matteo 
Sammartino (RHUL), in collaboration with ARM, world-leading designer of 
multi-core chips.

For an informal discussion about the post, please contact Dr. Matteo Sammartino 
on matteo.sammart...@rhul.ac.uk.

# Brief description of the project

Digital devices are increasingly complex, therefore there is a pressing need to 
automate the assessment of their correctness. Formal verification provides 
highly effective techniques to assess the correctness of systems. However, 
formal models are usually built by humans, and as such can be error-prone and 
inaccurate.

The project aims to develop a novel verification framework for hardware, which 
combines learning, testing and model-checking. Not all models are suitable for 
this purpose and hence specific classes of models will need to be developed, 
depending on the task at hand. Subsequently, learning and verification 
techniques for these classes need to be devised and tested in realistic case 
studies. We have an industrial partner, ARM, that will provide valuable 
guidance on the design and development of the aforementioned tasks.

# The ideal candidate

We are looking for candidates with a PhD in one of the following areas: 
model-based testing and verification, model learning, automated analysis of 
hardware systems. Experience in multiple areas will be valued. Candidates 
ideally should also have strong programming skills.

# Where to apply

https://urldefense.com/v3/__https://jobs.royalholloway.ac.uk/0922-411__;!!IBzWLUs!UHRVDKYuGBisANVHYXkRq9B3MgRVK7e_eBNc9OvbewBWtdzXJdp8PWhGd3OtSRBvpXV5hVLVaqRZO0QebeM5Cd07RV69HWCsb5Y_vDKT_18g$
  


==
Matteo Sammartino, Lecturer
Royal Holloway University of London
Department of Computer Science
Tel.: (+44) (0) 1784 44 3690
Office: 2-07, Bedford Building
https://urldefense.com/v3/__https://matteosammartino.com/__;!!IBzWLUs!UHRVDKYuGBisANVHYXkRq9B3MgRVK7e_eBNc9OvbewBWtdzXJdp8PWhGd3OtSRBvpXV5hVLVaqRZO0QebeM5Cd07RV69HWCsb5Y_vF-Ta8ou$
  


This email, its contents and any attachments are intended solely for the 
addressee and may contain confidential information. In certain circumstances, 
it may also be subject to legal privilege. Any unauthorised use, disclosure, or 
copying is not permitted. If you have received this email in error, please 
notify us and immediately and permanently delete it. Any views or opinions 
expressed in personal emails are solely those of the author and do not 
necessarily represent those of Royal Holloway, University of London. It is your 
responsibility to ensure that this email and any attachments are virus free.


[TYPES/announce] Postdoc Position in Testing AI Ethics at King's College London

2022-08-29 Thread M.R. Mousavi
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Research Associate in Testing AI Ethics
at King's College London

Vacancy terms: Full time, fixed term contract for 18 months
Salary: £38,826 per annum, including London Weighting Allowance
Deadline : 15 September 2022

Application link:
https://urldefense.com/v3/__https://jobs.kcl.ac.uk/gb/en/job/049688/Research-Associate-in-Testing-AI-Ethics__;!!IBzWLUs!Wd037xsBfW7AStKnlyn6V4K1dYt3j8c9j1azBFKGMHsKFEqdL6ib8P0r1H9XvTdhrKbudbtLF28t6DVMEMgZtH0hY-pATf-DQBU$
  



Job description

Within the UKRI Trustworthy Autonomous System Node on Verifiability, we
have an exciting opening for a postdoctoral researcher on testing ethical
aspects of AI. These include testing aspects such as fairness and bias, as
well as privacy and explainability. You will be working within a vigorous
multi-disciplinary environment of the Trustworthy Autonomous System program
with researchers across many disciplines designing and verifying the
autonomous systems of the future. You will be using and advancing the state
of the art in testing (validation and verification) methods to provide
assurances of ethical decision making i n sub-symbolic AI components, such
as neural networks and statistical machine learning techniques.

This post will be offered on a fixed-term contract for 18 months

This is a full-time post - 100% full time equivalent

Key responsibilities

Developing world-leading research results in collaboration with the
team, on testing ethical concerns on AI;
Developing a comprehensive and rigorous set of requirements for
such ethical concerns;
Developing public benchmarks and datasets for evaluating the
developed techniques and their future alternatives;
Coordinating the related activities within the team and within the
larger project and program.

The above list of responsibilities may not be exhaustive, and the post
holder will be required to undertake such tasks and responsibilities as may
reasonably be expected within the scope and gradin g of the post.

Skills, knowledge, and experience

Essential criteria

A doctoral degree in Computer Science, Software Engineering, or closely
related fields (also candidates with their dissertations submitted or under
submission will be considered).
Solid track record of study and research in software engineering and
software testing (validation and verification)
Proficiency in programming; familiarity with AI frameworks
Possessing analytical skills; basic knowledge of statistical methods

Desirable criteria

Affinity with ethical theories and their formalisation
Affinity with formal verification and mathematical modelling techniques


[TYPES/announce] Postdoc position on specification and verification of heterogeneous systems at Imperial

2022-06-17 Thread Donaldson, Alastair F
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi all

John Wickerson and I have an opening for a two year postdoc on specification 
and verification of heterogeneous systems, and their programming languages. See 
here for 
details. I'd be very grateful if you should share this with folks who might be 
interested.

Feel free to contact either 
me or 
John if you're interested in applying and would like to chat informally first.

Thanks!

Ally



[TYPES/announce] Postdoc position in Tokyo: model checking and optimization metaheuristics

2022-04-19 Thread Ichiro Hasuo
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[Please distribute, apologies for multiple postings.]

Open Position for a PostDoc Researcher
(Model Checking Extended with Optimization Metaheuristics, April 2022)

ERATO Hasuo Metamathematics for Systems Design Project (ERATO MMSD
) invites applications for a postdoc
researcher. We aim to combine model checking and optimization
metaheuristics, in order to scale formal verification techniques up to
real-world industrial problems that are complex and black-box. We aim to do
so, at the same time, in a way guided by solid meta-theoretical foundations
such as those which we've presented in LICS and CAV. We thus explore new
shapes of application of logic to modern software and systems. The position
will be especially suited for those who have experience in model checking
research and who wish to expand their research portfolio.

Some further details are found below. See
https://urldefense.com/v3/__https://group-mmm.org/eratommsd/open-position-for-a-postdoc-researcher-march-2022/__;!!IBzWLUs!BDZN4rGPRuQkPWQZcGBZBnmH8ZJjFN7noYdQLXvoXdEnxRidC1Otggp1onYqYgQRJpapZntWM2LN3g$
 
for full details.

Thanks a lot for your consideration.
Best, Ichiro


-
JOB DESCRIPTION

The candidate will work at National Institute of Informatics
, Tokyo, Japan, and will pursue a novel
extension of model checking techniques (temporal logic, automata theory)
with optimization metaheuristics (evolutionary computation, stochastic
optimization, statistical machine learning).

The goal is to overcome two major challenges that currently limit the
applicability of formal verification techniques to real-world industrial
systems, namely *scalability* and the *absence of white-box models*. In our
endeavor towards the goal, we do not mind relying on testing, rather than
exhaustive verification; this puts us somewhat closer to so-called *lightweight
formal methods*.

That said, our theoretical development shall be nothing "lightweight." We
believe that there is a great theoretical depth here--we will explore the
depth using logical, automata-theoretic, and/or categorical machinery.
This *theory
of * *"lightweight" formal methods* will significantly expand the current
landscape of application of logic to software.

The position should be especially suited for model checking researchers who
wish to expand their research portfolio. We find case studies in our
industrial collaborations and seek applicability to those real-world
problems (they are mostly from the manufacturing industry). At the same
time, we seek rigorous logical/automata-theoretic/categorical foundations
for the solutions we come up with--so our work stays well in the realm of
the formal verification community. We work in an interdisciplinary
environment, and the candidate will be constantly exposed to interaction
with control theory, software engineering, automated driving, and category
theory.

The candidate will work closely with Prof. Ichiro Hasuo
 and a few other team members. It is
possible that the candidate be granted an academic title (such as Project
Assistant/Associate Professor).
References

The following are some outcomes of our efforts so far. They are listed here
in order to exemplify concrete topics. Note that the topics of these papers
are diverse, and the candidate is not expected to follow all of them. A
good match with one of them would suffice.

   - Masaki Waga, Étienne André, Ichiro Hasuo: Symbolic Monitoring Against
   Specifications Parametric in Time and Data. CAV (1) 2019: 520-539. doi
   
 arXiv
   

   (The topic is the theory of timed automata, which strikes a balance
   between theory and applicability.)
   - Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo: Widest
   Paths and Global Propagation in Bounded Value Iteration for Stochastic
   Games. CAV (2) 2020: 349-371 doi
   
 arXiv
   

[TYPES/announce] postdoc position in Lille (France) on type systems and logical methods

2022-03-16 Thread Patrick Baillot
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Applications are invited for a postdoc position at the University of Lille, 
France. The successful candidate will work under the supervision of Patrick 
Baillot, on research topics related to type systems and logical methods in one 
of the following areas (non exclusive list):
- timing or complexity analysis for sequential, parallel or concurrent systems 
(e.g. for process calculi or session types); 
- privacy properties of programs (sensitivity analysis, differential privacy…) 
- typing methods for synchronous languages (e.g. static analysis and clock 
calculus).

Candidates should have, or expect shortly to obtain, a PhD in Computer Science, 
with expertise in programming languages, logic or formal methods. The position 
is for one year. The starting date could be June 2022. There is no teaching 
load. Knowledge of French is not required.

 The candidate will join the SyCoMoRES team 
(https://urldefense.com/v3/__https://www.cristal.univ-lille.fr/en/teams/sycomores/?force_lang=true__;!!IBzWLUs!HggkZOp9ERXT8-2F41p5ejd_OCyQcj_15NrgIKnkEMLkjUrNkN8aRXhksgksQmiqv_KvRf66QsSAIA$
  ), which is a joint project team between Inria, CNRS and University of Lille. 
It belongs to the CRIStAL research center 
(https://urldefense.com/v3/__https://www.cristal.univ-lille.fr/en/__;!!IBzWLUs!HggkZOp9ERXT8-2F41p5ejd_OCyQcj_15NrgIKnkEMLkjUrNkN8aRXhksgksQmiqv_KvRf5_xU4NAQ$
  ). The position is funded by I-site Université Lille Nord-Europe.
 Lille is a youthful and dynamic city, located in the north of France, at the 
crossroads of Europe, close to Paris (1h10 by train), Brussels and London.
 
If you are interested please contact me as soon as possible, with a brief 
outline of your academic background and research interests.
As a second step, a complete application will consist of
+ a cover letter;
+ a detailed CV including a list of publications and a summary of research;
+ contact information for two or three academic references;
This application should be sent by email to patrick.bail...@univ-lille.fr .

The applications will be reviewed as soon as they are received and until the 
position is filled.

Patrick Baillot 
(https://urldefense.com/v3/__https://pro.univ-lille.fr/patrick-baillot/__;!!IBzWLUs!HggkZOp9ERXT8-2F41p5ejd_OCyQcj_15NrgIKnkEMLkjUrNkN8aRXhksgksQmiqv_KvRf7dGYLD7A$
  )


[TYPES/announce] Postdoc position on session types for Erlang, University of Glasgow

2022-03-07 Thread Simon Gay

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


University of Glasgow
College of Science and Engineering
School of Computing Science

Research Assistant / Associate
Ref:077847
Grade 6/7: £29,614 - £33,309 / £36,382 - £40,927 per annum

We have a position for a research assistant / associate in the theory, 
design and implementation of programming languages. This position is 
associated with the EPSRC-funded project "STARDUST: Session Types for 
Reliable Distributed Systems".


The project is funded until 30th September 2024 and the position is 
available from 1st May 2022.



*Project Description*

Distributed software systems are an essential part of the infrastructure 
of modern society. Such systems typically comprise diverse software 
components deployed across networks of hosts. Ensuring their reliability 
is challenging, as software components must correctly communicate and 
synchronise with each other, and any of the hardware or software 
components may fail. Failure and service "outage" is extremely costly, 
with worldwide financial losses due to software failures in 2017 
estimated at US$1.7tn, up from US$1.1tn in 2016.


Failures can occur at all levels of the system stack: hardware, 
operating systems, networks, software, and users. Here we focus on using 
advanced programming language technologies to enable the software level 
to handle failures that arise from any level of the stack. Our aim is to 
provide software-level reliability for distributed systems by combining 
fault prevention with fault tolerance. The key objective is to combine 
the communication-structuring mechanism of session types with the 
scalability and fault-tolerance of actor-based software architectures.


The result will be a well-founded theory of reliable actor programming, 
supported by a collection of libraries and tools, and validated on a 
range of case studies. Key aims are to deliver tools that provide 
lightweight support for developers – e.g. warning of potential issues – 
and to allow developers to continue to use established idioms. By doing 
so we aim to deliver a step change in the engineering of reliable 
distributed software systems.


The project is a collaboration between the University of Glasgow 
(Professor Simon Gay and Professor Phil Trinder), Imperial College 
London (Professor Nobuko Yoshida) and the University of Kent (Professor 
Simon Thompson and Dr Laura Bocchi). The industrial partners are Actyx 
AG, Erlang Solutions Ltd, Quviq AB and Tata Consultancy Services.



*Principal Duties*

The successful candidates will be responsible for conducting research 
into the theory and practice of session types for actor languages, and 
for evaluating programming language designs and implementations in 
relation to realistic case studies provided by the industrial collaborators.


The main line of work in Glasgow is the development of a session type 
system for Erlang. The first phase of the project has produced a session 
type system for a higher-order actor-based functional calculus, with a 
prototype implementation. The next phase will transfer these theoretical 
results into a session type system for Erlang, implemented as either a 
language extension or an external tool.


You should have, or be close to completion of, a PhD in a relevant area, 
or have comparable experience; an awarded PhD or equivalent experience 
is necessary for appointment at Grade 7. You should have a track record 
of publication and communication of research results, strong programming 
and software engineering skills, and a strong background in programming 
languages, including type systems and implementation. It is desirable 
also to have one or more of the following: a combination of theoretical 
and practical skills; knowledge of the theory or practice of concurrent 
and distributed systems; knowledge of the theory or practice of 
actor-based languages;
knowledge of the theory of session types. Experience with the theory and 
implementation of type systems in general is more important than 
specific knowledge of session types or actor languages.


We seek applicants at an international level of excellence. The School 
of Computing Science at the University of Glasgow has an international 
research reputation, and Glasgow, Scotland's largest city, offers an 
outstanding range of cultural resources and a high quality of life.


It is the University of Glasgow’s mission to foster an inclusive 
climate, which ensures equality in our working, learning, research and 
teaching environment.


We strongly endorse the principles of Athena SWAN, including a 
supportive and flexible working environment, with commitment from all 
levels of the organisation in promoting gender equity.


Information about the Programming Language research theme at the 
University of Glasgow:



[TYPES/announce] postdoc position, University of Warsaw

2022-02-23 Thread Sławomir Lasota
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[ erratum: mistaken salary amount corrected ]

Postdoc position in automata theory, University of Warsaw

**
- Application deadline: March 31, 2022
- Starting date: As soon as possible
- Salary: 27.000 EUR per annum (very competitive in Poland)
- Duration: one year, possible extension to another year
- Project: "Data-enriched models of computation" funded by NCN
- Principal investigator: Prof. Sławomir Lasota  
(https://urldefense.com/v3/__http://www.mimuw.edu.pl/*sl__;fg!!IBzWLUs!EHBRhAjeYEDUNQwhE6Oizf3ysQHhCfrM64bEGeqiw5AEo4uvAQEo_0JzR29C8gnYnG9kBakO3hXXeA$
 )
- Contact: s...@mimuw.edu.pl
**

The project aims at advancing theoretical foundations at the borderline
between automata theory, concurrency and verification. We promise, except
for very competitive salary, a vibrant working atmosphere in the automata
group at the University of Warsaw, and exciting and challenging research
problems.

The ideal candidate is expected to have:

• PhD degree or equivalent in computer science or math
• Solid background in formal methods and automata theory
• Significant publication record
• Strong motivation for research work in foundations of computer science
• Advanced skills in written and spoken English.

To apply, please send your curriculum vitae to s...@mimuw.edu.pl.


[TYPES/announce] postdoc position, University of Warsaw

2022-02-21 Thread Sławomir Lasota
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position in automata theory, University of Warsaw

**
- Application deadline: March 31, 2022
- Starting date: As soon as possible
- Salary: 27.000 PLN per annum (very competitive in Poland)
- Duration: one year, possible extension to another year
- Project: "Data-enriched models of computation" funded by NCN
- Principal investigator: Prof. Sławomir Lasota  
(https://urldefense.com/v3/__http://www.mimuw.edu.pl/*sl__;fg!!IBzWLUs!BtApIM-cXc3QIz-uFVhZyCjZ2BOhP7hAkMH_R2QVfeCgW11UeT8lSuTsD640A1V5VM0Mc321-Gz1Ew$
 )
- Contact: s...@mimuw.edu.pl
**

The project aims at advancing theoretical foundations at the borderline
between automata theory, concurrency and verification. We promise, except
for very competitive salary, a vibrant working atmosphere in the automata
group at the University of Warsaw, and exciting and challenging research
problems.

The ideal candidate is expected to have:

• PhD degree or equivalent in computer science or math
• Solid background in formal methods and automata theory
• Significant publication record
• Strong motivation for research work in foundations of computer science
• Advanced skills in written and spoken English.

To apply, please send your curriculum vitae to s...@mimuw.edu.pl.


[TYPES/announce] Postdoc position at the University of Lisbon

2021-12-22 Thread Vasco Thudichum Vasconcelos
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

University of Lisbon -- One Post Doctoral Research Fellowship

We are looking to fill one post-doctoral research fellowship in the area of 
programming languages, type systems and logics. The position is funded by the 
research project "SafeSessions - Safe Concurrent Programming with Session 
Types", 
https://urldefense.com/v3/__https://www.lasige.pt/project/safesessions/__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb_UCBGYxw$
 .

We seek applicants with strong interest in some of the following topics: 
programming language design and implementation, logics and types, concurrency 
and distribution. Applicants should hold a PhD degree in Computer Science or 
related area.

The position is funded by the Foundation for Science and Technology for an 
initial period of 12 months, renewable until the end of the project (February 
29, 2024 or six months thereafter). Applications are open until February 15, 
2022.

The complete offer description can be found at 
https://urldefense.com/v3/__https://www.euraxess.pt/jobs/721789__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb8bu0XBiQ$
 . Further information can be obtained from 
lasige-candidatu...@listas.di.ciencias.ulisboa.pt. Applicants are encouraged to 
contact Professor Vasco T. Vasconcelos directly.


About the University of Lisbon and the LASIGE research lab

The University of Lisbon (ULisboa) is the largest university in Portugal and a 
leading one within wider Europe.  Comprising eighteen faculties, ULisboa offers 
400 degree programmes at undergraduate and postgraduate level.  Each year it 
accepts more than 5,000 international students – around 10% of its total cohort 
– who represent 100 different countries. ULisboa leads the main international 
rankings, is amongst the 200 best universities worldwide according to the 2019 
Shanghai Ranking.

LASIGE, 
https://urldefense.com/v3/__https://www.lasige.pt__;!!IBzWLUs!A2S_14d2AW5szG565PdsS_-WGxz9tgiyFXWyJtiRYtTTta3AONbI602l85wghr-phhaVjb-lI63vlA$
 , is a research unit at ULisboa evaluated as Excellent by the Portuguese 
Science Agency (FCT) in 2018, with a perfect score of 15 points. LASIGE closely 
mentors more than 100 young researchers (at masters, doctoral, and 
post-doctoral level), continually stimulating excellence in research. LASIGE 
members teach MSc and PhD level courses in Computer Science and Engineering 
(CSE) at ULisboa, regularly publish in top venues, and enjoy top-notch 
bibliometric indices. LASIGE runs a large number of international projects, 
boasts three spin-offs, and multiple technology transfers.

The high-level research conducted at LASIGE, the scientific background and 
international projection of its group leaders, the academic and industrial 
network to which it belongs, and the experience in advanced training of its 
members makes LASIGE the perfect research unit to work as a postdoc.

If this was not enough, the city of Lisbon offers history and culture, 
shopping, restaurants, nearby beaches and a vibrant nightlife.

[TYPES/announce] Postdoc Position on Verification of Concurrent Systems via Model Learning, Royal Holloway University of London -- Application deadline 9 Jan 2022

2021-12-03 Thread Matteo Sammartino
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

- Application deadline: Midnight, 9 Jan 2022
- Starting date: As soon as possible
- Salary: £35,931-£37,979
- Duration: until February 2023


Applications are invited for the post of Post-Doctoral Research Assistant in 
the Computer Science Department at Royal Holloway, University of London.

Successful applicants will be working on the EPSRC-funded "Verification of 
Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led 
by Alexandra Silva (UCL/Cornell) and Matteo Sammartino (Royal Holloway 
University of London).

This is a joint research effort involving Royal Holloway University of London, 
University College London, and ARM, world-leading designer of multi-core chips.

For an informal discussion about the post, please contact Dr. Matteo Sammartino 
on matteo.sammart...@rhul.ac.uk.


# Project Description

Digital devices increasingly rely on multi-threaded computation, with 
sophisticated concurrent behaviour becoming prevalent at any scale. As the 
complexity of these systems increases, there is a pressing need to automate the 
assessment of their correctness, especially with respect to concurrency-related 
aspects. Formal verification provides highly effective techniques to assess the 
correctness of systems. However, formal models are usually built by humans, and 
as such can be error-prone and inaccurate.

The CLeVer project aims to:

- develop a novel verification framework that relies on learning techniques to 
automatically build and verify models of concurrency, with a particular focus 
on multi-core systems.

- apply the framework to real-world verification tasks, in collaboration with 
ARM.

# The ideal candidate

We are looking for candidates with a PhD in one of the following areas: 
model-based testing and verification, formal methods for concurrency, automated 
analysis of hardware systems. Experience in multiple areas will be valued. 
Candidates ideally should also have strong programming skills.

# Where to apply

https://urldefense.com/v3/__https://jobs.royalholloway.ac.uk/0721-259-R-R__;!!IBzWLUs!GBUI4ogBjKihbUy7Zjvs5uy-jYLfnkDBmHoLxe66Aocp0u-vNUn0dwNvEzw0ElB4e1xgKh3NbHDrlQ$
 


[TYPES/announce] Postdoc position in quantum formal verification @ Université Paris-Saclay, CEA List, France

2021-12-03 Thread christophe chareton
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The emerging quantum software group @ CEA List, Université Paris-Saclay,
offers
a two years fully-funded postdoctoral position at the crossroad of quantum
programming, program analysis and formal methods.


=== OUR GROUP

We are an emerging group in formal verification and static analysis of
quantum
programs, integrated in the Software Safety Laboratory of CEA List,
Université
Paris-Saclay. Our long term goal is to design and develop formal techniques
and
tools enabling productive and certified quantum programming. Especially, we
develop Qbricks [1], a proof of concept environment for formally verified
quantum programming language.

See our website at 
https://urldefense.com/v3/__https://qbricks.github.io/__;!!IBzWLUs!DTmRMuyfh6ehH9DSFJaqLMIs4YlesQRyI8Q8dkpjvQlB5Tx-NTs4Fg265PDuyMEj-jAvzHF-RqvC7g$
  for additional information.

=== ABOUT THE POSTDOC POSITION

Adapting the best practice for classical computing formal verification --
deductive
verification, first order logic reasoning--, our recent development of
Qbricks enables
formal specification -- circuit well-formedness, functional behavior,
complexity --
and verification for quantum programming with ideal qubits. The goal of
this post-
doctoral position is to extend  this practice to quantum compilation and
physical
qubits implementations.  Possibilities include, among others, error
correction
mechanisms in certified quantum code, together with specifications and
reasoning
technique for certifying its reliability, automatized certified optimizer
for quantum
circuits, hardware agnostic assembly language together
with its compiler, qubit mapping, etc

Keywords: quantum programming, compilation, optimization, formal
verification, deductive
verification


=== HOW TO APPLY

Applications should be sent to christophe.char...@cea.fr as soon as
possible
(first come, first served) and by early February 2021 at the latest.
Candidates
should send a CV, a cover letter, a transcript of all their university
results,
as well as contact information of two references. The  position is expected
to
start in May 2021.

Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA)
Contact: christophe.chare...@cea.fr, sebastien.bar...@cea.fr


[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An
Automated
Deductive Verification Framework for Circuit-building Quantum Programs.
ESOP
2021.


[TYPES/announce] Postdoc position: Automated Reasoning and Proof Certificates (part-time)

2021-11-28 Thread Georg Weissenbacher
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

This is an announcement of a part-time postdoc position at TU Wien
(Vienna, Austria).

The Research Unit Formal Methods in Systems Engineering at TU Wien is
looking for a postdoctoral researcher and offers a position for 6
years (for 20 hours/week). The expected starting date is January 2022.

Tasks:
+ Independent teaching or participation in teaching and supervision of students
+ Project work and leadership of project groups
+ Publishing activities
+ Participation in and organization of scientific events
+ Participation in organizational and administrative tasks of the
research division and the faculty

Your profile:
+ Completed doctoral studies in a relevant field (e.g., automated reasoning)
+ Research experience in the area automated propositional reasoning
and checking of proof certificates; in-depth knowledge of the subject
area propositional reasoning (CDCL), checking of propositional proof
certificates (DRAT, DPR, DSR), and Craig Interpolation
+ Deep interest in scientific problems and the motivation for
independent and goal-oriented research
+ The ability to develop methods, concepts, as well as their
realization and evaluation and the willingness to contribute in
scientific projects
+ Experience in national and international research cooperation as
well as in project management and presentations
+ Experience in teaching and publication activities as well as
interest and enthusiasm in research and work/support with students
+ Organizational and analytical skills as well as a structured way of working
+ Excellent command of the English language and very good
communicative skills and team competences
+ Very good skills in English communication and writing. Knowledge of
German (level B2) or willingness to learn it in the first year.

More details and the application form can be found on
https://urldefense.com/v3/__https://jobs.tuwien.ac.at/Job/168937__;!!IBzWLUs!GnI7CRlER0RPBnSdLfkSIqfhSQ5CewoYzU0VV4JeSzZe9zbLONKX5-1Aq3VFv7ae33NrqL_onkI4LA$
 


[TYPES/announce] postdoc position in Lille (France) on type systems and logical methods

2021-11-22 Thread Patrick Baillot
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a postdoc position at the University of Lille, 
France. The successful candidate will work under the supervision of Patrick 
Baillot, on research topics related to type systems and logical methods in one 
of the following areas (non exclusive list): 
timing analysis for sequential, parallel or concurrent systems ; privacy 
properties of programs (sensitivity, differential privacy…) ; typing methods 
for synchronous languages (e.g. static analysis for clock assignment).

Candidates should have, or expect shortly to obtain, a PhD in Computer Science, 
with expertise in programming languages, logic or formal methods. The position 
is for one year. The starting date would be at the beginning of 2022 but is 
negociable. There is no teaching load. Knowledge of French is not required.

 The candidate will join the SyCoMoRES team 
(https://urldefense.com/v3/__https://www.cristal.univ-lille.fr/en/teams/sycomores/?force_lang=true__;!!IBzWLUs!F-NQSW8QIIvOoBOvgM0TAKrSixOOksZrCRmqvMQ5sJ1Ez_u_CxbUhSs0brVMpgvO8RZtbPQyth0LcA$
  ), within the CRIStAL research center 
(https://urldefense.com/v3/__https://www.cristal.univ-lille.fr/en/__;!!IBzWLUs!F-NQSW8QIIvOoBOvgM0TAKrSixOOksZrCRmqvMQ5sJ1Ez_u_CxbUhSs0brVMpgvO8RZtbPQIu1IuCw$
  ). The position is funded by I-site Université Lille Nord-Europe.

If you are interested please contact me as soon as possible, with a brief 
outline of your academic background and research interests. 
As a second step, a complete application will consist of
+ a cover letter;
+ a detailed CV including a list of publications and a summary of research;
+ contact information for two or three academic references;
This application should be sent by email to patrick.bail...@univ-lille.fr .

The review of applications will begin on December 6 and continue until 
the position is filled.

Patrick Baillot 
(https://urldefense.com/v3/__https://pro.univ-lille.fr/patrick-baillot/__;!!IBzWLUs!F-NQSW8QIIvOoBOvgM0TAKrSixOOksZrCRmqvMQ5sJ1Ez_u_CxbUhSs0brVMpgvO8RZtbPQc0FGwiw$
  )


[TYPES/announce] Postdoc position in distributed computing at the IMDEA Software Institute

2021-11-09 Thread Alexey Gotsman
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a postdoc position at the IMDEA Software Institute 
in Madrid, Spain. The successful candidate will work under the supervision of 
Alexey Gotsman 
(https://urldefense.com/v3/__https://software.imdea.org/*gotsman/__;fg!!IBzWLUs!FJLHfUxN51laoXQiqq-QhAhDmnBJIj0hzQBw9R8QsnzIKzbhyt_IeWDpvsBYPfa3cjR0s_7Ty7ptNA$
 ), with research topics determined based on the common interests of the 
candidate and the supervisor. Possible areas include blockchains and 
distributed transaction processing. This covers algorithms, correctness proofs 
and system engineering.

Candidates should have, or expect shortly to obtain, a PhD in Computer Science, 
with expertise in distributed computing theory, distributed systems or formal 
methods. The position is initially for one year, with possibilities for 
extension. The starting date is negotiable. The position is based in Madrid, 
Spain, where the IMDEA Software Institute is situated. The institute provides 
for travel expenses and an internationally competitive salary. The working 
language at the institute is English.

Applicants interested in the position should submit their application at 
https://urldefense.com/v3/__https://careers.software.imdea.org/using__;!!IBzWLUs!FJLHfUxN51laoXQiqq-QhAhDmnBJIj0hzQBw9R8QsnzIKzbhyt_IeWDpvsBYPfa3cjR0s_6IkkGLyQ$
  reference code 2021-11-postdoc-distributed. The deadline for applications is 
January 9th, 2022. For enquiries about the position please contact Alexey 
Gotsman 
(https://urldefense.com/v3/__https://software.imdea.org/*gotsman/__;fg!!IBzWLUs!FJLHfUxN51laoXQiqq-QhAhDmnBJIj0hzQBw9R8QsnzIKzbhyt_IeWDpvsBYPfa3cjR0s_7Ty7ptNA$
 ).



[TYPES/announce] Postdoc Position in Formal Verification

2021-10-06 Thread Ralf Kuesters

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

The Institute of Information Security at University of Stuttgart offers a

fully-funded Postdoc position in formal verification

The successful candidate is expected to work on tool-supported formal 
verification of security-critical systems and security protocols.


The position is available immediately with an internationally 
competitive salary (German public salary scale TV-L E13 or TV-L E14, 
depending on the candidate's qualification, ranging from about 4.600 
Euro to 6.200 Euro monthly gross salary).  The appointment period 
follows the German Wissenschaftszeitvertragsgesetz (WissZeitVg), ranging 
from one year to up to six years.


The Institute of Information Security offers a creative international 
environment for top-level international research in Germany's high-tech 
region.


The successful candidate should have a Ph.D. (or should be very close to 
completion thereof) in Computer Science, Mathematics, Information 
Security, or a related field. We value strong analytical skills and


- solid knowledge of logic, proofs and/or formal verification techniques 
(Theorem Proving, Type Checking, etc.),

- solid programming experience.

Knowledge in security is not required, but a plus. Knowledge of German 
is not required.


The University of Stuttgart is an equal opportunity employer. 
Applications from women are strongly encouraged. Severely challenged 
persons will be given preference in case of equal qualifications.


To apply, please send email with subject "Application: Postdoc Position 
Formal Verification" and a single PDF file containing the following 
documents to ralf.kuest...@sec.uni-stuttgart.de:
* Cover letter (explaining your scientific background and your 
motivation to apply)

* Curriculum Vitae
* List of publications
* Copies of transcripts and certificates (Bachelor, Master, PhD)
* Names of at least two references

The deadline for applications is

October 31st, 2021.

Late applications will be considered until the position is filled.

See 
https://urldefense.com/v3/__https://sec.uni-stuttgart.de/__;!!IBzWLUs!Go5GoU6GW0_u-STe-GsXubd-ARSgxsdKHQlSHfAeOTwWGrUX-iBX4zVsts8ItYoc7loZnIPpW48uow$
  for more information about the institute.

See https://urldefense.com/v3/__https://www.sec.uni-stuttgart.de/institute/job-openings/__;!!IBzWLUs!Go5GoU6GW0_u-STe-GsXubd-ARSgxsdKHQlSHfAeOTwWGrUX-iBX4zVsts8ItYoc7loZnIN7yBIyHw$  for the 
official job announcement.


For further information please contact: Prof. Dr. Ralf Küsters, 
ralf.kuest...@sec.uni-stuttgart.de.


--
Prof. Dr. Ralf Küsters
Institute of Information Security - SEC
University of Stuttgart
Universitätsstraße 38
D-70569 Stuttgart
Germany
https://urldefense.com/v3/__https://sec.uni-stuttgart.de__;!!IBzWLUs!Go5GoU6GW0_u-STe-GsXubd-ARSgxsdKHQlSHfAeOTwWGrUX-iBX4zVsts8ItYoc7loZnIP-YlExvA$ 
Phone: +49 (0) 711 685 88283


[TYPES/announce] Postdoc position: Formal Methods (Munich, Germany)

2021-08-30 Thread Gunther Reißig

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

We invite applications for a post-doctoral researcher position in the
field of formal methods, in Munich, Germany, the city
of the Oktoberfest. The successful candidate is expected to advance
the state of the art of abstraction-based synthesis and verification
and to extend existing synthesis software. Depending on background and
interests of the candidate, possible research foci are: automated
determination of error bounds for floating-point implementations of
numerical algorithms; parallelizable on-the-fly synthesis algorithms;
adaptive state discretization; input/output languages and problem
specific compiler for synthesis software.

Required qualifications:
* PhD degree in Computer Science, Systems and Control, Mathematics,
  or a related field. Exceptionally qualified and experienced
  candidates with an MSc degree will also be considered.
* Solid experience in one of the following fields: Set-valued
  numerics; validated floating-point arithmetic; dynamic programming;
  formal methods; reachability analysis; software development.
* Programming proficiency (C or Ada).
* Efficient communication skills in English.

The position is full-time and paid according to pay scale ``TVOeD
Bund, E 14''. Actual income depends on marital status and professional
experience, and starts from EUR 33000 net p.a. (E-13/EUR 31000 for
applicants with an MSc degree). Reimbursement for travel expenses to
conferences. No teaching load. The position is available immediately
and for a duration until April 2023. It is open to applicants
worldwide; no special security clearance necessary.

Your complete application consists of the following documents, which
should be sent as a single PDF file to the email address given below
(deadline: September 19, 2021):

* CV
* One-page cover letter (clearly indicating available start date as
  well as relevant qualifications, experience and motivation)
* University certificates and transcripts (BSc, MSc and PhD degrees)
* Up to three letters of recommendation
* List of publications
* Possibly an English language certificate

All documents should be in English or German.

Gunther Reissig
https://urldefense.com/v3/__http://www.reiszig.de/gunther/__;!!IBzWLUs!EgjqJNBwkxQajNf9KNtq1VHZe5mDmNadGClXcuNGBg8XbbzKAivNcbY_sPbUIyx4-_c3jb83jy2igA$ 
Email: gunther2...@reiszig.de, Subject: Postdoc ref 9y22x

Bundeswehr University Munich, Germany
Department of Aerospace Engineering
Institute of Control Engineering



[TYPES/announce] Postdoc position: Formal Verification/Synthesis (Munich, Germany, deadline: August 28, 2021)

2021-07-28 Thread Gunther Reißig

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

We invite applications for an EU funded post-doctoral researcher
position in the field of formal verification/synthesis. The successful
candidate is expected to advance the state of the art of
abstraction-based synthesis and verification for nonlinear
continuous-state plants and to extend existing synthesis
software. Depending on background and interests of the candidate,
possible research foci are: automated determination of error bounds
for floating-point implementations of numerical algorithms;
parallelizable on-the-fly synthesis algorithms; adaptive state
discretization; input/output languages and compiler for synthesis
software.

Required qualifications:
* PhD degree in Computer Science, Systems and Control, Mathematics,
  or a related field. Exceptionally qualified and experienced
  candidates with an MSc degree will also be considered.
* Solid experience in one of the following fields: Set-valued
  numerics; validated floating-point arithmetic; dynamic programming;
  formal verification/synthesis; professional grade software
  development.
* Programming proficiency (C or Ada).
* Efficient communication skills in English.

The position is full-time and paid according to pay scale ``TVOeD
Bund, E 14''. Actual income depends on marital status and professional
experience, and starts from EUR 33000 net p.a. (E-13/EUR 31000 for
applicants with an MSc degree). Reimbursement for travel expenses to
conferences. No teaching load. The position is available immediately
and for a duration until April 2023. It is open to applicants
worldwide; no special security clearance necessary.

Your complete application consists of the following documents, which
should be sent as a single PDF file to the email address given below
(deadline: August 28, 2021):

* CV
* One-page cover letter (clearly indicating available start date as
  well as relevant qualifications, experience and motivation)
* University certificates and transcripts (BSc, MSc and PhD degrees)
* Up to three letters of recommendation
* List of publications
* Possibly an English language certificate

All documents should be in English or German.

Gunther Reissig
http://www.reiszig.de/gunther/
Email: gunther2...@reiszig.de, Subject: Postdoc ref 9y22x
Bundeswehr University Munich, Germany
Department of Aerospace Engineering
Institute of Control Engineering


[TYPES/announce] Postdoc position: Formal methods in control (Munich, Germany), ref 9y22x

2021-07-18 Thread Gunther Reissig
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear Sirs,
I would like to point you to the announcement of a Postdoc position in
Munich, Germany, the city of the Oktoberfest.

I would appreciate if you could advertise the position in your
department or forward it to whomever you deem appropriate.

The announcement is attached as a pdf file, and a plain text version
can be found at the end of this email.

Thank you.

Sincerely,
Gunther Reissig


Gunther Reißig, Dr. habil.
Professor

Bundeswehr University Munich
Department of Aerospace Engineering
LRT-15, Institute of Control Engineering

85577 Neubiberg (Munich)
Germany

E-Mail: gunther.reis...@unibw-muenchen.de
WWW:http://www.reiszig.de/gunther/
FAX:+49-89-6004-4565 
Skype:  guntherreissig


Postdoc position: Formal methods in control (Munich, Germany)

Bundeswehr University Munich, Germany
Department of Aerospace Engineering
Institute of Control Engineering

We invite applications for an EU funded post-doctoral researcher
position in the field of formal methods in control. The successful
candidate is expected to advance the state of the art of
abstraction-based synthesis and verification for nonlinear
continuous-state plants and to extend existing synthesis
software. Depending on background and interests of the candidate,
possible research foci are: automated determination of error bounds
for floating-point implementations of numerical algorithms;
parallelizable on-the-fly synthesis algorithms; adaptive state
discretization; input-output interface of synthesis software.

Required qualifications:
* PhD degree in Systems and Control, Computer Science, Mathematics,
  or a related field. Exceptionally qualified and experienced
  candidates with an MSc degree will also be considered.
* Solid experience in one of the following fields: Set-valued
  numerics; validated floating-point arithmetic; dynamic programming;
  formal methods in control.
* Programming proficiency (C or Ada).
* Efficient communication skills in English.

The position is full-time and paid according to pay scale ``TVOeD
Bund, E 14''. Actual income depends on marital status and professional
experience, and starts from EUR 33000 net p.a. (E-13/EUR 31000 for
applicants with an MSc degree). Reimbursement for travel expenses to
conferences. No teaching load. The position is available immediately
and for a duration until April 2023. It is open to applicants
worldwide; no special security clearance necessary.

Your complete application consists of the following documents, which
should be sent as a single PDF file to the email address given below
(deadline: July 28, 2021):

* CV
* One-page cover letter (clearly indicating available start date as
  well as relevant qualifications, experience and motivation)
* University certificates and transcripts (BSc, MSc and PhD degrees)
* Up to three letters of recommendation
* List of publications
* Possibly an English language certificate

All documents should be in English or German.

Gunther Reissig
http://www.reiszig.de/gunther/
Email: gunther2...@reiszig.de, Subject: Postdoc ref 9y22x

AusschreibungEmailA.pdf
Description: Binary data


[TYPES/announce] Postdoc Position in Formal Verification

2021-07-13 Thread Ralf Kuesters

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

The Institute of Information Security at University of Stuttgart offers a

fully-funded Postdoc position in formal verification

The successful candidate is expected to work on tool-supported formal 
verification of security-critical systems and security protocols.


The position is available immediately with an internationally 
competitive salary (German public salary scale TV-L E13, or TV-L E14, 
depending on the candidate's qualification, ranging from about 4.600 
Euro to 6.200 Euro monthly gross salary).  The appointment period 
follows the German Wissenschaftszeitvertragsgesetz (WissZeitVg), ranging 
from one year to up to six years.


The Institute of Information Security offers a creative international 
environment for top-level international research in Germany's high-tech 
region.


The successful candidate should have a Ph.D. (or should be very close to 
completion thereof) in Computer Science, Mathematics, Information 
Security, or a related field. We value strong analytical skills and


- solid knowledge of logic, proofs and/or formal verification techniques 
(Theorem Proving, Type Checking, etc.),

- solid programming experience.

Knowledge in security is not required, but a plus. Knowledge of German 
is not required.


The University of Stuttgart is an equal opportunity employer. 
Applications from women are strongly encouraged. Severely challenged 
persons will be given preference in case of equal qualifications.


To apply, please send email with subject "Application: Postdoc Position 
Formal Verification" and a single PDF file containing the following 
documents to ralf.kuest...@sec.uni-stuttgart.de:
* Cover letter (explaining your scientific background and your 
motivation to apply)

* Curriculum Vitae
* List of publications
* Copies of transcripts and certificates (Bachelor, Master, PhD)
* Names of at least two references

The deadline for applications is

August 1st, 2021.

Late applications will be considered until the position is filled.

See https://sec.uni-stuttgart.de/ for more information about the institute.

See https://www.sec.uni-stuttgart.de/institute/job-openings/ for the 
official job announcement.


For further information please contact: Prof. Dr. Ralf Küsters, 
ralf.kuest...@sec.uni-stuttgart.de.


--
Prof. Dr. Ralf Küsters
Institute of Information Security - SEC
University of Stuttgart
Universitätsstraße 38
D-70569 Stuttgart
Germany
https://sec.uni-stuttgart.de
Phone: +49 (0) 711 685 88283


[TYPES/announce] Postdoc position in software security at Penn State CSE

2021-07-01 Thread Gang (Gary) Tan
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Postdoc position at Penn State Computer Science and Engineering

Applications are invited for a full-time postdoctoral researcher
position in the Security of Software (SOS) Lab at Penn State
(http://www.cse.psu.edu/~gxt29/sos/).  The SOS Lab focuses on
methodologies that help create secure software systems.  We are
seeking a highly qualified individual to work in the area of software
security, including topics such as software security verification,
compiler-based software security, binary code analysis and
hardening. An applicant should possess a doctoral degree in Computer
Science or Computer Engineering and have strong background in computer
security, programming languages, or formal methods.  The candidate
must have an excellent track record of original research and the
ability to work as part of a team.

The postdoc will be provided with competitive salary and employment
benefits. The initial appointment will be for one year, with an option
to renew for a second year.

Inquiries about the position should be directed to Dr. Gang Tan
(g...@psu.edu).  Applicants should apply via the following website
and be prepared to provide at least two names of references when
asked. Applications will be reviewed until the position
is filled.

https://psu.wd1.myworkdayjobs.com/en-US/PSU_Academic/job/University-Park-Campus/Postdoctoral-Researcher_REQ_014314-1

Penn State is a major research university ranked 3rd in U.S.  in
industry-sponsored research.  The CSE department is ranked 6th in
computer-security research (as per csrankings.org) and 8th in U.S. in
research expenditures and has strong research programs in security.
The U.S. News and World Report consistently ranks Penn State's College
of Engineering undergraduate and graduate programs among the top in
the nation.

--

Gang (Gary) Tan
Professor, Penn State CSE and ICDS
W358 Westgate Building
http://www.cse.psu.edu/~gxt29
Tel:814-8657364



[TYPES/announce] Postdoc Position at Simon Fraser University in Vancouver, Canada

2021-06-21 Thread Gaboardi, Marco
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The announcement below may be relevant for people interested in Rust, ownership 
types, and verification looking for a postdoc position.

Best,
Marco

Steve Ko (Associate Professor at Simon Fraser University in Vancouver, Canada, 
https://steveyko.github.io/) is looking for a postdoc with a background in 
programming languages and/or software engineering. The postdoc will work on a 
research project that explores verification for mobile systems software using 
the Rust language combined with symbolic execution and other verification 
tools. The project is being done in collaboration with Marco Gaboardi 
(Associate Professor at Boston University in Boston, USA, 
http://cs-people.bu.edu/gaboardi/). The postdoc will be the main lead of the 
project and potentially work with a group of PhD/MS/undergraduate students. The 
expected duration of the position is two years. Interested applicants are 
encouraged to send their CV directly to Steve Ko at steve...@sfu.ca.

 - Steve


[TYPES/announce] Postdoc Position, Programming Group - SCS, University of St.Gallen

2021-06-21 Thread Guido Salvaneschi
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A fully funded postdoc position is open in the Programming Group at
the School of Computer Science, University of St. Gallen (CH).
The position is supervised by Prof. Guido Salvaneschi.

Our research interests include programming languages and
software engineering, with applications to distributed systems
and security. For an overview of our research topics, please
check the page:
https://programming-group.com

The position is supported by the Swiss National Science Foundation.
It is available immediately with an internationally
competitive salary and an initial appointment of two years.

The successful candidate should have a Ph.D. (or should be very close to
completion thereof) in Computer Science, Mathematics, or a related field.

The position will be filled as soon as a suitable candidate is found.
Applications should be sent to guido.salvanes...@unisg.ch
with a CV, including a publication list, and a short motivation letter.


-- 
Guido Salvaneschi
Associate Professor
University of St.Gallen - Switzerland


[TYPES/announce] Postdoc Position in Formal Security Analysis of Cryptographic Protocols and Web Applications, University of Stuttgart, Germany

2021-06-15 Thread Ralf Kuesters
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Institute of Information Security at University of Stuttgart offers a

fully-funded Postdoc position.

The successful candidate is expected to work on tool-supported formal
analysis of cryptographic protocols and web applications building, among
others, on our work published at EuroS 2021, S 2019, CSF 2017, CCS
2016, CCS 2015, ESORICS 2015, and S 2014. One goal is to provide
tool-supported security analysis based on DY* for our web infrastructure
model (WIM).

The position is available immediately with an internationally
competitive salary (German public salary scale TV-L E13 or TV-L E14,
depending on the candidate's qualification).  The appointment period
follows the German Wissenschaftszeitvertragsgesetz (WissZeitVg), ranging
from one year to up to six years.

The Institute of Information Security offers a creative international
environment for top-level international research in Germany's high-tech
region.

The successful candidate should have a Ph.D. (or should be very close to
completion thereof) in Computer Science, Mathematics, Information
Security, or a related field. We value strong analytical skills.
Knowledge in one or more of the following fields is an asset:

 - Formal Methods (Verification, Theorem Proving, F*, Type Checking, etc.)
 - Security Protocol Analysis
 - Web Security

Knowledge of German is not required.

The University of Stuttgart is an equal opportunity employer.
Applications from women are strongly encouraged. Severely challenged
persons will be given preference in case of equal qualifications.

To apply, please send email with subject "Application: Postdoc Position"
and a single PDF file containing the following documents to
ralf.kuest...@sec.uni-stuttgart.de:
* Cover letter (explaining your scientific background and your
motivation to apply)
* Curriculum Vitae
* List of publications
* Copies of transcripts and certificates (Bachelor, Master, PhD)
* Names of at least two references

The deadline for applications is

July 4th, 2021

Late applications will be considered until the position is filled.

See https://sec.uni-stuttgart.de/ for more information about the institute.

See https://www.sec.uni-stuttgart.de/institute/job-openings/ for the
official job announcement.

For further information please contact: Prof. Dr. Ralf Küsters,
ralf.kuest...@sec.uni-stuttgart.de.

-- 
Prof. Dr. Ralf Küsters
Institute of Information Security - SEC
University of Stuttgart
Universitätsstraße 38
D-70569 Stuttgart
Germany
https://sec.uni-stuttgart.de
Phone: +49 (0) 711 685 88283


[TYPES/announce] Postdoc position at Cambridge in programming with equations

2021-06-01 Thread Jeremy Yallop
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We have an opening in Cambridge for a researcher on the Frex project
(https://www.cl.cam.ac.uk/~jdy22/projects/frex).  Informal enquiries
are welcome: please feel free to get in touch.

---
Research Assistant / Associate in Programming with Equations (Fixed Term)
https://www.jobs.cam.ac.uk/job/29773/

Applications are invited for a Research Assistant/Associate to join
the Frex project.

The Frex project investigates the use of equations in programming.
There is often a large gap between what programmers know about their
programs and what compilers are able to deduce.  Frex targets this gap
by exposing to the compiler the equations proved by programmers about
programs so that they can be used to improve optimisation and type
checking.

The position will involve working with Frex project members at the
Universities of Cambridge, Edinburgh and St Andrews to extend and
improve the design and implementations of Frex. Work up to this point
has focused on equations for first-order single-sorted algebras and we
plan to extend the techniques to more elaborate settings.

The successful candidate is likely to have (or expect to be awarded
soon) a PhD in computer science or a related discipline, as well as a
track record of published research and experience or demonstrable
interest in some combination of the following:

- Dependently typed programming languages or proof assistants based on
type theory (e.g. Agda, Idris, Coq, Lean)

- Functional programming languages (e.g. F#, OCaml, Haskell)

- Partial evaluation, normalization by evaluation, multi-stage
programming, supercompilation or related techniques

- Algebraic structures, universal algebra and categorical algebra

Informal enquiries are welcome and should be directed to Dr Jeremy
Yallop (jeremy.yal...@cl.cam.ac.uk)

Expected starting date: 1 September 2021


[TYPES/announce] Postdoc position at CMU: Verified DSLs for high assurance systems

2021-05-31 Thread Eunsuk Kang
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are looking for a motivated postdoctoral scholar to work on formal
methods for the development of high-assurance software and cyber-physical
systems. In particular, the project involves the development and
enhancement of systems through the composition and verification of programs
written in high-level domain-specific languages (DSLs). Potential research
problems include: (1) design and implementation of DSLs for high-assurance
autonomous systems, (2) compositional verification techniques for the DSLs,
and (3) techniques for debugging and repair of DSL programs. You will also
be expected to mentor PhD students involved in this project and contribute
to the development of a scalable, practical DSL development environment.

** Location **
You will be a member of the Institute for Software Research, School of
Computer Science at Carnegie Mellon University in the USA. Pending the
evolving situation with COVID-19, you will be expected to work from
Pittsburgh, PA.

** Qualifications **
Candidates are expected to have a PhD in Computer Science or related
fields, with a strong background and research record in formal methods,
software engineering, and/or programming languages. Familiarity with
automated verification technologies (e.g., model checkers, SMT solvers) is
desirable.

** Timeline **
The position is expected to begin in September 2021 for 1 year, with a
possibility of extension.

** Instructions **
To apply, please send a copy of your latest CV and research statement to
Eunsuk Kang (esk...@cmu.edu).


[TYPES/announce] Postdoc position at the LIP laboratory, ENS de Lyon, France

2021-05-11 Thread Damien Pous
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The LIP laboratory, located at the ENS de Lyon in France, is offering a 1
year post-doc position in computer science, starting on the 1st September
2021. Candidates should have a PhD and a strong background in one of the
subjects studied in the LIP. (Please refer to http://www.ens-lyon.fr/LIP/ for
details.) The salary will depend on the successful candidate's prior
research experience with a guaranteed minimum of 2300 EUR/month before
taxes.

An application consists of a single PDF file containing:
- a CV including a full list of publications; and
- a research project that in particular proposes a mentor in one of the
research teams of the LIP.

Inside the LIP laboratory, the Plume team
http://www.ens-lyon.fr/LIP/PLUME/?page_id=7 could be of particular interest
to the readers of the types and fom mailing lists (logic, semantics, formal
verification).

The application should be sent by email to russell.har...@ens-lyon.fr and
nicolas.trotig...@ens-lyon.fr by the 30th May, 23:59 UT. Reference letters
should be sent directly by email to the same addresses with the same
deadline.

With best regards,
Damien Pous


[TYPES/announce] postdoc position (6 years) in CL group in Innsbruck

2021-05-10 Thread Aart Middeldorp
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

6 year postdoc position in computational logic
==

The University of Innsbruck invites applications for a 6 year postdoctoral
position in the Computational Logic research group. Candidates must hold a
PhD degree in computer science. A strong background in computational logic
is required and knowledge of term rewriting is a welcome additional
qualification. The ideal candidate enjoys working with students at all
levels. Candidates are expected to conduct research leading to a
habilitation and contribute to teaching and administration. Knowledge of
German is not essential.

The position is a full-time "B1/3 position" with teaching obligations of
4 hours per semester. The annual gross salary is approximately EUR 55,000.
The official job advert (reference MIP-11910) appeared at

https://lfuonline.uibk.ac.at/public/karriereportal.details?asg_id_in=11910

Applications (including CV, publication list, and two letters of
recommendation) must be submitted electronically at

https://lfuonline.uibk.ac.at/public/karriereportal.bewerben?page=w_id=11910

no later than 28 May 2021. The starting date for the position is
1 October 2021. Informal inquiries may be addressed to

aart.middeldorp at uibk.ac.at

The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and
1976, is superbly located in the beautiful surroundings of the Tyrolean
Alps. The combination of the Alpine environment and urban life in this
historic town provides a high quality of living.

Further information is available from the following links:

Computational Logic:
http://cl-informatik.uibk.ac.at/ 

Department of Computer Science:
http://informatik.uibk.ac.at/ 

University of Innsbruck: 
http://www.uibk.ac.at/ 

City of Innsbruck: 
http://www.innsbruck.at/


[TYPES/announce] Postdoc position at Chalmers (2 years) in Programming Language Technology for Privacy

2020-11-18 Thread David Sands
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi,


I have an opening for a postdoctoral researcher at Chalmers, with preferred 
start at the beginning of the new year.  I'm looking for someone with proven 
research skills in relevant areas of programming languages (semantics, formal 
verification, static analysis, type systems) as well as experience and 
knowledge of reasoning about probabilistic systems in general, and preferably 
within differential privacy.


Deadline for applications is December 1!


Contact me for more info.

The formal ad and application procedure is here:


https://www.chalmers.se/en/about-chalmers/Working-at-Chalmers/Vacancies/Pages/default.aspx?rmpage=job=8926=UK


Cheers

Dave


ps. The department also have an open postdoc position in "taking functional 
languages to embedded devices" which you may have missed in an earlier 
announcement by Alejandro Russo - also very relevant to the types community.


https://www.chalmers.se/en/about-chalmers/Working-at-Chalmers/Vacancies/Pages/default.aspx?rmpage=job=8918





[TYPES/announce] Postdoc position at Boston College

2020-11-15 Thread Joseph Tassarotti
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A postdoctoral position is available in the Computer Science department at
Boston College as part of an NSF-supported project on formal verification
of machine learning algorithms. Candidates should have an interest in
formal verification and/or semantics of probabilistic programs.

Applications will be reviewed on a rolling basis until the position is
filled. The starting date is flexible, and may be as early as January 2021.

Please contact me for further information.

Applications may be submitted here:
https://bc.csod.com/ux/ats/careersite/2/home/requisition/4223?c=bc


[TYPES/announce] Postdoc position in Formal Methods, Programming Languages, and Systems, at the University of Salzburg, Computational Systems Group

2020-07-20 Thread Ana Sokolova
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are happy to announce an opening for a postdoc position within the
Computational Systems Group at the Department of Computer Sciences,
University of Salzburg,

The position is for up to 2.5 years with an initial contract for 1 year.
The ideal candidate is interested in one or more (ideally all) of the
areas: Formal Methods, Programming Languages, and Systems.

The position is associated with an Austria-wide project "Teaching Digital
Thinking" financed by the ministry of education related to teaching
computer science content to non-computer-science students and understanding
what computer science students could gain from other areas. We expect some
help from you regarding the project, but this is not supposed to be too
much work. We also expect you to engage in a reasonably small amount of
teaching. Other than that, we expect you to collaborate with us on research
in one of the mentioned areas. You would also have the freedom to conduct
independent research.

Please contact Christoph Kirsch (c...@cs.uni-salzburg.at) and/or Ana Sokolova
(a...@cs.uni-salzburg.at) for more information. The official opening (in
German) is available at:
https://www.uni-salzburg.at/fileadmin/multimedia/Serviceeinrichtung%20Personal/documents/A_0042_Postdoc_CoWi_II.pdf
.
The application deadline is August 5, 2020.

Best,
Ana and Christoph


[TYPES/announce] postdoc position in Aarhus, Denmark, at Center for Basic Research in Program Verification

2020-05-18 Thread Lars Birkedal
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


We are looking for Postdocs to work in the Center for Basic Research in Program 
Verification
in Aarhus, Denmark. Research topics include: extensions of higher-order 
concurrent
separation logics (such as our Iris logic, see iris-project.org), e.g., to 
reason about
distributed systems; probabilistic program logics; logical relations for 
relational reasoning
about safety and security properties; formal modeling of low-level capability 
machines,
and secure compilation; guarded cubical type theory; and Coq formalizations.
The Post Doc positions are for two years (with a possibility of extension).

Application deadline is June 1, 2020.

See 
https://www.au.dk/om/stillinger/job/center-for-basic-research-in-program-verification-cpv-is-looking-for-postdocs/
for more information.

Please contact me at birke...@cs.au.dk if you have 
any questions.

Best wishes,
Lars Birkedal


-- --
Lars Birkedal
Villum Investigator
Professor, Head of Logic and Semantics Group
Dept. of Computer Science
Aarhus University
Aabogade 34
8200 Aarhus N
Denmark
birke...@cs.au.dk
www.cs.au.dk/~birke



[TYPES/announce] Postdoc position at Tufts in Program Synthesis

2020-05-13 Thread Jeff Foster
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Tufts University Department of Computer Science invites applications for a 
postdoctoral research position. The candidate will work with Prof. Jeff Foster 
on a DARPA-funded project on program synthesis using symbolic solving and 
evolutionary algorithms.

Applicants should have expertise in at least one of those areas, though those 
with closely related expertise will also be considered. Strong applicants will 
also have demonstrated strong programming and organizational skills. The 
postdoctoral researcher will join the Tufts University Programming Languages 
group (TuPL), a collaborative, highly collegial group of PL researchers. More 
information about Prof. Foster (https://www.cs.tufts.edu/~jfoster/) and TuPL 
(https://tupl.cs.tufts.edu) can be found on the web. For more information about 
the position, please contact Prof. Foster (jfos...@cs.tufts.edu).

Interested candidates should send their CV, including the names of two 
references, to Prof. Foster at jfos...@cs.tufts.edu. Applications will be 
considered immediately, and application review will continue until the position 
is filled. The starting date is negotiable, and the position will last from 1-4 
years, depending on funding availability and preferences of the applicant.


Equal Employment Opportunity Statement

Tufts University, founded in 1852, prioritizes quality teaching, highly 
competitive basic and applied research, and a commitment to active citizenship 
locally, regionally, and globally. Tufts University also prides itself on 
creating a diverse, equitable, and inclusive community. Current and prospective 
employees of the university are expected to have and continuously develop skill 
in, and disposition for, positively engaging with a diverse population of 
faculty, staff, and students.

Tufts University is an Equal Opportunity/Affirmative Action Employer. We are 
committed to increasing the diversity of our faculty and staff and fostering 
their success when hired. Members of underrepresented groups are welcome and 
strongly encouraged to apply. See the University’s Non-Discrimination statement 
and policy here https://oeo.tufts.edu/policies-procedures/non-discrimination/. 
If you are an applicant with a disability who is unable to use our online tools 
to search and apply for jobs, please contact us by calling Johny Laine in the 
Office of Equal Opportunity (OEO) at 617-627-3298 or at johny.la...@tufts.edu. 
Applicants can learn more about requesting reasonable accommodations at 
http://oeo.tufts.edu.

[TYPES/announce] Postdoc position: verified timing-channel security for seL4

2020-02-10 Thread Toby Murray
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position: verified timing-channel security for seL4

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Applications close: February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

Timing channels plague modern systems, undermining their security.
Yet no operating system provides provable protection against them.
We believe that seL4 can be the first kernel to meet this challenge [1],
building on its world-first proof of confidentiality enforcement [2]
and its unique mechanisms for implementing time protection [3].

The seL4 project is seeking a highly motivated postdoctoral
researcher to investigate methods for proving that operating system
kernels can defend against timing channels. We are seeking somebody
with a research background in formal methods and security.

You will contribute to the development of methods for reasoning about
timing channels in verified operating system kernels, applied to the
seL4 kernel. Your work will also investigate how to extend seL4’s
existing proofs of information flow security, which primarily cover
storage channels, to also encompass timing channels.

Further details about the research project are summarised in the
following position paper:

[1] Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?" in Proceedings of the
Workshop on Hot Topics in Operating Systems (HotOS),
pages 23-29, May 2019.
https://arxiv.org/abs/1901.08338

The position is for two years in the first instance, based at the
University of Melbourne under Dr Toby Murray
(https://people.eng.unimelb.edu.au/tobym/).  You will work with a
close-knit team here at University of Melbourne, and collaborate
heavily with UNSW and Data61’s Trustworthy Systems group, in Sydney.

Candidates should have experience in at least one of the following:
 - program verification (e.g. Hoare logic)
 - information flow security (e.g. non-interference)
 - interactive theorem provers (e.g. Isabelle, Coq, etc.)

Applications close on February 25, 09:00 AM Australian Eastern Daylight
Time (AEDT; GMT +11)

To apply, or fore more information, visit:

http://jobs.unimelb.edu.au/caw/en/job/900474/research-fellow-in-verified-operating-system-security

Informal enquiries should be directed to
  Toby Murray
  toby.mur...@unimelb.edu.au
  https://people.eng.unimelb.edu.au/tobym/

References

[1] Gernot Heiser, Gerwin Klein and Toby Murray.
"Can We Prove Time Protection?", HotOS 2019

[2] Toby Murray, et al.
"seL4: From General Purpose to a Proof of Information
Flow Enforcement", IEEE Symposium on Security and Privacy 2013

[3] Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser.
"Time Protection: The Missing OS Abstraction", EuroSys 2019


[TYPES/announce] Postdoc position in Dependently Typed Programming, St Andrews

2019-11-04 Thread Edwin Brady
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,
There is a position available for a post doctoral research fellow to
work on Type Driven Development in Idris - for more details, and further
particulars, see below, or you can see it at
https://www.vacancies.st-andrews.ac.uk/Vacancies/W/6438/0/250507/889/research-fellow-ar2286sb

Any informal inquiries, please contact me directly on ec...@st-andrews.ac.uk

Edwin

Advert follows:

Applications are invited for a Research Fellow to work with Dr Edwin
Brady in the School of Computer Science at the University of St Andrews
on an EPSRC funded project "Programming as Conversation: Type-Driven
Development in Action".

The project aims to investigate the extent to which precise type systems
enhance programmer productivity, by developing languages and tools to
support the methodology of type-driven development.  It will build on
recent work developing a new version of the dependently typed
programming language Idris (https://www.idris-lang.org) and will involve
defining a semantics for program construction and manipulation as a
typed domain specific language for implementing editor actions. These
actions will include refactorings, and synthesising programs from their
types.

The successful candidate will have (or be about to obtain) a PhD in
Computer Science or a related subject. A strong background in functional
programming, dependent types or other advanced type systems is required.
The appointee will be expected to present their work both internally and
externally and will be expected to help with supervision and training of
postgraduate and undergraduate research students.

Funded by EPSRC (Engineering and Physical Sciences Research Council),
this post is available for three years, with a start date as soon as
possible.

For informal enquiries, please contact: Dr Edwin Brady, School of
Computer Science, ec...@st-andrews.ac.uk.

The University is committed to equality for all, demonstrated through
our working on diversity awards (ECU Athena SWAN/Race Charters; Carer
Positive; LGBT Charter; and Stonewall).  More details can be found at
http://www.st-andrews.ac.uk/hr/edi/diversityawards/.

Please quote ref:  AR2286SB

Closing Date:  26 November 2019






pEpkey.asc
Description: application/pgp-keys


[TYPES/announce] PostDoc Position in Quantitative Modeling at Aalborg University

2019-10-31 Thread Max Tschaikowski

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

PostDoc Position in Quantitative Modeling at Aalborg University, Denmark


We are looking for a highly motivated researcher with interest in formal
quantitative modeling.

The position is for one year with the possibility for an extension for
one year. The tentative starting date is February 2020 or soon thereafter.

Applicants are required to demonstrate strong background and
understanding in formal methods. An ideal candidate would have
experience with

--- Formal quantitative modeling using Markov chains or systems of
differential equations and;
--- Tool development facilitating the use of formal methods in practice.

The envisaged research will focus on the development of novel
optimality/verification preserving reduction techniques for quantitative
models. The PostDoc will be supervised by Max Tschaikowski and be a
member of the DEIS group of Kim Larsen. She/he will be expected to
perform independent research, collaborate with team members and help
with the supervision of PhD and MSc students as appropriate.

The envisaged research will build upon the publications listed below and
the accompanying software tool ERODE
(http://sysma.imtlucca.it/tools/erode/).

L. Cardelli, M. Tribastone, M. Tschaikowski, and A. Vandin.
Maximal aggregation of polynomial dynamical systems.
Proceedings of the National Academy of Sciences (PNAS), 2017

L. Cardelli, M. Tribastone, M. Tschaikowski, and A. Vandin.
Symbolic computation of differential equivalences.
Symposium on Principles of Programming Languages (POPL), 2016


Host institution: The Computer Science Department at Aalborg University
takes a leading international position within data management and
verification. It is a very young university (1974) but with a strong
international profile in Mathematics, and Computer Science &
Engineering, also hosting the two most highly cited Computer Scientists
of the country. Denmark in general and Aalborg in particular are known
for their excellent quality of life. Denmark took the top spot on the
United Nation's World Happiness Report, 2013 & 2014 & 2016 and came in
third in the 2015 report:
http://www.visitdenmark.co.uk/en-gb/denmark/art/happiest-people-world .


Application procedure: The applicant must have obtained a PhD degree
before the appointment day. In addition to an academic CV and
recommendation letters, the applicant should provide a short cover
letter which describes the applicant’s background, research interests
and initial thoughts and ideas. More specifically, interested applicants
should provide the following:

- A cover letter describing the reasons for applying, qualifications in
relation to the position, and intentions and visions for the position.
- Current academic curriculum vitae.
- Letters of recommendation (2 - 3).
- Copies of relevant certificates (Master of Science and PhD). On
request you could be asked for an official English translation.
- Additional qualifications in relation to the position (e.g., secured
scientific grants, participation in committees or boards, organization
of scientific events, etc.).
- Personal data.

For any questions, please do not hesitate to contact Max Tschaikowski (
tschaikow...@cs.aau.dk / www.maxtschaikowski.com ).

Applications should be send by email to Max Tschaikowski.




[TYPES/announce] Postdoc position at Imperial College London in software testing and programming languages

2019-09-10 Thread Donaldson, Alastair F
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a postdoctoral position, joint between the
Software Reliability Group and the Multicore Programming Group, under
the direction of Cristian Cadar and Alastair Donaldson.

We are looking for motivated applicants interested in working at the
intersection of software testing and programming languages. The research
will focus on two main strands:

* The first research strand will focus on testing compilers for popular
programming languages. We will design novel techniques to detect
compiler bugs that are currently out of reach to existing compiler
testing techniques. Particular attention will be given to bugs that are
security-critical in nature, presenting a largely unexplored attack
surface whereby software that is correct at the source level can
nevertheless be vulnerable to exploitation when erroneously compiled
into binary form. We also aim to mitigate this threat at runtime by
using novel multi-version execution techniques in which versions of the
same program compiled by different compilers are run in parallel.

* The second research strand will focus on helping software systems
evolve safely and securely. It will take a holistic approach to the
challenges of safe and secure software evolution, by combining offline
program analysis techniques such as static analysis and symbolic
execution to verify or comprehensively test software patches, with
runtime mechanisms such as multi-version execution for keeping the
software updated and secure against potentially erroneous changes that
make it into the deployed system.

For more details about this position, please see:
https://srg.doc.ic.ac.uk/vacancies/postdoc-comp-pass-19/

Deadline: 13 October 2019


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

2019-07-01 Thread 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.


[TYPES/announce] Postdoc position on quantified effects at Reykjavik University

2019-06-18 Thread Tarmo Uustalu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Quantified computational effects and interaction

Department of Computer Science, Reykjavik University

One postdoc position

Applications are invited for one postdoctoral position at the
Department of Computer Science, Reykjavik University.  The position is
part of a three-year research project funded by the Icelandic Research
Fund under the direction of Tarmo Uustalu. The overarching goal of to
advance the theory and practice of disciplined effectful programming,
based on graded monads, monad-like structures and interaction
laws. Interested applicants should contact the PI (email ta...@ru.is)
for closer details on the research proposal.

The successful candidate will benefit from, and contribute to, the
research environment at the Icelandic Centre of Excellence in
Theoretical Computer Science (ICE-TCS), with research groups on
concurrency, logic and semantics, algorithms, combinatorics. For
information about ICE-TCS and its activities, see

http://icetcs.ru.is/.

Moreover, she/he will cooperate with Shin-ya Katsumata and Maciej
Piróg during the project work and will benefit from the interaction
with their research groups at the National Institute of Informatics in
Tokyo and the University of Wroclaw.

*Qualification requirements*

Applicants for the postdoctoral position should have, or be about to
defend, a PhD degree in Computer Science or a closely related
field. Previous knowledge of at least one of lambda calculus and
functional programming, proof theory/type theory, programming language
semantics, category theory in computer science, proof assistants is a
prerequisite.

*Remuneration*

The wage will be approx 500 kISK per month before income tax, but
depend on the qualifications and experience of the postdoc. Check
http://payroll.is/en/ for what this means in terms of take-home pay. A
tax relief for foreign experts may apply.

The position is for two years, to start in autumn 2019 (the start date
is negotiable), and is renewable for another year, based on good
performance and mutual satisfaction.

*Application details*

Interested applicants should send their CV, including a list of
publications, to the PI (email ta...@ru.is), together with a statement
outlining their suitability for the project and the names of at least
two references.

Informal enquiries about the project and the conditions of work are
very welcome.

We will review applications as they arrive. Please apply before
5 July 2019.


[TYPES/announce] PostDoc Position in Program Analysis and Repair

2019-05-02 Thread Jooyong Yi
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A postdoctoral position is available at Ulsan National Institute of Science and 
Technology (UNIST). 

Job description:
=

The position will involve research in automated program repair in which our 
research team is specialized. You can obtain relevant information and 
publications in http://www.jooyongyi.com/. The ideal candidate will be someone 
who can synergize with our research team, as he or she continues to research 
further his/her own research topic.


Work environment:


UNIST (https://www.unist.ac.kr/) is a research-focussed national university 
located in the south-eastern part of South Korea. Despite its relatively young 
history (established in 2007), the university was ranked 1st for the last two 
years among all South Korean universities according to the CWTS Leiden Ranking. 
The working languages of the university are Korean and English, and Korean 
language skills are not a requirement for the position. 


Living environment:


The selected researcher is eligible to stay in an on-campus apartment. The 
university is located in the suburb of Ulsan, a South Korea's largest 
industrial city. The city shares its border with the nation's most historic 
city, Gyeongju, and the nation's largest harbor city, Busan. 


Application:


Interesting applicants may send their CV to me via jooy...@unist.ac.kr. 


Jooyong Yi
Assistant Professor
School of Electrical & Computing Engineering
Ulsan National Institute of Science and Technology
http://www.jooyongyi.com/


[TYPES/announce] Postdoc position on Automatic Parallelization of Dalvik Bytecode at CNAM, Paris

2019-01-31 Thread Tristan Crolard
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position on Automatic Parallelization of Dalvik Bytecode

Applications are invited for a Postdoctoral Research Fellow position
working on automatic parallelization of Android applications. While
modern smartphones possesses powerful CPUs with many-cores, smartphone
applications often tend not to fully exploit all the available power.

The overall aim of the project is to investigate the possibility of
automatic parallelization of Dalvik bytecode to improve applications
performances on multicore architectures. Dalvik bytecode is used as
the distribution format of Android applications. Android Runtime (ART)
compiles Dalvik applications into native machine code upon
installation. We propose to investigate high level parallelization of
Dalvik code before deploying it on ART.

This project is a collaboration between the CEDRIC laboratory of CNAM
and manycore.io. The postdoc will take place in Paris both at the CEDRIC 
laboratory and at manycore.io. The postdoc will be supervised by
Pr. Tristan Crolard and Dr. Sami Taktak at CEDRIC laboratory and
Nicolas Toper at manycore.io. The postdoc is available for a period of
1 year.

The successful candidate will have to develop a formal model of Dalvik 
code and formalize code transformation for automatic parallelization of 
Android applications. The work will involve developing techniques that
combine programming languages semantics, compilation and formal methods.

To apply you must hold (or be close to achieving) a PhD in Computer
Science. You should have demonstrated your research competence in formal 
methods and/or programming languages semantics and compilation. You
should also have a strong mathematical background, good programming
skills. English proficiency is required.

Interested applicants are encouraged to contact us with inquiries.

Sami Taktak 
Tristan Crolard 
Nicolas Toper 

https://cedric.cnam.fr
https://www.manycore.io


[TYPES/announce] PostDoc position at Inria Paris on Formally Secure Compilation in Coq

2019-01-04 Thread Catalin Hritcu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello,

A PostDoc position is available in my group at Inria Paris on Formally
Secure Compilation in Coq (https://secure-compilation.github.io).
I am seeking outstanding candidates with a strong, internationally
competitive research track record. Particularly interesting for us is
research expertise in:
- formal verification in the Coq proof assistant
  and verified compilation in particular (e.g. CompCert)
- security foundations, e.g., reference monitoring,
  hyperproperties, noninterference
Here are some (non-exhaustive) lists of potential research topics:
http://prosecco.gforge.inria.fr/personal/hritcu/temp/habil/catalin_habil.pdf#page=80

Candidates are expected to work collaboratively on project-relevant
topics and help advise students, but can also dedicate some of their
time to their own independent projects. For exceptional candidates
with enough experience we can also discuss about Starting Researcher
positions, who can propose and follow their own research agenda and be
fairly independent. Our team can also support such exceptional
candidates for permanent Researcher positions funded and awarded
competitively by Inria. Further details about these various positions
are available at https://secure-compilation.github.io/#positions

Do not hesitate to contact me if you are interested!

Regards,
Catalin


[TYPES/announce] Postdoc Position at the University of Minnesota

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

Dear All,

I am looking for postdocs for my group at the University of Minnesota, Twin
Cities, USA. The length is about 18-24 months but negotiable. The funding
can support a wide range of topics in type theory and programming language
theory. I am particularly interested in raising the rigor of computer
programs or mathematical proofs. To name a few possible research directions:

1. higher-dimensional type theory (e.g., cubical type theory)
2. mechanization of proofs (e.g., in homotopy theory)
3. property-based testing

I am open to other topics not on the list. Please check my website
https://favonia.org for the work I did. Teaching is not required, but we
can discuss it if you are interested. The start date is flexible though I
prefer early spring.

REQUIREMENT

You must have a Ph.D. in Computer Science, Mathematics, Philosophy, or some
related field when the job starts. I need your CV, your cover letter
(explaining your motivation) and two professional references.

PREFERENCE

Background in type theory or programming language theory, good publication
record, and experience in proof mechanization are all pluses.

HOW TO APPLY

If you are currently an employee of the University of Minnesota, use this
link:

https://hr.myu.umn.edu/jobs/int/328079

Otherwise, this is for everyone else:

https://hr.myu.umn.edu/jobs/ext/328079

DIVERSITY

We take diversity and inclusiveness seriously, which is an important reason
why I joined the University. I strongly encourage people of often
underrepresented groups (not just regarding race or gender) to consider
this position.

Best,
Favonia
they/them/theirs
http://favonia.org


[TYPES/announce] Postdoc position at Colorado in data-driven program analysis with potential industrial applications

2018-12-20 Thread Bor-Yuh Evan Chang
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The Programming Languages and Verification Group at the University of
Colorado Boulder (CUPLV) is looking for exceptional candidates for a
postdoctoral research associate working in the area of data-driven program
analysis. This position presents a unique opportunity for potential
industrial application in collaboration with GitHub.

The ideal candidate has a background in the area of programming languages
and verification, as well as being interested in extending his or her
research to machine learning.

The postdoctoral research associate will collaborate with professors
Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Sergio Mover, as well as
engineers at GitHub. The researcher will have an opportunity to lead a
project on program repair and will contribute to potential technology
transfer with our industrial partner.

To apply, please send an email to Bor-Yuh Evan Chang <
evan.ch...@colorado.edu> or Sriram Sankaranarayanan 
with a CV and contact information for two or three references.

Our group has active projects in areas such as the following:
  - program analysis
  - program synthesis
  - cyberphysical systems

Compensation is highly competitive and commensurate with experience.
Teaching opportunities will be available.

For more information about our group, please see .

Boulder, located at the base of the Rocky Mountains, is consistently
awarded top-rankings for health, education, and quality of life.  It is
also home to a concentration of high-tech industry and to a vibrant
start-up community. It is located 30 miles from downtown Denver.


[TYPES/announce] Postdoc Position Reminder

2018-11-29 Thread Mislove, Michael W
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,

This is a reminder that we have an open postdoc position in Quantum Programming 
Languages here at Tulane. The project goal is to devise models of high-level 
functional quantum programming languages that support recursion, including 
recursive types. We’re also interested in contextuality as a quantum resource. 
This is a part of a multi-university research project that includes a new team 
at the University of Maryland whose work on Hoare logics for quantum 
programming languages also is of interest. Details and application instructions 
can be found at https://apply.interfolio.com/56794 

  Thanks,
  Mike Mislove

===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===



smime.p7s
Description: S/MIME cryptographic signature


[TYPES/announce] Postdoc position: Symbolic tools for the formal verification of cryptographic protocols

2018-11-09 Thread Steve Kremer
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A 12-month position for post-doctoral research on

  Symbolic tools for the formal verification of cryptographic protocols

is available at the Inria Nancy / LORIA research center within the Inria
project team

PESTO: Proof techniques for security protocols [1]

as part of the ERC Grant

SPOOC: Automated Security Proofs of Cryptographic Protocols [2]

Security protocols are distributed programs that aim at ensuring
security properties, such as confidentiality, authentication or
anonymity, by the means of cryptography. Such protocols are widely
deployed, e.g., for electronic commerce on the Internet, in banking
networks, mobile phones and more recently electronic elections. As
properties need to be ensured, even if the protocol is executed over
untrusted networks (such as the Internet), these protocols have shown
extremely difficult to get right. Formal methods have shown very useful
to detect errors and ensure their correctness.

One generally distinguishes two families of security properties: trace
properties and observational equivalence properties. Trace properties
verify a predicate on a given trace and are typically used to express
authentication properties. Observational equivalence expresses that an
adversary cannot distinguish two situations and is used to model
anonymity and strong confidentiality properties.

The Tamarin prover [3] is a state-of-the art protocol verification tool
which has recently been extended to verify equivalence properties in
addition to trace properties. SAPIC [4] allows protocols to be specified
in a high-level protocol specification language, an extension of the
applied pi-calculus, and uses the Tamarin prover as a backend by
compiling the language into multi-set rewrite rules, the input format of
Tamarin. Tamarin and SAPIC have been successfully used to verify
standards such as TLS 1.3 and 5G AKA as well as industrial protocols
such as OPC UA. The objective of this postdoc is to contribute to the
development of the SAPIC/Tamarin toolchain, work on extensions and use
the tool(s) to analyse particular classes of protocols.

Successful candidates must have defended a PhD in computer science, or
expect to defend their PhD before taking up the position. Expected
qualifications are:

- solid knowledge of logic, proofs and/or formal verification techniques,
- solid programming experience, ideally with functional programming in
OCAML or Haskell.

Security knowledge is not required, but a plus.

Contacts:
Jannik Dreier (jannik.dre...@loria.fr)
Steve Kremer (steve.kre...@loria.fr)

Duration: 12 months (possibility to extend for another 12 months)
Starting date: September 1, 2019 (earlier date negociable)

The position is located at the Inria Nancy / LORIA research center in
Nancy, France, with over 430 researchers, engineers and technicians.
Nancy is a young (more than 45,000 students) city in eastern France with
a rich cultural life and a high quality of life. It is famous for its
Unesco World Heritage Site "Place Stanislas". Paris is only 1h30 by TGV,
Luxembourg, Germany and the Vosges mountains less than 1h30 by car.

Applications, including
- a motivation letter including your scientific and career projects,
- a CV describing your research activities (max. 2 pages),
- a short description of your best contributions (max. 1 page for max. 3
contributions including theoretical research, implementation or industry
transfer),
- your two best publications,
- if you have not defended yet, the list of expected members of your PhD
committee and the expected date of defense,

should be sent to the the addresses indicated above as two pdf files
(one for the publications, the other for the other documents).

Additionally, at least one recommendation letter from your PhD
advisor(s), and up to two additional letters of recommendation should be
sent directly by their authors to the email addresses indicated above.

Applications should be received by June 30, 2019, but applications
received later may still be considered.

Informal enquiries concerning the position are welcome.

[1] https://team.inria.fr/pesto/
[2] http://homepages.loria.fr/skremer/spooc/
[3] http://tamarin-prover.github.io/
[4] http://sapic.gforge.inria.fr/


[TYPES/announce] Postdoc position on the Mercedes project in Twente (Netherlands): Maximal Reliability of Concurrent and Distributed Software

2018-10-31 Thread m.huisman
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position on the Mercedes project in Twente (Netherlands):
Maximal Reliability of Concurrent and Distributed Software

University of Twente
Group: Formal Methods and Tools
Contact: Prof. Dr. Marieke Huisman 
(m.huis...@utwente.nl<mailto:m.huis...@utwente.nl>)

Job Description
You will be working on the Mercedes project, a 1,5 million euro personal grant 
for Marieke Huisman, funded by NWO.

Goal of the Mercedes project is to develop techniques to ensure the maximal 
reliability of concurrent and distributed software. In earlier projects, we 
started working on the development of a tool set for the verification of 
concurrent programs, called VerCors which is a result of Marieke Huisman’s 
earlier ERC project on verification of concurrent software. The VerCors tool 
set uses deductive program verification, i.e., the desired program properties 
are written in a pre-postcondition style (using a form of separation logic).

The focus of this Postdoc project will be on enabling verification of large 
programs with a significant concurrent aspect. Your ideas would be implemented 
in or should be applicable to the VerCors tool set. We value contributions to 
the theory of large-scale verification, to the process in which verification 
can be applied to large-scale software projects, and/or to the implementation 
of features that may have a significant impact on the usability of VerCors in 
the context of large scale verification.

For more information about the concrete project, please contact Marieke Huisman 
(m.huis...@utwente.nl<mailto:m.huis...@utwente.nl>).

We seek
We are looking for a researcher with an independent mind who is willing to 
cooperate in our team. It is understood that he or she works on the topics 
listed above. Further we ask for good communicative and collaboration skills. 
Candidates should be prepared to prove their English language skills.

As a research outcome we expect publications and (prototype) tools.

We offer
- One post doc position for two years (38 hrs/week), with a possibility of 
extension of upto 2 more years.
- A stimulating scientific environment
- Full status as an employee at the University of Twente, including pension and 
health care benefits.
- Gross salary for a Postdoc is dependent on experience and background, but 
will minimally be € 3.068,00 per month (scale 10.4), plus holiday allowance 
(8%) and end-of-year bonus (8.3%).
- Excellent facilities for professional and personal development.
- Good secondary conditions, in accordance with the collective labour agreement 
CAO-NU for Dutch universities
- A green Campus with lots of sports facilities

Further information
- FMT group: http://fmt.cs.utwente.nl/
- Prof. Dr. Marieke Huisman 
(m.huis...@utwente.nl)<mailto:m.huis...@utwente.nl)>: 
http://wwwhome.cs.utwente.nl/~marieke/
- Project webpage: http://fmt.ewi.utwente.nl/research/projects/Mercedes/

Application
To apply for the button, visit
https://www.utwente.nl/en/organization/careers/vacancy/!/423176/postdoc-position-on-the-mercedes-project-on-maximal-reliability-of-concurrent-and-distributed-software

Please use the Apply Now button at the bottom of the page.

Deadline: November 24, 2018. Earlier applications are welcome and an early 
start date is an advantage.

Your application should consist of:

- a cover letter (explaining your specific interest and qualifications);
- a full Curriculum Vitae,
  to apply for the PhD student position, this should include a list of
  all courses + marks, and a short description of your MSc thesis;
  to apply for the post doc position, this should include a list of
  all publications, and a short description of your PhD thesis;
- references (contact information) of two scientific staff members.




[TYPES/announce] Postdoc position on side-channel analysis and avoidance in Hardware (Chalmers University of Technology)

2018-10-18 Thread Alejandro Russo

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

-
Postdoctoral position (up to two years) on side-channel analysis and 
avoidance

in Hardware at Chalmers University of Technology, Sweden
-

* Important dates:

  October  30 - Deadline for applications
  November 5  - Tentative date for interviews

* Expected starting date: January 2019.

For details, including employment conditions and how to apply, see:



This position is funded by a grant from Intel Corp and will get 
supervised by
Prof. Carl-Johan Seger 
() and
Prof. Alejandro Russo (). Prof. 
Seger has,
after 21 years at Intel corporation, a wealth of experience in verifying 
Intel's

microprocessors and is intimately familiar with the constraints and scale of
modern processors. He also has extensive experience in building formal
verification tools, and symbolic simulators in particular, for modern
microprocessors. Prof. Russo has vast expertise on protecting privacy in 
modern
software systems and his work has impacted different research 
communities and
appeared in prestigious conferences on programming languages, operating 
systems,

and security.

The project is dedicated to contribute and further research on (i) utilizing
some notion of dependent types to verify security and the 
presence/absence of
side-channels in multi-cycle circuits, (ii) apply symbolic execution 
techniques

to boost accuracy when needed, (iii) implement a tool that combines these
techniques, and (iv) perform evaluations on state-of-the-art public domain
microprocessor designs.

The position is to be carried out within both the Information Security 
(iSec)
and Functional Programming (FP) research groups. Both groups combine 
world-class
researchers in language-based security and functional programming. In 
addition,

there is a strong type-theory research group that can be used as a source of
knowledge in dependent types. Competitive candidates will have a strong 
computer
science background, both theoretical and practical, with emphasis on 
programming

languages techniques; expertise in some of the areas of interests for this
position; a passion for high-quality software research and development; and
excellent analytical and communication skills. Prior publications are
meritorious. English is the working language for research in Chalmers's
Department of Computer Science and Engineering.

For a popular science description of the project, please refer to the 
following

link: https://www.chalmers.se/en/departments/cse/news/Pages/Intel.aspx



[TYPES/announce] PostDoc Position at UCLouvain in Formal Verificaion, Privacy, and Security

2018-10-17 Thread Thomas Wilson
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi Everyone,

A two years postdoc scholarship to work at UCLouvain with Axel Legay and
Thomas Given-Wilson. Further details below.

Regards,

- Thomas Given-Wilson


Position:
-

A two years postdoc scholarship to work at UCLouvain with Axel Legay and
Thomas Given-Wilson. Net salary between 2300 and 2500 euro after taxes,
social security included.

Main Competences: Formal verification, privacy, security.

Beneficial Competencies: software development, model checking,
information theory.

Starting date: February 2019 (flexible)


Objective of the Serums project:
--

In order to achieve high quality healthcare provision, it is
increasingly important to collect highly confidential and personal
medical data that has been obtained from a variety of sources, including
personal medical devices and to share this through a variety of means,
including public networks and other systems whose security cannot be
implicitly trusted. Patients rightly expect full privacy, except where
permission has been explicitly given, but they equally expect to be
provided with the best possible medical treatment. Evidence suggests
that integrating home-based healthcare into a holistic treatment plan is
more cost effective, reduces travel-associated risks and costs, and
increases the quality of healthcare provision, by allowing the
incorporation of more frequent home-, work- and environment-based
monitoring and testing into medical diagnostics. There is thus a strong
and urgent demand to deliver better, more efficient and more effective
healthcare solutions that can achieve excellent patient-centric
healthcare provision, while also complying with increasingly strict
regulations on the use and sharing of patient data. This provision needs
to be multi-site, crossing traditional physical and professional
boundaries of hospitals, health centres, home and workplace, and even
national borders. It needs to engage hospitals, medical practitioners,
consultants and other specialists, as well as incorporating
patient-provided data that is produced by personal monitoring devices,
healthcare apps, environmental monitoring etc. This creates huge
pressures. The goal of the Serums project is to put patients at the
centre of future healthcare provision, enhancing their personal care,
and maximising the quality of treatment that they can receive, while
ensuring trust in the security and privacy of their confidential medical
data.

 

UCLouvain's role in the project:
---

The objective of this postdoc position is to develop new security proofs
to ensure correctness of security properties developed in Sérums.

In addition, the postdoc will participate to development of new research
to guarantee privacy of data and evaluate solutions developed by the
consortium.


How to apply:
--

Contact Axel Legay at axel.le...@uclouvain.be with a CV and, if
possible, a letter of recommendation

 
For more information:
--

Contact Axel Legay at axel.le...@uclouvain.be



signature.asc
Description: OpenPGP digital signature


[TYPES/announce] Postdoc position in Safety control and energy efficiency for embedded systems

2018-08-30 Thread Jalil Boudjadar
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position in Safety control and energy efficiency


The Department of Engineering at Aarhus University is inviting applications for 
a 18-months postdoctoral position within Safety control and energy efficiency 
for hybrid propulsion systems.
The research is a part of an innovative industrial project focusing on 
combining different environmental-friendly energy sources for zero-emission 
marine applications.

The position is available from November 1st 2018, or as soon as possible 
hereafter.

Propulsion of ships pollutes through emission of CO2 and harmful particles when 
operated by diesel engines. Electrification of ship propulsion is a way to 
introduce clean tech-solutions in the transport sector of special interests in 
harbors and costal zones. This project addresses the hybrid electrical 
propulsion of ships where the electrical power is partly supplied from 
batteries and partly generated on-board by means of fuel cells fueled by 
hydrogen. The ultimate goal of the position work package is to specify and 
analyze the safety control and develop an efficient scheduling of the energy 
sources, according to the real-time sealing conditions, to optimize the 
performance and resource consumption.

Tasks
The primary task of the Postdoc researcher is to develop a proof of concept for 
the safety control and power management systems for a maritime solution 
combining two energy sources: battery and fuel-cell electric technology. This 
task includes:


  *   Specification and testing of the safety control algorithms for individual 
subsystems, integration and formal verification.
  *   Specification of the different energy sources (fuel cell, battery) supply 
balancing.
  *   Investigation on certification regulations, in particular those related 
to Safety and Integrity Levels SILs of IEC61508 Standard.
  *   Risk assessment.
Your profile
Applicants should hold a PhD in Computer Science/Engineering, Control and 
automation, or a related subject.

The applicant should have experience/background with the following topics:


  *   Formal specification and verification of control systems.
  *   Energy and performance modeling and analysis.
  *   Model-based design and optimization.
  *   Be interested in Real-time scheduling.
About the Electrical and Computer Engineering Section
Electrical and computer engineering are closely related engineering disciplines 
that focus on the development of hardware and software for intelligent units 
and networks. This includes hardware at system and component levels as well as 
many different types of software for controlling electronic devices and 
networks.

The research areas within the Electrical and Computer Engineering Section at 
Department of Engineering support the development within this area. The outcome 
greatly influences our daily lives as advanced technologies are incorporated 
into an increasing number of products, for example in industrial processes, at 
hospitals and in information infrastructures.

Place of Employment and Place of Work
The place of employment is Aarhus University, and the place of work is Science 
and Technology, Finlandsgade 22, 8200 Aarhus N., Denmark.
The postdoctoral researcher will be a part of the Software Engineering group.

More information
For further information please contact Dr. Jalil Boudjadar 
(ja...@eng.au.dk<mailto:ja...@eng.au.dk>).

Deadline
All applications must be made online and received by: 30.09.2018

Position link and where to apply: 
http://www.au.dk/en/about/vacant-positions/scientific-positions/stillinger/Vacancy/show/1001819/5283/



[TYPES/announce] Postdoc position at Paris Diderot University

2018-07-06 Thread Alexis Saurin IRIF
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

RAPIDO -- Reasoning And Programming with Infinite Data-Objects.
(http://www.irif.fr/~saurin/RAPIDO)

* postdoc positions in RAPIDO project:

We are opening a post-doc position in RAPIDO project, which is aimed
at studying logical methods and tools for enhancing reasoning and
programming on infinite data.
The post-doc would start sometimes during the fall 2018 (start date
between october 2018 and january 2019).

RAPIDO is an ANR-funded project hosted at Paris Diderot University
involving researchers from three french labs: IRIF (Univ Paris Diderot),
LIP (ENS Lyon) and LSV (ENS Paris Saclay). It is coordinated by Alexis
Saurin (IRIF lab, sau...@irif.fr) and the post-doc position will
administratively be hosted by Paris Diderot University.

RAPIDO aims at gathering young researchers to investigate the
applicability of proof-theoretical methods to reason and program on
infinite data objects. The goal of the project is to develop logical
systems capturing infinite proofs (proof systems with least and greatest
fixed points as well as infinitary proof systems), to design and to study
programming languages for manipulating infinite data such as streams both
from a syntactical and semantical point of view. Moreover, the ambition of
the project is to apply the fundamental results obtained from the proof-
theoretical investigations (i) to the development of software tools
dedicated to the reasoning about programs computing on infinite data,
e.g. stream programs (more generally coinductive programs), and (ii) to
the study of properties of automata on infinite words and trees from a
proof-theoretical perspective with an eye towards model-checking problems.

* Topics and requirements for applicants

We are looking for young researchers who can contribute to the research
topics of RAPIDO. Candidates should hold a PhD in computer science or a
closely related field (or be close to complete their PhD) with skills in
formal methods and logic and a strong expertise in at least one of the
following topics:
*
  automata theory, coinduction, cyclic and infinitary
  proofs, denotational semantics, functional programming,
  games and game semantics, infinitary rewriting, lazy
  evaluation, linear logic, MSO logic, proof assistants,
  proof theory, realizability, streams, temporal logics.
*
We will be particularly interested in applications of candidates having
an experience using the Coq proof assistant, but this is not a
requirement for applying!

* Important dates:

Informal enquiries: as soon as possible
Application deadlines: july 18th 2018
Starting date: between october 2018 and january 2019.

* Application submission guidelines

Applications should be sent to Alexis Saurin before July 18th 2018
in an email entitled "RAPIDO postdoc application", providing:
- a detailed CV with a publication list,
- a research statement of at most two pages plus bibliography,
- and one or two recommendation letters.

Potential candidates are strongly encouraged to contact the project
coordinator (together with other project members) for informal
enquiries as soon as the announcement is released, and at least when
*starting* preparing their application (for info on topics such as starting
dates, connections with project sites, salary...).

More informations on the post-doc position available at:
https://www.irif.fr/~saurin/RAPIDO/files/post-doc-announcement-2018.txt

Best,

Alexis

-- 
Alexis Saurin
CNRS researcher, IRIF


[TYPES/announce] postdoc position at Chalmers | University of Gothenburg

2018-07-03 Thread Thorsten Berger

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

Postdoc position in the area of software variability (with strong ties 
to robotics and embedded/cyber-physical systems). Apply by *July 5*. We 
are looking for a candidate with a good formal background, including 
experiences with Functional Programming, Model-Driven Engineering. and 
Formal Methods.


OVERVIEW

Employment: Fixed-term, 2 years
Extent: 100 % of full time
Location: Department of Computer Science and Engineering / Division of 
Software Engineering, Chalmers | University of Gothenburg

First day of employment: As soon as possible
Applications via: 
https://www.gu.se/english/about_the_university/job-opportunities/vacancies-details/?id=2776

Application deadline: July 5 CEST (strict)


GENERAL INFORMATION

The department of Computer Science and Engineering is jointly hosted by 
Chalmers University of Technology and the University of Gothenburg. It 
is a strongly international department with approximately 80 faculty 
among a total of 260 employees originating from 30 countries. Located in 
Gothenburg -- Sweden’s second-largest city -- the department is 
surrounded by a vibrant ecosystem of software-intensive companies, such 
as Volvo Cars and Volvo AB, Ericsson, ABB, Boeing, and SAAB Aeronautics. 
The department is connected to three science parks in Gothenburg for 
industrial collaborations in fields including intelligent vehicles and 
transport systems, mobile internet, energy, nanotechnology, and life 
sciences. Alumni and members of the department have also created many 
startups, including revolutionary ones such as Spotify.


The announced postdoc position is located at the division of Software 
Engineering. With 21 faculty members it is arguably one of the largest 
software-engineering institutes world-wide, conducting research at the 
highest international level in topics such as model-driven engineering, 
testing, software product lines, empirical software engineering, 
requirements engineering, autonomic computing, and cloud computing. This 
year, the division organizes two of the most influential 
software-engineering conferences, ICSE’18 and SPLC’18. For industrial 
research, the division hosts the Software Center, an associated 
institute with a network of five universities and ten global companies 
including Siemens, Axis, and Jeppesen.



JOB ASSIGNMENTS

The postdoctoral researcher will conduct research in the areas of 
software product-line engineering, model-driven engineering or empirical 
software engineering. The position is embedded into the EU ITEA project 
REVAMP with a focus on re-engineering and migration of variant-rich 
systems into modern and scalable product-line architectures. It is also 
closely related to the EU project Co4Robots where modern variability 
mechanisms (including dynamic variability and adaptation mechanisms) 
will be conceived for robotics and cyber-physical systems. The primary 
job assignment is research, with excellent collaboration opportunities 
with the project partners, including SCANIA, ABB, SAAB, ALTRAN, PAL 
Robotics, and Bosch, among potentially other European partners. The 
position includes 10-20% teaching (negotiable) at the Software 
Engineering division by supervising Master theses and supporting courses 
as a teaching assistant.


Applicants must have a PhD degree in Computer Science, Software 
Engineering or a closely related discipline. Prior publications, 
excellent references, fluency in English as well as good communication, 
collaboration, self-organization, and programming skills are also required.



APPLICATION

Applications are to be written in English and need to contain:
- Cover letter expressing the applicant’s motivation, experiences, and 
relevant qualifications in relation to the announced position
- Detailed curriculum vitae including publications, teaching 
experiences, and three references with their contact details
- Official transcripts of education certificates (degrees, including 
grade reports and other documents when applicable).


Applications only online by July 5 (end of day CEST, strict) via:
https://www.gu.se/english/about_the_university/job-opportunities/vacancies-details/?id=2776

Please contact Thorsten Berger (contact information below) for questions 
about the position.


--
Thorsten Berger
Associate Professor

Department of Computer Science and Engineering
Chalmers | University of Gothenburg, Sweden
http://www.cse.chalmers.se/~bergert
Tel.: +46 (0) 31 772 6075
Mob.: +46 (0) 729 746 246
Skype: tberger.work



[TYPES/announce] Postdoc position in Logic

2018-06-05 Thread Iemhoff, R. (Rosalie)
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc position in Logic at Utrecht University, the Netherlands.
 
The postdoc is embedded in the research project “Optimal Proofs”  funded by the 
Netherlands Organization for Scientific Research led by Dr. Rosalie Iemhoff, 
Department of Philosophy and Religious Studies, Utrecht University. The project 
in mathematical and philosophical logic is concerned with formalization in 
general and proof systems as a form of formalization  in particular. Its 
mathematical aim is to develop methods to describe the possible proof systems 
of a given logic and establish, given various criteria of optimality, what the 
optimal proof systems of the logic are. Its philosophical aim is to develop 
general criteria for faithful formalization in logic and to thereby distinguish 
good formalizations  from bad ones.  The mathematical part of the project 
focusses on, but is not necessarily restricted to, the (non)classical logics 
that occur in computer science, mathematics, and philosophy, while the 
philosophical part of the project also takes into account domains where 
formalization in logic is less common. The postdoc is expected to contribute 
primarily to the mathematical part of the project. Whether the research of the 
postdoc also extends to the philosophical part of the project depends on his or 
her interests. 

Qualifications

We are looking for a talented and dedicated researcher with a PhD in logic, 
preferably in mathematical or philosophical logic, with excellent track record 
and research skills relative to experience,  excellent academic writing and 
presentation skills, and publications in high-level  journals or books. 

Additional information

For more information on the practical details of the positions and the 
application procedure , please visit 
https://www.academictransfer.com/nl/47996/postdoc-position-in-logic-10-fte/
https://www.uu.nl/en/organisation/working-at-utrecht-university/jobs
For more information on the project, please contact Rosalie Iemhoff at 
r.iemh...@uu.nl.

 Deadline for applications: 22 June, 2018.



[TYPES/announce] Postdoc position in formal verification for formal compositional contracts

2018-05-16 Thread Łukasz Czajka
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Deon Digital and DIKU are looking for a postdoc in formal verification
for formal compositional contracts in a domain-specific language
specifying rules (obligations, permissions, prohibitions) without
conflating these with specific execution strategies (as done in smart
contracts). Contracts are hosted on a variety of
blockchain/distributed ledger systems. The postdoc is to develop
proof-assisted semantic foundations and verification technology (for
example--but not necessarily--in Coq) for guaranteed sound contract
analysis and reasoning, ranging from basic security and privacy
properties to quantitative analysis of resources and time constraints
to guard against both errors and traps in (smart) contracts.

Application: Now until June 10th, 2018.

Position: The postdoc is a 2-year position co-funded by Deon Digital
and the Danish Innovation Foundation; it carries a competitive salary,
advantageous tax status for researchers moving to Denmark, and shares
in Deon Digital; it is automatically converted into a permanent
position at Deon Digital after the postdoc period. The postdoc will
work with Prof. Fritz Henglein and his colleagues at the Programming
Languages and Theoretical Computer Science section at DIKU; and with
Dr. Jesper Andersen at Deon Digital Denmark and his team at Deon
Digital Denmark (all of whom are computer scientists with a background
in semantics-based programming language theory and technology).

Requirements: Relevant Ph.D. in computer science, awarded by end of
June 2018, with documented high research quality.  Maximum 6 months of
work in private sector since start of Ph.D. studies (requirement by
funding agency).  Interest in working in congenial, self-organizing
environments at both Deon Digital and DIKU.  Flexible remote work from
home is possible in the beginning, but an eventual move to Copenhagen
is expected.

Application: If you are interested in the position, please send your
CV, 1-3 papers, and (links to some of) your open source software
contributions (if any) by email to Fritz Henglein, hengl...@diku.dk.
The position is open now.  Applications will be accepted from now
until June 10th, 2018; they will be processed on an ongoing
(first-come) basis.

DIKU (diku.dk) is the Department of Computer Science at the University
of Copenhagen with 40+ junior and senior faculty researching
fundamentals and applications of algorithms, programming languages and
systems, data science, machine learning, image processing,
human-computer interaction, and more.  DIKU's research is consistently
ranked highly.   Its newly formed section on Programming Languages and
Theoretical Computer Science is located on the North Campus in
Copenhagen, 15 minutes (by bicycle or public transportation) from Deon
Digital's R center.

Deon Digital (deondigital.com) is a rapidly growing Zürich-based
start-up developing domain-specific language technology for
blockchain/distributed ledger-hosted contracts, with applications in
finance, insurance, pensions, mobility (transportation), logistics,
supply chain, commodity trading and more.  Its research and
development center is located in the Christianshavn section of
Copenhagen, close to DIKU, the city center and 10 minutes from
Copenhagen airport.


[TYPES/announce] PostDoc Position on Formally Secure Compilation at Inria Paris

2018-04-09 Thread Catalin Hritcu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A Postdoctoral Researcher position is available on my secure
compilation project at Inria Paris. The project is aimed at building
the first formally secure compilation chains for realistic programming
languages like C. Such compiler chains will ensure that high-level
abstractions cannot be violated even when interacting with untrusted
low-level code or when some program components were compromised.

I am seeking exceptional candidates with a strong, internationally
competitive track record of research in programming languages, formal
verification, or security. Particularly interesting areas include:

- formal verification in a proof assistant like Coq and
  verified compilation in particular

- security foundations, e.g., reference monitoring, hyperproperties,
  noninterference, fully abstract translations

Candidates are expected to work collaboratively and help advise students.

Please see the project web page (https://secure-compilation.github.io)
for more details about the project and about such open positions.
Do not hesitate to contact me if you are interested in joining the team!

Best Regards,
Catalin Hritcu


[TYPES/announce] Postdoc position in Logic, Gothenburg (Sweden), Deadline: 31st May 2018

2018-03-31 Thread Graham Leigh
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

POSTDOC POSITION IN LOGIC, GOTHENBURG (SWEDEN)
* University of Gothenburg, Sweden
* Duration: 2 years, starting Autumn 2018
* Deadline for applications is 31st May 2018
* The Department of Philosophy, Linguistics and Theory of Science at University 
of Gothenburg is inviting applications for a Postdoc position in Logic. Topics 
of interest include proof-theoretic studies of reflection and induction, 
axiomatic theories of truth, type-theoretic foundations, and fixed-point 
calculi such as the modal mu-calculus.
* For full details see 
http://www.gu.se/english/about_the_university/job-opportunities/vacancies-details/?id=1637


[TYPES/announce] Postdoc position in Orsay, France

2018-03-15 Thread Sylvie Boldo

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

Hello,

I would like to advertise a postdoc position available in Orsay, France.
The goal is to develop formal proofs about the floating-point evaluation of 
polynomials and is within the FastRelax project

  http://fastrelax.gforge.inria.fr/


To see details and to apply, please go to
  https://jobs.inria.fr/public/classic/en/offres/2018-00418

Do not hesitate to forward this email to any appropriate candidate or
mailing list.

Best regards,

Sylvie Boldo

--
Sylvie Boldo, Toccata project, Inria Saclay - Île-de-France
PCRI, Bât. 650 - Université Paris-Sud - 91405 ORSAY Cedex


[TYPES/announce] postdoc position at Inria Rennes

2018-03-05 Thread Alan Schmitt
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The CELTIQUE team (https://team.inria.fr/celtique/) has a postdoc
position available on the compilation of recursive functions to
inductive definitions in Coq.

To see details and to apply, please go to
https://jobs.inria.fr/public/classic/en/offres/2018-00432.

Do not hesitate to forward this email to any appropriate candidate or
mailing list.

Best regards,

Alan Schmitt

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-01: 407.98, 2017-01: 406.13


signature.asc
Description: PGP signature


[TYPES/announce] Postdoc position at the Pennsylvania State University

2017-09-29 Thread Gang Gary Tan

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

Postdoc position at Penn State Computer Science and Engineering

Applications are invited for a full-time postdoctoral researcher
position in the Security of Software (SOS) Lab at Penn State
(http://www.cse.psu.edu/~gxt29/sos/).  The SOS Lab focuses on
methodologies that help create secure software systems.  We are
seeking a highly qualified individual to work in the area of software
security, including binary code analysis and hardening as well as
compiler-based software security.  An applicant should possess a
doctoral degree in Computer Science or Computer Engineering and have
strong background in computer security, programming languages, or
formal methods.  The candidate must have an excellent track record of
original research and the ability to work as part of a team.

The postdoc will be provided with competitive salary and employment
benefits. The initial appointment will be for one year, with an option
to renew for a second year.

Inquiries about the position should be directed to Dr. Gang Tan
(g...@cse.psu.edu).  Applicants should send a resume with at least two
names of references. Applications will be reviewed until the position
is filled.

Penn State is a major research university ranked 3rd in U.S.  in
industry-sponsored research.  The CSE department is ranked 8th in
U.S. in research expenditures and has strong research programs in
security.  The U.S. News and World Report consistently ranks Penn
State's College of Engineering undergraduate and graduate programs
among the top in the nation.

--
Gang (Gary) Tan
Associate Professor, CSE Department
Penn State University
W358 Westgate Building
http://www.cse.psu.edu/~gxt29/
Tel: 814-8657364, Fax: 814-8653176


[TYPES/announce] Postdoc Position in Program Verification at Carnegie Mellon University, Silicon Valley

2017-08-01 Thread Pasareanu, S Corina (ARC-TI)[SGT, INC]
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

A post-doctoral researcher position focusing on symbolic verification 
techniques for cyber-security is available at Carnegie Mellon University at the 
Silicon Valley Campus (Mountain View, CA). The research project titled 
"Integrated Symbolic execution for Space-Time Analysis of Code (ISSTAC)" 
involves symbolic execution of Java Bytecode for automatically identifying (1) 
denial of service attacks (by determining worst case complexity of a program in 
terms of both time and space usage) and (2) side channel attacks (by 
determining if observations about the execution time or memory usage of a 
program can leak secret information). This is a multi-year collaborative effort 
with researchers from Vanderbilt University, University of California at Santa 
Barbara and Queen Mary University, London. There are many research directions 
within the scope of this project, including constraint solving and model 
counting techniques, heuristics for scalable symbolic program analysis, 
automated worst-case behavior analysis, quantitative information flow using 
symbolic execution, attack and defense synthesis, distributed computations, 
combinations of symbolic execution and fuzzing, etc.


Candidates for the post-doctoral position should have a doctoral degree in 
computer science (or related field) and should have familiarity with symbolic 
execution techniques and SMT-solvers. Security knowledge is a plus. Candidates 
interested in this position should e-mail a CV, brief statement of research 
interests and a reference (with e-mail address) to Corina Pasareanu 
(corina.pasare...@west.cmu.edu).

The position is available now and will be open until filled. You can find more 
information about the ISSTAC project here 
http://www.cmu.edu/silicon-valley/research/isstac/.



[TYPES/announce] Postdoc position at the University of Lisbon (2nd call)

2017-06-22 Thread vv@di
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We welcome applications for a fulltime postdoctoral research position
at the University of Lisbon.

The position is funded by the research project "CONFIDENT -
Communication Contracts for Distributed Systems Development",
http://gloss.di.fc.ul.pt/content/confident, a three year collaborative
project between a team at the Faculty of Sciences (including Vasco T.
Vasconcelos and Antónia Lopes) and another at Tecnico (Paulo Mateus
and Pedro Adao).

The objective of the project is the development of tools and
technology for describing, testing, statically verifying, and
inferring communication contracts for the effective construction and
evolution of complex distributed systems, notably RESTful
applications. Particular attention will be given to the validation of
security requirements of APIs. We plan to integrate the theory of
behavioural type systems into a notion of communication contracts,
effective in driving the software development life cycle of RESTful
applications.

We seek applicants with strong interest in some of the following
topics: programming language design and implementation, programming
logics and types, language-based security, verification and testing,
concurrency and distribution.

The contract is for one year, extensible for a second year.
Applicable administrative rules may be found at the FCT site,
http://www.fct.pt/apoios/bolsas/index.phtml.en.

Applications should include a curriculum vitae in pdf format, contact
details for three referees, and should be sent to

LaSIGE - Large-Scale Informatics Systems Laboratory
http://www.lasige.di.fc.ul.pt
Email: Pedro Gonçalves, pgoncal...@di.fc.ul.pt
Phone: +351 21 750 05 32

Interested applicants are encouraged to contact Professor Vasco
T. Vasconcelos directly.

Application deadline: 30th June 2017



[TYPES/announce] Postdoc Position at DePaul University

2017-05-19 Thread James Riely
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Postdoc Position at DePaul University

We invite applicants for a postdoc position at DePaul University, School of
Computing.  The appointment is for a one academic year, with full
benefits, and is renewable for up to two years.

The postdoc will be working on the project NSF funded project: Relaxing
Soundness https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617175 under PIs
James Riely and Radha Jagadeesan.

It would be desirable for applicants to have expertise in one or more of the
following:
+ Concurrency theory
+ Relaxed memory models
+ Distributed databases and data structures
+ Programming Languages
+ Automated theorem provers

Applications should include CV, statement of teaching interests, a
cover letter, and three letters of recommendation that, preferably, address
the candidate's teaching qualifications or potential.

Contact James Riely or Radha Jagadeesan for additional inquiries at {jriely,
rjagadeesan}@cs.depaul.edu


[TYPES/announce] Postdoc position at the University of Lisbon

2017-05-10 Thread Vasco T. Vasconcelos
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We welcome applications for a fulltime postdoctoral research position
at the University of Lisbon.

The position is funded by the research project "CONFIDENT -
Communication Contracts for Distributed Systems Development",
http://gloss.di.fc.ul.pt/content/confident 
, a three year collaborative
project between a team at the Faculty of Sciences (including Vasco T.
Vasconcelos and Antónia Lopes) and another at Técnico (Paulo Mateus
and Pedro Adão).

The objective of the project is the development of tools and
technology for describing, testing, statically verifying, and
inferring communication contracts for the effective construction and
evolution of complex distributed systems, notably RESTful
applications. Particular attention will be given to the validation of
security requirements of APIs. We plan to integrate the theory of
behavioural type systems into a notion of communication contracts,
effective in driving the software development life cycle of RESTful
applications.

We seek applicants with strong interest in some of the following
topics: programming language design and implementation, programming
logics and types, language-based security, verification and testing,
concurrency and distribution.

The contract is for one year, extensible for a second year.
Applicable administrative rules may be found at the FCT site,
http://www.fct.pt/apoios/bolsas/index.phtml.en 
.

Applications should include a curriculum vitae in pdf format, contact
details for three referees, and should be sent to

LaSIGE - Large-Scale Informatics Systems Laboratory
http://www.lasige.di.fc.ul.pt 
Email: Pedro Gonçalves, pgoncal...@di.fc.ul.pt 
Phone: +351 21 750 05 32

Interested applicants are encouraged to contact Professor Vasco
T. Vasconcelos directly.

Application deadline: 30th June 2017.

[TYPES/announce] Postdoc position at MPI-SWS, Kaiserslautern, Germany

2017-05-08 Thread Maria Christakis
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a full-time postdoctoral research

position at the Max Planck Institute for Software Systems (MPI-SWS)

based at Kaiserslautern, Germany, under the supervision of Maria

Christakis (https://mariachris.github.io/).

 

MPI-SWS offers an internationally renowned research community as well

as a multicultural and open working environment. Maria has recently

won the prestigious EAPLS Best Dissertation Award and is excited to

continue her work on Practical Formal Methods with a talented and

motivated postdoctoral researcher.

 

The initial postdoc appointment is for two years, starting anytime

after October 2017, with an option to extend to a third year

(depending on performance).

 

The position is relatively independent in that it is not tied to a

specific project and there is considerable freedom to choose a

research topic. Nevertheless, the postdoc is expected to collaborate

closely with other researchers in the group. Thus, the main topics of

interest are:

- defect analysis of smart contracts

- collaborative verification and testing

- systematic testing of large programs

- practical concurrency error detection

 

The successful candidate will have a strong background in at least one

of the following areas:

- automatic test generation

- software verification

- static and/or dynamic program analysis

- security

 

Qualified candidates are encouraged to contact Maria directly by

e-mail (maria AT mpi-sws DOT org), and in addition, submit a formal

online application at:

 

  https://apply.mpi-sws.org/

 

The application consists of a CV, a research statement, and a list of

referees.

 

Application deadline: Friday, 14 July.



[TYPES/announce] Postdoc Position at Queen Mary

2017-04-10 Thread Nikos Tzevelekos

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

We are hiring one research fellow with a strong background in 
programming languages and verification, who can contribute to the design 
and implementation of a Java heterogeneous compilation tool, informed by 
semantic models.


The deadline for applications is 08 MAY 2017.

The position is for 12 months with the possibility of extension to 30 
months. It is based in the School of Electronic Engineering and Computer 
Science, Queen Mary University of London, under the supervision of Nikos 
Tzevelekos, and is part of a joint project with Dan Ghica and the 
University of Birmingham.


The project is financed by the EPSRC grant "System-Level Game Semantics: 
A semantic framework for composing systems”, in collaboration with 
external partners Aarhus University, Yale University, and Facebook.


Informal inquiries can be sent to nikos.tzevele...@qmul.ac.uk.
Job link: http://bit.ly/2ohUkEM

Please share.


Nikos Tzevelekos
Senior Lecturer in Computer Science
Queen Mary University of London

Valuing Diversity & Committed to Equality
QMUL is proud to be a London Living Wage Employer


[TYPES/announce] Postdoc position in proof theory in Paris

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


  Postdoc position in proof theory in Paris


There is an opening of a postdoc position on structural and
computational proof theory. The position is financed by
the ANR within the project FISP.

<https://www.lix.polytechnique.fr/~lutz/orgs/FISP.html>

The postdoc will be hosted by INRIA and the Laboratoire d'Informatique
(LIX) at the Ecole Polytechnique, one of the "Grand Ecoles" in the French
university system, located in the suburbs of Paris.

The successful candidate will be working within the PARSIFAL team.

<http://team.inria.fr/parsifal/>

Starting date should be in Fall 2017.

Applicants must have a Ph.D. or equivalent in computer science or
mathematics, and should have a strong background in proof theory
and related topics. The principal responsibility of the postdoc
will be to carry out research in the area of proof theory within the
FISP project. There are no teaching duties.

For further information, see
<http://www.lix.polytechnique.fr/~lutz/orgs/fisp-postdoc.html>

or contact
Lutz Strassburger <l...@lix.polytechnique.fr>

Applications should be sent via email to Lutz Strassburger
<l...@lix.polytechnique.fr> and should include a CV, a research
statement (1-2 pages), and one or two recommendation letters. The
application deadline is

*** April 16, 2017 ***





[TYPES/announce] Postdoc position at IT University of Copenhagen

2017-02-03 Thread Rasmus Ejlers Møgelberg
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

I would like to advertise a 2-year postdoc position available at the IT 
University of Copenhagen, Denmark. The suggested starting date is August 2017, 
but this is negotiable. The position is part of my research project Type 
Theories for Reactive Programming funded by Villum Fonden, and running for 5 
years involving 2 PhDs and 2 postdoc positions in total. I include a short 
description of the goals of the project below.

Applicants should have experience with category theory and denotational 
semantics. Knowledge of models of (dependent) type theory or functional 
reactive programming is an advantage, but is not required.

The deadline for application is February 28. Further information on the 
position and how to apply can be found here:
http://bit.ly/2kl7zRy

I encourage all interested in applying to contact me in advance.

Rasmus Møgelberg

-

Project description

Type theories are formal systems that can be viewed both as programming 
languages and logical systems for formalised mathematics. From a computer 
science perspective, this is useful because it allows for programs, their 
specifications, and the proofs that these satisfy the specification to be 
expressed in the same formalism.

The logical interpretation of type theories means that all programs must 
terminate. For this reason, programming and reasoning about non-terminating 
reactive programs in type theory remains a challenge. This is unfortunate since 
these include many of the most critical programs in use today.  In this 
project, we aim to design a new type theory useful for programming with and 
reasoning about reactive programs.
We build on recent progress in guarded recursion and functional reactive 
programming, using modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an 
extension of Cubical Type Theory with guarded recursive types. These can be 
used for smooth programming with coinductive types and construction of models 
of advanced programming languages. This part of the project is a collaboration 
with professor Lars Birkedal at Aarhus University.

Type theories are formal systems that can be viewed both as programming 
languages and logical systems for formalised mathematics. From a computer 
science perspective, this is useful because it allows for programs, their 
specifications, and the proofs that these satisfy the specification to be 
expressed in the same formalism.

The logical interpretation of type theories means that all programs must 
terminate. For this reason, programming and reasoning about non-terminating 
reactive programs in type theory remains a challenge. This is unfortunate since 
these include many of the most critical programs in use today.
In this project, we aim to design a new type theory useful for programming with 
and reasoning about reactive programs.
We build on recent progress in guarded recursion and functional reactive 
programming, using modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an 
extension of Cubical Type Theory with guarded recursive types. These can be 
used for smooth programming with coinductive types and construction of models 
of advanced programming languages. This part of the project is a collaboration 
with professor Lars Birkedal at Aarhus University.
- See more at: 
https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180828=5#sthash.uggmBukd.dpu
Project description
Type theories are formal systems that can be viewed both as programming 
languages and logical systems for formalised mathematics. From a computer 
science perspective, this is useful because it allows for programs, their 
specifications, and the proofs that these satisfy the specification to be 
expressed in the same formalism.

The logical interpretation of type theories means that all programs must 
terminate. For this reason, programming and reasoning about non-terminating 
reactive programs in type theory remains a challenge. This is unfortunate since 
these include many of the most critical programs in use today.
In this project, we aim to design a new type theory useful for programming with 
and reasoning about reactive programs.
We build on recent progress in guarded recursion and functional reactive 
programming, using modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an 
extension of Cubical Type Theory with guarded recursive types. These can be 
used for smooth programming with coinductive types and construction of models 
of advanced programming languages. This part of the project is a collaboration 
with professor Lars Birkedal at Aarhus University.
- See more at: 

[TYPES/announce] Postdoc position at the University of Lisbon

2017-01-29 Thread Vasco T. Vasconcelos
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

***  Post-doc opening on Communication Contracts for Distributed
Systems Development ***

We welcome applications for a fulltime postdoctoral research position
at the University of Lisbon.

The position is funded by the research project "CONFIDENT -
Communication Contracts for Distributed Systems Development",
http://gloss.di.fc.ul.pt/content/confident 
, a three year collaborative
project between a team at the Faculty of Sciences (including Vasco T.
Vasconcelos and Antónia Lopes) and another at Técnico (Paulo Mateus
and Pedro Adão).

The objective of the project is the development of tools and
technology for describing, testing, statically verifying, and
inferring communication contracts for the effective construction and
evolution of complex distributed systems, notably RESTful
applications. Particular attention will be given to the validation of
security requirements of APIs. We plan to integrate the theory of
behavioural type systems into a notion of communication contracts,
effective in driving the software development life cycle of RESTful
applications.

We seek applicants with strong interest in some of the following
topics: programming language design and implementation, programming
logics and types, language-based security, verification and testing,
concurrency and distribution.

The contract is for one year, extensible for a second year.
Applicable administrative rules may be found at the FCT site,
http://www.fct.pt/apoios/bolsas/index.phtml.en 
.

Applications should include a curriculum vitae in pdf format, contact
details for three referees, and should be sent to

LaSIGE - Large-Scale Informatics Systems Laboratory
http://www.lasige.di.fc.ul.pt 
Email: Pedro Gonçalves, pgoncal...@di.fc.ul.pt 
Phone: +351 21 750 05 32

Interested applicants are encouraged to contact Vasco T. Vasconcelos
directly.

Application deadline: 28th February 2017.

Re: [TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

2017-01-12 Thread Peter Sewell
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

On 15 December 2016 at 23:20, Peter Sewell 
wrote:

> [please circulate this to any likely candidates - thanks, Peter]
>
> Research Associate/Senior Research Associate in Applied Semantics for
> Production Architectures
>

Updating this: the likellihood of new funding means we may be able to make
several appointments, to build a really strong team.   Closing date 24 Jan,
as before.

Peter



> University of Cambridge Computer Laboratory
> Research Associate £29,301 - £38,183 or Senior Research Associate £39,324
> - 49,772
> Fixed-term: until February 28, 2019, when the grant funding the post
> currently ends.
> Details: http://www.jobs.cam.ac.uk/job/12397/
>
>
> Do you want to help build mathematically rigorous foundations for
> real-world computing, to make it more robust and secure?
>
> We have an ongoing project to establish rigorous semantic models for
> production multiprocessors, to provide a clear basis for programming,
> software verification, and hardware verification. This involves long-term
> close collaborations with ARM and IBM, and we have an agreement with ARM to
> take their internal ISA description, build a mathematical model based on
> it, integrate it with the concurrency semantics we are developing, and
> release the whole in a form usable for verification. This will provide the
> first strongly validated public model for a production multiprocessor
> architecture. We also have a close collaboration with the CHERI research
> project, developing processors with hardware-accelerated in-process memory
> protection and sandboxing, together with an open-source operating system
> and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the
> heart of the CHERI design process. For more details, see some of our
> previous papers:
> POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (
> http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (
> http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (
> http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf),
> CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html),
> CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (
> http://rems.io).
>
> We have a position available to work on:
>
> - the development of our Sail metalanguage for ISA description: a language
> with a lightweight dependent type system, designed to capture ARM, IBM
> POWER, and CHERI instruction semantics in an engineer-friendly way;
> - translation from Sail to generate efficient emulators and usable
> theorem-prover definitions;
> - mechanised proof about the architecture definitions, e.g. of security
> properties, relationships between concurrency models, and correctness
> results for high-level language concurrency compilation; and/or
> - development of reasoning, symbolic execution, debugging, and/or
> model-checking tools above the architecture definitions - the initial work
> should generate many opportunities along these lines.
>
> The successful candidate must have a PhD (or equivalent experience), a
> track-record of publication in relevant areas of Computer Science, good
> knowledge of English and communication skills, and the expertise and
> commitment to apply rigorous semantics to real systems. We're looking for
> people with the skills to make solid models and tools, well-engineered and
> widely usable. You should have expertise in one or more of:
>
> - functional programming (e.g. OCaml)
> - programming language semantics and type systems
> - theorem provers, especially Isabelle and/or Coq
> - symbolic execution
> - model-checking
>
> For senior applicants, e.g. who will be able to contribute substantially
> to future grant applications, it may be possible to appoint at the Senior
> Research Associate level.
>
> This is part of the broader REMS (Rigorous Engineering for Mainstream
> Systems) programme grant: a lively collaboration between systems and
> semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and
> apply mathematically rigorous semantics to mainstream systems.
>
> Informal enquiries should be directed to Peter Sewell (
> peter.sew...@cl.cam.ac.uk).
>
> To apply online for this vacancy, please click on the 'Apply' button
> below. This will route you to the University's Web Recruitment System,
> where you will need to register an account (if you have not already) and
> log in before completing the online application form.
>
> Please ensure you upload your Curriculum Vitae (CV) and a cover letter
> explaining your potential contribution to the project, as pdf documents.
> Include the names of 2 or 3 referees at the appropriate point in the online
> application. Your referees should be prepared to send references within a
> week of the closing date, if asked by the University. If you upload any
> additional 

[TYPES/announce] postdoc position (5 years) in Innsbruck

2017-01-12 Thread Aart Middeldorp

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

  5 year postdoc position in computational logic
  ==

The University of Innsbruck invites applications for a 5 year postdoctoral
position in the Computational Logic research group. Candidates must hold a
PhD degree in computer science. A strong background in computational logic
(in particular automated and interactive theorem proving, SMT solving, term
rewriting, type theory) is desired. The ideal candidate enjoys working with
students at all levels. Candidates are expected to conduct research leading
to a habilitation and contribute to teaching and administration. Knowledge
of German is not essential.

The position is a full-time "B1/3 position" with teaching obligations of
4 hours per semester. The annual gross salary is approximately EUR 50,000.
The official job advert (reference MIP-9118) appeared at

http://orawww.uibk.ac.at/public/karriereportal.details?asg_id_in=9118

Applications (including CV, publication list, and two letters of
recommendation) must be submitted electronically at

https://orawww.uibk.ac.at/public/karriereportal.bewerben?page=w_id=9118

no later than 2 February 2017. The starting date for the position is
1 March 2017. Informal inquiries may be addressed to

aart.middeldorp at uibk.ac.at

The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and
1976, is superbly located in the beautiful surroundings of the Tyrolean
Alps. The combination of the Alpine environment and urban life in this
historic town provides a high quality of living.

Further information is available from the following links:

Computational Logic:
http://cl-informatik.uibk.ac.at/

Department of Computer Science:
http://informatik.uibk.ac.at/

University of Innsbruck:
http://www.uibk.ac.at/

City of Innsbruck:
http://www.innsbruck.at/


[TYPES/announce] Postdoc position in provably secure systems

2016-12-20 Thread Roberto Guanciale
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We are seeking candidates for a Postdoc position in the department of computer
science at KTH Royal Institute of Technology. The candidate will join the 
PROSPER team,
led by Prof. Mads Dam and assistant professor Roberto Guanciale.
Our research vision is to produce  novel software and platforms that have
mathematically guaranteed security properties through the use of formal 
modelling and verification.

We are looking for highly-qualified candidates that can contribute to the work 
on 
designing and modelling of various low-level system software components,
on verification on low-level code, and on the modelling and analysis of the 
underlying hardware platforms.

KTH Royal Institute of Technology in Stockholm is the largest and oldest 
technical university in Sweden.
No less than one-third of Sweden’s technical research and engineering education 
capacity at university level is provided by KTH. 

The application deadline is 08 Jan 2017. The starting date is open for 
discussion.
Ideally we would like the successful candidate to start in spring 2017.

The full advertisement can be found at

https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:126536/

Roberto Guanciale


[TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

2016-12-16 Thread Peter Sewell
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[please circulate this to any likely candidates - thanks, Peter]

Research Associate/Senior Research Associate in Applied Semantics for
Production Architectures

University of Cambridge Computer Laboratory
Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 -
49,772
Fixed-term: until February 28, 2019, when the grant funding the post
currently ends.
Details: http://www.jobs.cam.ac.uk/job/12397/


Do you want to help build mathematically rigorous foundations for
real-world computing, to make it more robust and secure?

We have an ongoing project to establish rigorous semantic models for
production multiprocessors, to provide a clear basis for programming,
software verification, and hardware verification. This involves long-term
close collaborations with ARM and IBM, and we have an agreement with ARM to
take their internal ISA description, build a mathematical model based on
it, integrate it with the concurrency semantics we are developing, and
release the whole in a form usable for verification. This will provide the
first strongly validated public model for a production multiprocessor
architecture. We also have a close collaboration with the CHERI research
project, developing processors with hardware-accelerated in-process memory
protection and sandboxing, together with an open-source operating system
and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the
heart of the CHERI design process. For more details, see some of our
previous papers:
POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (
http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (
http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (
http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI
ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI (
https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (
http://rems.io).

We have a position available to work on:

- the development of our Sail metalanguage for ISA description: a language
with a lightweight dependent type system, designed to capture ARM, IBM
POWER, and CHERI instruction semantics in an engineer-friendly way;
- translation from Sail to generate efficient emulators and usable
theorem-prover definitions;
- mechanised proof about the architecture definitions, e.g. of security
properties, relationships between concurrency models, and correctness
results for high-level language concurrency compilation; and/or
- development of reasoning, symbolic execution, debugging, and/or
model-checking tools above the architecture definitions - the initial work
should generate many opportunities along these lines.

The successful candidate must have a PhD (or equivalent experience), a
track-record of publication in relevant areas of Computer Science, good
knowledge of English and communication skills, and the expertise and
commitment to apply rigorous semantics to real systems. We're looking for
people with the skills to make solid models and tools, well-engineered and
widely usable. You should have expertise in one or more of:

- functional programming (e.g. OCaml)
- programming language semantics and type systems
- theorem provers, especially Isabelle and/or Coq
- symbolic execution
- model-checking

For senior applicants, e.g. who will be able to contribute substantially to
future grant applications, it may be possible to appoint at the Senior
Research Associate level.

This is part of the broader REMS (Rigorous Engineering for Mainstream
Systems) programme grant: a lively collaboration between systems and
semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and
apply mathematically rigorous semantics to mainstream systems.

Informal enquiries should be directed to Peter Sewell (
peter.sew...@cl.cam.ac.uk).

To apply online for this vacancy, please click on the 'Apply' button below.
This will route you to the University's Web Recruitment System, where you
will need to register an account (if you have not already) and log in
before completing the online application form.

Please ensure you upload your Curriculum Vitae (CV) and a cover letter
explaining your potential contribution to the project, as pdf documents.
Include the names of 2 or 3 referees at the appropriate point in the online
application. Your referees should be prepared to send references within a
week of the closing date, if asked by the University. If you upload any
additional documents which have not been requested, we will not be able to
consider these as part of your application.

Please quote reference NR10978 on your application and in any
correspondence about this vacancy.

The University values diversity and is committed to equality of opportunity.

The University has a responsibility to ensure that all employees are
eligible to live and work in the UK.


[TYPES/announce] Postdoc position in the area of formal verification

2016-12-09 Thread Taolue Chen
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

[Apology for cross-posting.]

Applications are invited for a Postdoctoral Research Fellow position
working on formal verification. The work is being funded by EPSRC.

The aim of the project is to carry out perturbation analysis for
quantitative verification, i.e.,

(1) to analyse how the verification result is affected by the perturbation
of parameters and to provide a quantitative measure thereof; and
(2) to develop software tools to facilitate the perturbation analysis. The
toolkit will be employed to conduct case studies on real-world problems.

For some background on the kind of work, see the following papers

http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/fase16.pdf
http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/TSE16.pdf
http://www.eis.mdx.ac.uk/staffpages/taoluechen/pub-papers/concur14.pdf


The postdoc will be supervised by Dr Taolue Chen and be based in the
Department of Computer Science at Middlesex University London, UK. We offer
a competitive salary (in the range of £36,179 to £41,560 per annum). The
post is available for one year.

To apply, you must hold (or be close to achieving) a PhD in Computer
Science or a closely related discipline. You should have demonstrated your
research competence through high-quality and high-impact publications in
formal verification.

Informal enquiries are strongly encouraged and should be made to:

* Dr Taolue Chen (t.c...@mdx.ac.uk, taolue.c...@gmail.com)
 http://www.eis.mdx.ac.uk/staffpages/taoluechen/


[TYPES/announce] Postdoc Position in Distributed Systems/Verification/Coq

2016-11-17 Thread Ilya Sergey
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The PPLV group at University College London (UCL) has an opening for a
one-year postdoctoral position.

The successful candidate will work on the topic of implementing and
verifying distributed protocols and systems in the Coq proof assistant,
taking part in the research project "Program Logics for Compositional
Specification and Verification of Distributed Systems", funded by Ilya
Sergey's recently-awarded EPSRC First Grant. The project also involves
collaborators from University of Washington, US.

The ideal candidate will have a Ph.D. in Computer Science, general
knowledge of formal methods, and expertise in interactive theorem proving,
with substantial experience in using Coq, Agda, or similar tools.
Candidates should demonstrate strong programming and formal modeling
skills. Previous experience with concurrent or distributed programming is a
considerable plus.

The application deadline is December 8. 2016. The start date is negotiable,
but ideally it should be early in 2017. Here is the official advert with
more details, and the application link:

http://bit.ly/2f56sS1

Please, pass this on to anyone you think might be interested, and get in
touch with me if you have more questions about the position or UCL.

Kind regards.
Ilya


[TYPES/announce] Postdoc position in Verification of Infinite-state Systems

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


Postdoc position in Verification of Infinite-state Systems
(Updated Nov 2, 2016)
http://www.cs.uiowa.edu/~tinelli/html/positions.html


Project Supervisor

Professor Cesare Tinelli, Computational Logic Center
Department of Computer Science, The University of Iowa
http://www.cs.uiowa.edu/~tinelli


Project Description

The project's overall objective is to develop and implement improved 
SMT-based
verification/model checking techniques to verify safety properties of 
synchronous
data-flow models of infinite-state embedded reactive software. The 
project will
focus on contract-based compositional reasoning, automatic invariant 
discovery,
static analysis of contracts, and interactive contract generation. The 
new

techniques will be implemented in the Kind 2 model checker.


Position

The ideal candidate would be one with:
- A PhD in Computer Science or a closely related field
- A strong background in logic and/or automated reasoning
- Knowledge of and experience with SAT/SMT and model checking
- Experience designing, building, and maintaining large software systems
- Excellent programming skills
- Solid programming experience in OCaml or similar languages
- Good English writing and speaking skills
- The ability to work in a collaborative environment
- A strong commitment to research excellence

The position is a full time appointment in the Computational Logic 
Center at the
University of Iowa, with a starting salary of $58,000/year plus benefits 
which
include health insurance, paid leave, and access to university 
facilities and

activities.
It will start on **January 1, 2017** and is expected to have a duration 
of up to

two years, based on performance and continued availability of funds.
The position will remain open until filled.

Depending on the candidate's interests, there might be an opportunity to 
teach one
course per year in the Computer Science department as a visiting 
assistant professor.
This is, however, a separate position that would entail a corresponding 
reduction of
effort in the postdoc appointment. It should be understood as an 
opportunity, not as

a requirement for the postdoc contract.

Inquiries and applications should be sent via e-mail to to Prof. Tinelli 
with
"Model Checking postdoc" in the subject. When sending an application 
please include
your CV together with a brief description of your research 
accomplishments and

interests, and the names of three references.

-
Computational Logic Center

The Computational Logic Center at the University of Iowa is jointly 
headed by
Professors Omar Chowdhury, Aaron Stump, and Cesare Tinelli. In recent 
years, it has
included on average 3-5 postdocs, 6-8 PhD students and a number of 
master's and
undergraduate students. Its work has been funded by AFRL, AFOSR, DARPA, 
DOD, NASA,
NSF, General Electric, Intel, Rockwell Collins, and United Technologies. 
Its main
areas of research are automated deduction, satisfiability modulo 
theories, model
checking, verified-programming languages, foundations of programming 
languages, and
formal methods for security and privacy. The center has a strong 
emphasis on
theoretical foundations but is also known for a number of languages and 
tools co-
developed with external partners and used in academia and industry. 
These include
the SMT-LIB standard and benchmark library, the CVC3 and CVC4 SMT 
solvers, the Kind
and Kind 2 model checkers, the LFSC proof framework and checker, and the 
StarExec

solver execution service.


[TYPES/announce] PostDoc position at ITU

2016-10-14 Thread Carsten Schuermann
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

The IT University of Copenhagen seeks to hire outstanding researchers
at its Interdisciplinary Centre for Democracy and Technology
(DemTech).

The research will be conducted under the supervision of Carsten
Schuermann.  DemTech specializes on mathematical foundations of secure
multi-party computation, the design and analysis of cryptographic
primitives and protocols, formal languages for voting systems and
their properties, and automated tools to reason about them. DemTech
has expertise in both the symbolic and the computational styles of
protocol analysis. DemTech has established itself as a leading center
for research on trust and security in election technologies.

Your role is to work on the logical foundations of secure multi-party
distributed systems, the modelling of voting protocols, the automated
extraction of software from high-level description, and the automatic
verification of security properties, both in the symbolic and the
computational model.

A successful applicant will hold a PhD in Computer Science or Applied
Mathematics,a proven interest in reasoning systems, cryptography, or
security modelling.  Experience in cryptography will be considered an
advantage.

The appointment will will initially one year that can be extended.
You will work in an exciting international setting and participate in
a fast growing and dynamic research environment.

For inquiries please contact, Pia Kystol Sørensen (pksr@itudk) or
Carsten Schürmann (cars...@itu.dk)

The position is available now.



[TYPES/announce] Postdoc position at INRIA

2016-08-19 Thread Nataliia Bielova
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi everyone, 

we are looking for 2 postdocs at INRIA Sophia Antipolis, next to Nice, France. 
The successful candidate will join the project lead by Nataliia Bielova and 
Arnaud Legout 
to work on web tracking prevention through program analysis and measurement of 
user 
discrimination on the Web. 

Possible starting date is this fall/winter for the duration of 1 year. 
Applicants should have, 
or expect to obtain shortly, a PhD in Computer Science, preferably with a focus 
on the 
topics mentioned above.  Potential candidates are encouraged to contact 
Nataliia Bielova 
(nataliia dot bielova at inria dot fr).

Nataliia







[TYPES/announce] postdoc position at Wesleyan

2016-08-06 Thread Dan Licata
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi everyone,

I am looking for a postdoc with me here at Wesleyan.  Possible start dates 
range from this coming fall to the following one.  Please email me or submit an 
application if you're interested!  

-Dan

The Department of Mathematics and Computer Science at Wesleyan
University invites applications for a one-year postdoctoral position,
that is potentially renewable for a second year, subject to satisfactory
performance and available funds. The postdoc will work with Assistant
Professor Dan Licata on the topic of homotopy type theory, specifically
directed type theory.  The successful applicant will be able to pursue
his/her own research agenda as well.  Teaching is not required, but
there may be an opportunity for the postdoc to teach 1 or 2 courses in
their first year for additional compensation if they desire to develop
their teaching skills and portfolio. Candidates will be expected to have
a Ph.D. in hand by the time of appointment.

We will review applications until the position is filled; possible start
dates range from September 2016 through winter and fall 2017.
Applications must be submitted at https://academicjobsonline.org/ajo/jobs/7590.
Applications must include a cover letter, curriculum vitae, and brief
research statement.  At least one (up to three) letters of
recommendation should be submitted on academicjobsonline by the
recommender, or the applicant may provide the email addresses of
referees from whom we will obtain confidential letters of
recommendation.

Wesleyan University, located in Middletown, Connecticut, does not
discriminate on the basis of race, color, religious creed, age, gender,
gender identity or expression, national origin, marital status,
ancestry, present or past history of mental disorder, learning
disability or physical disability, political belief, veteran status,
sexual orientation, genetic information or non-position-related criminal
record. We welcome applications from women and historically
underrepresented minority groups. Inquiries regarding Title IX, Section
504, or any other non-discrimination policies should be directed to:
Antonio Farias, VP for Equity & Inclusion, Title IX and ADA/504 Officer,
860-685-4771, afar...@wesleyan.edu.


[TYPES/announce] Postdoc Position at IMDEA in Security/Privacy/Verification

2016-07-11 Thread Boris Köpf
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

We invite applications for a postdoctoral position at the IMDEA Software 
Institute in Madrid, Spain. The successful candidate will join the group of 
Boris Köpf to work on topics at the intersection of security, privacy, and 
formal verification.

The post is available from September 2016 for the duration of up to three 
years. Applicants should have, or expect to obtain shortly, a PhD in Computer 
Science, preferably with a focus on the topics mentioned above.

The IMDEA Software Institute is located in the vibrant area of Madrid, Spain. 
It offers an open and collaborative working environment, where researchers can 
focus on developing new ideas and projects. Salaries at the Institute are 
internationally competitive. Potential candidates are encouraged to contact 
Boris Köpf with inquiries (boris dot koepf at imdea dot org). 


[TYPES/announce] Postdoc position in verification at IMDEA, Madrid

2016-06-30 Thread Alexey Gotsman
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for a postdoctoral position at the IMDEA Software 
Institute in Madrid, Spain. The post is available from September 2016 for the 
duration of up to three years. The postdoc will work under supervision of 
Alexey Gotsman in the area of reasoning about distributed systems.

The candidate should have, or expect shortly to obtain, a PhD in Computer 
Science, preferably with expertise in verification, programming languages or 
distributed computing/systems. He or she would be expected to develop research 
questions within a specific context, to undertake original individual research, 
and to prepare research papers.

The IMDEA Software Institute is located in the vibrant area of Madrid, Spain. 
It offers an ideal working environment, where researchers can focus on 
developing new ideas and projects. Salaries at the Institute are 
internationally competitive.

Interested applicants are encouraged to contact Alexey Gotsman with inquires 
(alexey dot gotsman at imdea dot org). Formal applications should be submitted 
over the web. Please select the "Postdoc researcher" option at 

https://careers.imdea.org/software/

and mention this announcement in your research statement. Review of 
applications will begin immediately.



[TYPES/announce] postdoc position in type systems at NJIT (NYC area)

2016-06-07 Thread Iulian Neamtiu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

One postdoc position in type systems is available in Prof. Iulian Neamtiu's 
research group at the New Jersey Institute of Technology, in the New York City 
metropolitan area.

PROJECT SCOPE
Using type systems to reason about, and enforce program properties that involve 
different software versions or different executions, e.g., correctness of 
program changes or record-and-replay fidelity.

APPLICATION REQUIREMENTS
Required experience/qualifications: a strong publication record in type systems 
and/or static analysis, and experience with implementing program analyses for 
real-world programs. 

Optional experience/qualifications, that are helpful but insufficient by 
themselves:
• rigorous techniques for reasoning about and manipulating programs, e.g., 
dynamic analysis or binary/bytecode transformation
• research experience in the areas of systems, security, or smartphones
• empirical software engineering/mining software repositories

APPLICATION
Apply here: http://njit.jobs/applicants/Central?quickFind=55021 
Your application should contain the following two documents:
• A cover letter summarizing your background and justifying how it fits 
this position.
• Your CV, which should include the name and contact info of at least 3 
references.
To be considered, applications need to include both these documents.

AVAILABILITY and DURATION
The position is available immediately, and will remain open until filled. While 
the start date is flexible, please note that the anticipated end date is June 
30, 2017. Subsequent appointments might be possible, subject to funding 
availability and performance.

SALARY
Annual salaries range from $40,000 to $55,000, depending on qualification and 
experience. 
Salary and benefits details: 
http://www5.njit.edu/research/sites/research/files/lcms/pdf/FY15-Salary-Computation-Guidelines-8-5-14.xlsx

GEOGRAPHICAL AREA
NJIT is in the greater New York City area, a 20 minute train ride from 
Manhattan.

CONTACT
Please contact Iulian Neamtiu for any questions.
https://web.njit.edu/~ineamtiu/
ineam...@njit.edu

Re: [TYPES/announce] Postdoc position on security protocol verification at NTU Singapore

2016-01-19 Thread Alwen Tiu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Apology for multiple postings.
There was a typo in the previous posting regarding the application
deadlines. Below is the corrected version.

Regards,
-Alwen
--

One postdoc position is available at the School of Computer Engineering,
Nanyang Technological University (NTU)  Singapore, for a project on
verification of security protocols funded by the Ministry of Education of
Singapore.

A particular emphasis will be on designing and implementing decision
procedures for finding attacks on protocols or producing formal proofs of
their security. We will be using a mixture of process algebraic and logical
frameworks to express protocols and their properties, in particular,
equivalence properties of security protocols.

Candidates must possess a PhD degree in Computer Science or related areas.
Candidates with strong backgrounds in process calculus, such as the
pi-calculus and its variants, and/or formal logic and theorem proving are
preferred. The salary range is between SGD 4000 - 6000 per month.

The position will be initially offered for one year, but can be extended up
to three years, subject to satisfactory performance and availability of
funding.

To apply for the position, please send a cover letter and your latest CV
(please indicate names of three referees in your CV) by email to Alwen Tiu (
a...@ntu.edu.sg, alwen@gmail.com). Applications will be accepted until
the position is filled, but to ensure the full consideration of your
application, please send your application by 21 February 2016. Only
shortlisted candidates will be notified of the results of their
applications. The selected candidate is expected to commence in April 2016.

If you have any further questions regarding the position and/or the
project, please email a...@ntu.edu.sg.


Regards,
Alwen Tiu


[TYPES/announce] Postdoc position on security protocol verification at NTU Singapore

2016-01-19 Thread Alwen Tiu
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

One postdoc position is available at the School of Computer Engineering,
Nanyang Technological University (NTU)  Singapore, for a project on
verification of security protocols funded by the Ministry of Education of
Singapore.

A particular emphasis will be on designing and implementing decision
procedures for finding attacks on protocols or producing formal proofs of
their security. We will be using a mixture of process algebraic and logical
frameworks to express protocols and their properties, in particular,
equivalence properties of security protocols.

Candidates must possess a PhD degree in Computer Science or related areas.
Candidates with strong backgrounds in process calculus, such as the
pi-calculus and its variants, and/or formal logic and theorem proving are
preferred. The salary range is between SGD 4000 - 6000 per month.

The position will be initially offered for one year, but can be extended up
to three years, subject to satisfactory performance and availability of
funding.

To apply for the position, please send a cover letter and your latest CV
(please indicate names of three referees in your CV) by email to Alwen Tiu (
a...@ntu.edu.sg, alwen@gmail.com). Applications will be accepted until
the position is filled, but to ensure the full consideration of your
application, please send your application by 21 August 2015. Only
shortlisted candidates will be notified of the results of their
applications. The selected candidate is expected to commence in October
2015.

If you have any further questions regarding the position and/or the
project, please email a...@ntu.edu.sg.


Regards,
Alwen Tiu


[TYPES/announce] Postdoc position at Penn on the DeepSpec project

2016-01-11 Thread Benjamin C. Pierce
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Join Penn as a postdoc on the DeepSpec  project! 

Outstanding postdocs with interests in programming languages, formal 
verification, and systems software are invited to join the programming 
languages group at Penn!  We are currently seeking researchers as part of “The 
Science of Deep Specification,” an NSF-funded Expedition in Computing.  

The goal of DeepSpec is to catalyze the adoption of deep specification 
techniques, through a tightly integrated combination of focused research, 
course development, and community building.  At Penn, Steve Zdancewic leads the 
Vellvm  project, which provides a Coq 
specification of the LLVM intermediate representation. In this Expedition, 
Vellvm will serve as a testbed for experimenting with proof-engineering 
techniques and as a component of a larger system involving many deep 
specifications. Handling deep specifications at such a large scale (and that 
evolve over time, as LLVM’s must) will require significant technical advances. 
Stephanie Weirich leads the CoreSpec  
project, which seeks to develop a Coq specification of the core language of the 
Glasgow Haskell Compiler (GHC).  This part of the DeepSpec project will extend 
the breadth of the connected network of specifications to include a 
industrial-strength high-level programming language.  Benjamin Pierce leads the 
QuickChick  project, focused on 
property-based testing of deep specifications.  The goal of this part of the 
DeepSpec research is to accelerate the development of deeply specified software 
by supporting a smooth transition between automated random testing and full 
formal verification.  Another strong focus of work at Penn will be on the role 
of deep specifications in modernizing undergraduate curricula in traditional 
core subjects such as operating systems and compilers.

These threads are closely connected to the other components of the DeepSpec 
consortium. In particular, this work will be done in the context of 
interconnected systems, interacting with and building on verified operating 
systems (CertiKOS, Yale), verified C compilers (CompCert and Verifiable C, 
Princeton), and verified hardware programming (Kami, MIT).  

The ideal candidate will have a PhD in Computer Science or a related field and 
experience with the Coq proof assistant or a similar tool. To ensure full 
consideration, please send a CV and research statement to Benjamin Pierce 
(bcpie...@cis.upenn.edu ), and arrange for at 
least three letters of reference to be sent to the same address, by February 
15, 2016.  

The University of Pennsylvania  is an equal opportunity employer. All qualified 
applicants will receive consideration for employment without regard to race, 
color, religion, sex, national origin, disability status, protected veteran 
status, or any other characteristic protected by law. 

More information about the DeepSpec project is available at deepspec.org 
.

Looking forward to your application,

 Benjamin Pierce
 Stephanie Weirich
 Steve Zdancewic





[TYPES/announce] postdoc position in dependent types at Dalhousie

2015-10-01 Thread Peter Selinger
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear colleagues,

I invite applications for one postdoctoral position, starting between
now and January 1, at Dalhousie University under my supervision.

The successful applicant will work on a project entitled "Trusted
Quantum Software via a Formally Verified Functional Quantum
Programming Language". Specifically, the project will involve the
design of a type system for a type-safe functional programming
language for quantum computing, loosely modelled on the Quipper
language (http://www.mathstat.dal.ca/~selinger/quipper/). It will also
involve developing the meta-theory (including semantics) of the
language, and eventually the formalization of some of this meta-theory
in a proof assistant.

Familiarity with type theory (especially dependent type theory),
programming language design, and/or semantics will be a prerequisite
for this postdoc. Familiarity with quantum computing will be helpful,
but is neither necessary nor sufficient for this position - the main
emphasis is on programming languages and type systems.

Although the position will be held at Dalhousie University in Canada,
it will be an asset if the candidate is able to travel, because I will
be spending one semester in Germany and one semester in the U.S. next
year, and ideally I would like the postdoc to be able to accompany me.

Funding for the project comes from the U.S. Air Force Office of
Scientific Research, and the research project will be part of a team
effort also involving collaborators from Tulane, Stanford, Oxford, the
University of Iowa, and the University of Pennsylvania.

The nominal start date for the project is September 30, 2015 (yes,
this is today!), so the start date can be immediately, or some time in
the near future.

The position is initially for 1 year, and can be extended for an
additional year. The salary is CAD $60,000 per year.

Interested applicants should contact Peter Selinger at
selin...@mathstat.dal.ca as soon as possible, and in any case before
October 21. I can provide more details about the research project to
interested applicants on request.

Thanks, -- Peter


[TYPES/announce] POSTDOC position at NOVA LINCS Lisbon (background in Programming Languages and Tools)

2015-08-10 Thread Luis Caires
[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

We would like to announce a post doc / research associate position at
NOVA Laboratory for Computer Science and Informatics (Lisbon) for
candidates with a strong background in topics such as programming
languages, programming language design and implementation, software
verification, and program analysis. The successful candidate will join
a just launched project on new programming models, incremental
verification techniques, and programming environments for the
interactive / live construction of trustworthy web/cloud applications.

Please contact me (lcaires(at)fct.unl.pt) for additional information
about the position and project. More information at:

http://nova-lincs.di.fct.unl.pt/open-positions/position-4

Best regards,

Luis Caires


-- 
Best regards,

Luis Caires
Head of Department
Director of NOVA Laboratory for Computer Science and Informatics
Departamento de Informática
FCT Universidade Nova de Lisboa
http://ctp.di.fct.unl.pt/~lcaires


[TYPES/announce] Postdoc position in symbolic execution at Imperial College London

2015-07-31 Thread Cristian Cadar

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

Applications are invited for a postdoctoral position in the Software
Reliability Group (http://srg.doc.ic.ac.uk/) in the Department of
Computing at Imperial College London.

The goal of this project is to investigate and design program
transformations --- both semantics-preserving and semantics-altering
--- that increase the scalability of symbolic execution. The
techniques will primarily be implemented on top of the KLEE symbolic
execution engine.

To apply for this position, you will need to have a strong background
in compilers and program analysis, and a good understanding of
software engineering and operating systems. You will also need
experience in building and working with large software systems and
tools. Prior experience with LLVM and KLEE is desirable, but not
required.

Applicants will have (or shortly expect to receive) a PhD degree (or
equivalent) in Computer Science or a related field, and will be expected
to have a proven track record with strong publications in relevant areas.

This position will be based at the South Kensington campus in central
London.

The application deadline is 4 September 2015, with interviews expected
to take place on 18 September.

For further information about this position, please visit
http://srg.doc.ic.ac.uk/vacancies.


  1   2   >