[TYPES/announce] PhD Position in Formal Verification of Autonomous Systems

[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 PhD candidates interested in conduction research in Formal 
Verification of Autonomous Cyber-Physical Systems (ACPS). The goal of the PhD 
project is to develop techniques for the design and verification of assured 
ACPS with a focus on runtime assurance. You will develop theory and tools for 
the construction of runtime monitors that capture under what conditions an ACPS 
is guaranteed to maintain safety. A key challenge in developing such monitors 
is to handle noisy, missing, or delayed data. Of particular interest is the 
investigation of compositional methods for constructing runtime monitors. The 
candidate will build on the latest advances in formal methods and learning 
theory, to develop methods that allow for building monitors with formal 
guarantees on their correctness and reliability.


This position is funded by the Wallenberg AI, Autonomous Systems, and Software 
Program (WASP 
https://urldefense.com/v3/__https://wasp-sweden.org/__;!!IBzWLUs!T4cTHrCyRiagt1iMJnBw-723XM7bjauK5mbWeKkhX-WmUVkbr2nqrRJ8F_4TQqTj9psK-i26lebz2--r4d7oib5XKsFR2UFqfw$
 ). 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=12785=UK__;!!IBzWLUs!T4cTHrCyRiagt1iMJnBw-723XM7bjauK5mbWeKkhX-WmUVkbr2nqrRJ8F_4TQqTj9psK-i26lebz2--r4d7oib5XKsGAJE3-mg$
 

For questions please reach out Hazem Torfah at 
haze...@chalmers.se

Deadline April 30, 2024.


--
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] SMT 2024 Third Call For Papers

[Yoni]

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



SMT 2024: 22nd International Workshop on Satisfiability Modulo Theories

Montreal, Canada, July 22-23, 2024



Paper Submission: April 28, 2024 11.59 pm AoE (Anywhere on Earth)

Notification: June 1, 2024

Conference website   
https://urldefense.com/v3/__http://smt-workshop.cs.uiowa.edu/2024/__;!!IBzWLUs!RpPA3z8hcctXB8bqRNpfpykmZB1jzxeH8nHOAa572ePHeBs4an791RnNij7N8uYLvRNMq9az3sHBdvhbPqPWs75wu5N7vA$
 

Submission link  
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=smt2024__;!!IBzWLUs!RpPA3z8hcctXB8bqRNpfpykmZB1jzxeH8nHOAa572ePHeBs4an791RnNij7N8uYLvRNMq9az3sHBdvhbPqPWs76m79FGQw$
 

== Overview

The aim of the workshop is to bring together researchers and users of SMT
tools and techniques. Relevant topics include but are not limited to:

- Decision procedures and theories of interest

- Combinations of decision procedures

- Novel implementation techniques

- Applications and case studies

- Benchmarks and evaluation methodologies

- Theoretical results

== Paper submission and Proceedings

Three categories of submissions are invited:

1. Extended abstracts : given the informal style of the workshop, we
strongly encourage the submission of preliminary reports of work in
progress. They may range in length from very short (a couple of pages) to
the full 10 pages and they will be judged based on the expected level of
interest for the SMT community. They will be included in the informal
proceedings.

2. Original papers: contain original research (simultaneous submissions are
not allowed) and sufficient detail to assess the merits and relevance of
the submission. For papers reporting experimental results, authors are
strongly encouraged to make their data available.

3. Presentation-only papers: describe work recently published or submitted
and will not be included in the proceedings. We see this as a way to
provide additional access to important developments that SMT Workshop
attendees may be unaware of.

Papers in all three categories will be peer-reviewed. Extended abstracts
and original papers should not exceed 10 pages. All papers should be in
standard-conforming PDF. Technical details may be included in an appendix
to be read at the reviewers' discretion. Final versions should be prepared
in LaTeX using the easychair.cls class file. (The 10 page limit does not
include references.). Presentation-only papers may be submitted as
originally published, if published elsewhere, and should not exceed 10
pages otherwise.

== Special Issue

Selected submissions may be invited to be included in a planned special
issue of “acta informatica” (to be confirmed).

== Invited Speakers

Sophie Tourret (INRIA)

Mathias Preiner (Stanford University)

== Program Chairs

Giles Reger - Amazon Web Services

Yoni Zohar - Bar-Ilan University

