[pl-seminar] Fwd: Job Opportunity at Automated Reasoning Group (Amazon)

[Aws Albarghouthi <aws@xxxxxxxxxxx>]

---------- Forwarded message ---------
From: Desai, Ankush <ankushpd@xxxxxxxxxx>
Date: Tue, Mar 10, 2020 at 5:13 PM
Subject: Job Opportunity at Automated Reasoning Group (Amazon)
To: Aws Albarghouthi <aws@xxxxxxxxxxx>

Hi Aws,

 

Hope you are doing well.

 

We are looking for a masters or undergrad student to join our team to work on application of formal methods to distributed systems in AWS.

 

Please let us know if you have anyone in mind. Please also feel free to forward this to others.

 

I have attached a draft job description below.

 

Thanks,

Ankush

 

------

We are looking for a great team member to work with us on the very important "code conformance to algorithm design" problem. Often, a service team reasons about correctness at the algorithm level, sometimes using tools. However, these algorithm designs are typically not connected to the implementations in code. As a result, the desirable properties of designs do not carry over to the code and code may violate the design. As code evolves, the design may no longer be an accurate representation of the implementation. To remedy this state of affairs, we want to develop and roll out to various services a framework for tying Java implementation code to design-level models. We want to automatically instrument Java code so that it generates events to drive a "monitor" that checks if executions are consistent with the algorithm design. Monitors may connect implementation state to algorithm state. We are initially going to work with the Amazon S3 team on this project but plan to roll out this capability more widely into the teams' CI flows and maybe even in prod in one-box deployments.

        

We are looking for someone who has good analytical and Java development skills, and enjoys working on and thinking about systems (as opposed to applications) code. At least two years of development experience is desired. An MS degree is preferred. We will train the new team member in runtime verification technology such as the JavaMOP tool (http://fsl.cs.illinois.edu/index.php/JavaMOP) and the P model checker (https://github.com/p-org/P).

 

 

--

Aws