[TYPES/announce] Recruitment of a research engineer in automated proof at LIRMM in Montpellier (France)

[David Delahaye]

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


*** Please feel free to circulate this message ***
*** Sorry for the multiple receptions ***

The LIRMM (UMR 5506, University of Montpellier, CNRS) is recruiting a 
full-time research engineer for a period of 12 months in the field of 
automated proof. The desired start date is January 1, 2023, and the 
position will be located in Montpellier (France).


*Assignments:*

The purpose of this position is to strengthen the software development 
capabilities of the MaREL team (specialized in the field of software 
engineering) of the Computer Science department of LIRMM.The person 
hired will be involved in the development of Goéland, an automated 
reasoning tool developed in the team by Julie Cailler (PhD student) for 
over a year. This tool is based upon a new proof search procedure for 
first-order logic, which leverages concurrency to produce proofs in the 
context of the tableaux method. This tool currently gives excellent 
results (as measured by the number of solved problems) in comparison 
with similar tools. Notably, it achieves better results in some problem 
categories than similar (tableaux-based) tools, some of which have been 
established for years. A conference article on Goéland has been accepted 
for publication at IJCAR 2022, a rank A conference, demonstrating the 
interest of the community for the approach used by that tool. 
Furthermore, Goéland has taken part in the CASC-J11 competition, 
organized in parallel with IJCAR 2022, and in which the current best 
automated deduction tools compete on different sets of problems. The 
tool has been awarded the “best newcomer” distinction during this 
competition.


The hired person will participate in the development and maintenance of 
the Goéland software, which is developed using Go, a language suited to 
concurrent programming. The aim of this position is twofold. The first 
mission is to get the tool in working for competitions, particularly 
CASC, a yearly occurrence that serves as a display of our work. The 
second is to apply the tool in a more industrial setting. A benchmark of 
problems originating from the modeling of industrial applications with 
the B method is already available (as a result of the ANR project Bware) 
but a number of extensions to Goéland are needed before it can be used 
on this benchmark.


In more detail, the assignments of the hired person will include:

 *

   Improving tests for proof search with equality. Equality reasoning
   is implemented but further testing is required for validation.

 *

   Integrating polymorphism in the proof search. Proof search with
   polymorphic types has been developed recently, but this feature has
   yet to be integrated and also requires tests for validation.

 *

   Integrating linear arithmetic reasoning in the proof search.
   Currently, the simplex method (for problems involving rational
   numbers) and the branch and cut algorithm (for problems involving
   integers) have been developed but their integration and testing
   remain to be done.

 *

   Testing the tool on the whole TPTP problems collection. This library
   of problems is used in particular for the CASC competition.

 *

   Testing the tool on the benchmark of industrial problems taken from
   the ANR project BWare . This test can only be carried out after the
   integration of polymorphism and linear reasoning in the tool.

*Activities:*

The hired person will work under the direction of David Delahaye 
(PR/full professor in the team MaREL), Simon Robillard (MCF/associate 
professor in the team MaREL), and Julie Cailler (PhD student in the team 
MaREL, with a thesis on the topic, and the main developer of Goéland).


The technical program follows the assignments described in the previous 
section. The order of assignments is not critical, with the exception of 
tests on the BWare benchmarks, for which the integration of polymorphism 
and linear arithmetic reasoning are prerequisites.


*Skills:*

The candidate must demonstrate the following:

 *

   High motivation for exploratory work in coordination with researchers

 *

   Familiarity with the notions of proof and proof search

 *

   Familiarity with concurrent programming (regardless of the
   programming language)

 *

   Aptitude for collaborative development and version management using Git

 *

   Experience with Agile project management

 *

   Excellent aptitude to work in collaboration and to engage external users

 *

   Fluency in English, both written and oral, for the purpose of
   scientific communication

 *

   Basic knowledge of French, with the intent to learn the language

 *

   Autonomy and initiative, aptitude to make technical decisions and
   justify them in the context of the project

 *

   Affinity for open-source software development

*Context:*

LIRMM (Laboratoire d'Informatique, de Robotique et de Microélectronique 
de 

[TYPES/announce] Faculty positions at Oxford

[Jeremy Gibbons]

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

Oxford University’s Computer Science Department is hiring four new faculty. The 
positions are open to all areas of computer science and the closing date is 12 
noon on 14 December 2022. For more information, see 
https://urldefense.com/v3/__https://www.cs.ox.ac.uk/aboutus/vacancies/vacancy-faculty-hiring.html__;!!IBzWLUs!V57LUu-qnhr5lyXYJTYlgr4x2YxBREjB5cPifFV41hysW9WqOhs5P5NRUhSKKDSrnlbrn3EXWbPdHsh4M-epV2UPsaEAS8AfhuWY1pDvqYA$
   


Jeremy

jeremy.gibb...@cs.ox.ac.uk
Oxford University Department of Computer Science,
Wolfson Building, Parks Road, Oxford OX1 3QD, UK.
+44 1865 283521
https://urldefense.com/v3/__http://www.cs.ox.ac.uk/people/jeremy.gibbons/__;!!IBzWLUs!V57LUu-qnhr5lyXYJTYlgr4x2YxBREjB5cPifFV41hysW9WqOhs5P5NRUhSKKDSrnlbrn3EXWbPdHsh4M-epV2UPsaEAS8AfhuWYO_e9VHI$
  

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

[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.