== Program Committee

Katalin Fazekas (TU Wien)

Viktor Kuncak (Ecole Polytechnique Fédérale de Lausanne)

Ahmed Irfan (SRI International)

Aina Niemetz (Stanford University)

Andrew Reynolds (University of Iowa)

Daniela Kaufmann (TU Wien)

Haniel Barbosa (Universidade Federal de Minas Gerais)

Nadia Labai (Amazon)

Clark Barrett (Stanford University)

Alexander Nadel (Technion & Intel)

Philipp Rümmer (University of Regensburg)

Nestan Tsiskaridze (Stanford University)

Guilherme Toledo (State University of Campinas)

Yannick Moy (AdaCore)

Martin Suda (Czech Technical University in Prague)

Stéphane Graham-Lengrand (SRI International)

François Bobot (CEA)

Mate Soos (Ethereum Foundation)

Nikolaj Bjørner (Microsoft)

[TYPES/announce] CfP - ICTCS24

[Riccardo Treglia]

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

*Call for Papers *ICTCS 2024 – 25th Italian Conference on Theoretical
Computer Science September 11-13, 2024, Turin, Italy
website: 
https://urldefense.com/v3/__https://ictcs2024.di.unito.it/__;!!IBzWLUs!Se5c4DXlCKj_aFoB3eFNs-LGOsxC0YiEef4iBsHjgsdBcGC5bUE1tIk3hkpGjGcSqs3F3CTnZ81uMFDSgzdHZGyyBH9MLcQKiaUTqYlUEEU$
 

Scope and Topics

The Italian Conference on Theoretical Computer Science (ICTCS) is the
conference of the Italian Chapter of the European Association for
Theoretical Computer Science.

The purpose of ICTCS is to foster the cross-fertilization of ideas stemming
from different areas of theoretical computer science. In particular, ICTCS
provides an ideal environment where junior researchers and PhD students can
meet senior researchers.

Contributions in any area of theoretical computer science are warmly
invited from researchers of all nationalities.

The topics of interest include, but are not limited to, the following: agents,
algorithms, argumentation, automata theory, complexity theory,
computational logic, computational social choice, concurrency theory,
cryptography, discrete mathematics, distributed computing, dynamical
systems, formal methods, game theory, graph theory, knowledge
representation, languages, model checking, process algebras, quantum
computing, rewriting systems, security and trust, semantics, specification
and verification, systems biology, theorem proving, type theory.

Paper Submission

Two types of contributions, written in English and formatted according to
Springer LNCS style, are solicited.

Regular papers: up to 12 pages PLUS bibliography, presenting original
results not appeared or submitted elsewhere. To ease the reviewing process,
the authors of regular papers may add an appendix, although reviewers are
not required to consider it in their evaluation.

Communications: up to 5 pages PLUS bibliography, suitable for extended
abstracts of papers already appeared/submitted or to be submitted
elsewhere, as well as papers reporting ongoing research on which the
authors wish to get feedback and overviews of PhD theses or research
projects.

Authors are invited to submit their manuscripts in PDF format by accessing:

Submission Page:  
https://urldefense.com/v3/__https://easychair.org/conferences/?conf=ictcs2024__;!!IBzWLUs!Se5c4DXlCKj_aFoB3eFNs-LGOsxC0YiEef4iBsHjgsdBcGC5bUE1tIk3hkpGjGcSqs3F3CTnZ81uMFDSgzdHZGyyBH9MLcQKiaUTZa0X5SA$
 

All accepted original contributions (regular papers and communications)
will be published on CEUR-WS.org.

For each accepted contribution, at least one of the authors is required to
attend the conference and present the paper.

TCS Special Issue

Following the tradition, the authors of the very best papers presented at
the conference will be invited to submit an extended version of their work
in a special issue of Theoretical Computer Science journal.
Invitations will be sent out after the workshop. The target is to publish
the special issue by the end of the year 2025.

Important Dates

Paper submission: 9 June, 2024
Notification: 14 July, 2024
Revised version for pre-proceedings: 30 August, 2024
Conference: 11 -13 September, 2024
Final version for proceedings: TBA

Organising Committee
Ugo de’Liguoro (Università di Torino)
Matteo Palazzo (Università di Torino)
Daniele Pautasso (Università di Torino)
Luca Roversi (Università di Torino)
Riccardo Treglia (King’s College London)

