Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Postdoctoral position on Program Semantics and...

Email Gateway (Jan 04 2023 at 12:47):

From: David Miguel Sanan Baena <cl-isabelle-users@lists.cam.ac.uk>
Apologies if you receive multiple copies of these open positions

A postdoctoral position in program semantics and verification is open at the Singapore Institute of Technology (SIT) under the supervision of Prof. David Sanan.

The project aims to minimize the gap between formal verification and efficient industrial applications. Specifically, we focus on constructing a verification framework for software using deductive reasoning, and on the formalization of smart contract semantics, with special attention to the Solidity language.

The candidate will work on formalizing programming language semantics, constructing a framework for scalable verification, and building mechanisms for automatic reasoning on Isabelle/HOL.

Qualifications:

• A Ph.D. in Computer Science, Mathematics, or a closely related discipline.
• Experience in formal methods and formal verification. Experience in Isabelle theorem prover is preferred.
• Familiar with program semantics and program logic, including Hoare Logic and Separation Logic.

SIT offers highly competitive salaries and is situated in Singapore, a multicultural English-speaking city. Singapore offers high-quality education and healthcare at all levels and very low tax rates.

The position is available full-time for one and a half years in the first instance, with the possibility of renewal(s).

Starting date: as soon as possible.

To apply, send an email with the CV to david.miguel@singaporetech.edu.sg

Notice: This e-mail may contain confidential and/or privileged information. If you are not the intended recipient or have received this e-mail in error, please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.
Singapore Institute of Technology, Co. Reg. No. 200917667D.

Email Gateway (Jan 22 2024 at 13:37):

From: David Miguel Sanan Baena <cl-isabelle-users@lists.cam.ac.uk>
Apologies if you receive multiple copies of these open positions

A postdoctoral position in program semantics and verification is open at the Singapore Institute of Technology (SIT) under the supervision of Prof. David Sanan.

The project aims to minimize the gap between formal verification and efficient industrial applications. Specifically, we are focusing on constructing a verification framework for software using deductive reasoning, and on formalizing the semantics of smart contracts, with special attention to the Solidity language.

The candidate will work on formalizing programming language semantics, constructing a framework for scalable verification, and developing mechanisms for automatic reasoning in Isabelle/HOL.

Qualifications:

• A Ph.D. in Computer Science, Mathematics, or a closely related discipline.
• Experience in formal methods and formal verification. Experience with the Isabelle theorem prover is preferred.
• Familiarity with program semantics and program logic, including Hoare Logic and Separation Logic.

The expected salary range is 75k~100k SGD + bonus. SIT is located in Singapore, a multicultural English-speaking city known for its high-quality education and healthcare systems, as well as very low tax rates.

This full-time position is available for one year initially, with the possibility of renewal(s).

Starting date: As soon as possible.

To apply, please send an email with your CV to david.miguel@singaporetech.edu.sg.

Last updated: Apr 20 2024 at 08:16 UTC