[TYPES/announce] Three Post-doc positions in RECIPROG project (located in France -- Lyon, Nantes and Paris)

[Alexis Saurin]

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

This is an announcement for three one-year postdoctoral positions funded 
by the ANR ReCiProg - Reasoning on Circular proofs for Programming, to 
be hosted in Lyon (LIP), Nantes (LS2N, Gallinette) and Paris (IRIF, 
PPS).


We seek strong candidates holding a PhD in Computer Science or 
Mathematics, and with expertise in one or several of the following 
areas:


*
Proof theory
*
Curry-Howard correspondence
*
Logics with fixed points
*
Coinductive reasoning
*
Proof assistants (formalization skills or development experience)
*
Type theory
*
Category theory
*
Automated deduction
*
Automata theory

In relation with the above topics, an experience in one or several of 
the following topics will be particularly appreciated: fixed-points and 
circular proofs, the Coq proof assistant, inductive and coinductive 
types, guarded recursion, coalgebras, inductive and coinductive theorem 
proving, categorical logic, infinitary term rewriting and infinitary 
lambda-calculi.


The successful candidate will be employed in one of the following French 
research lab, depending on her/his specific profile and scientific 
project:


- LIP (Plume Team), Lyon (local coordinator: Denis Kuperberg)
- LS2N (Gallinette Team), Nantes (local coordinator: Guilhem Jaber)
- IRIF (PPS & Picube Team), Paris (local coordinator: Alexis Saurin)

Application process:

*
Each potential candidate is advised to contact the project coordinator 
and the local coordinators of interest as soon as possible to express 
her/his intent to submit an application.

*
Deadline for applications is on May 15th, for a starting date between 
September 1st 2024 and December 31st 2024, to be negotiated.

*
Candidates should send their application to Alexis Saurin (alexis dot 
saurin at irif dot fr) with a subject containing "[RECIPROG post-doc 
application]".

*
The application should contain (i) a CV, (ii) a brief research statement 
(1-2 pages) & (iii) at least two contacts of reference persons (or 
reference letters if available) and it should indicate the site(s) of 
interest for the application.

*
The salary will depend on the successful candidate's prior research 
experience and of hiring site, with a guaranteed minimum of 2300 
EUR/month before taxes.

*
Each position is for a one-year post-doc.

Project summary:

RECIPROG is an ANR collaborative project (aka. PRC) running till the end 
of 2025 involving french teams in Lyon, Marseille, Nantes and Marseille, 
which aims at extending the proofs-as-programs correspondence (aka 
Curry-Howard correspondence) to recursive programs and circular proofs 
for logics and type systems using induction and coinduction. The project 
will contribute both to the necessary theoretical foundations of 
circular proofs and to the software development allowing to enhance the 
use of coinductive types and coinductive reasoning in the Coq proof 
assistant, as well as software verification techniques using circular 
tools.


More informations:

*
More informations can be found on the project webpage: 
https://urldefense.com/v3/__https://www.irif.fr/reciprog/index__;!!IBzWLUs!VzhX9zyYRdDzMxzHaVBBvvuNMTKT_a7EkUWpFgJeHxK_X3-Bd58e4Ir0kp5xAd5rs6FVgPDcEBXFiS1FWJIW91OQJOV8TmVq_KUJWVc$  and 
https://urldefense.com/v3/__https://www.irif.fr/reciprog/post-doc-offer-paril-2024__;!!IBzWLUs!VzhX9zyYRdDzMxzHaVBBvvuNMTKT_a7EkUWpFgJeHxK_X3-Bd58e4Ir0kp5xAd5rs6FVgPDcEBXFiS1FWJIW91OQJOV8TmVqq-4rZ0M$ 
 	*
Interested candidates may contact the project coordinator (Alexis 
Saurin) as well as the local coordinators (Guilhem Jaber, Denis 
Kuperberg, Luigi Santocanale & Alexis Saurin) to enquire about more 
specific research directions and the adequacy of their research profile.
 	* Cross-site projects involving members of the project from different 
labs are welcome.
 	* There is a one-year funding for each of the three sites of Lyon, 
Nantes and Paris.


--
Alexis Saurin
IRIF - CNRS, Université Paris-Cité & INRIA