[TYPES/announce] Research Fellow at UCL - Programming Principles, Logic, and Verification
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Research Fellow - Programming Principles, Logic and Verification University College London The Interface Reasoning for Interacting Systems (IRIS) project, led by Prof. David Pym (UCL), seeks to understand the compositional structure of systems and their communications, at all scales from computer code through distributed systems to organizational structure. We are seeking a Research Fellow to join our team and conduct theoretical and/or applicable research in this area. The research programme will be in the broad area of *verification* from the perspective of the IRIS project. We seek candidates with a PhD in computer science or a closely related area and an interest in any or all of the following: * program analysis and verification; * concurrency theory; * probability theory; * automated reasoning; * logic and formal methods. Previous experience in developing automated software tools is desirable, but not essential. The role will be jointly managed by James Brotherston (and David Pym) at UCL and John Wickerson at Imperial College. While based primarily at UCL, the role will involve frequent contact with Imperial College and the other project partners. The post is offered for 12 months initially, but is extensible up to 36 months. Informal enquiries prior to application are welcome and should be directed initially to James Brotherston at j.brothers...@ucl.ac.uk. Apply at: https://tinyurl.com/yctdne4y More info on IRIS at: https://interfacereasoning.com/
[TYPES/announce] Postdoc position at UCL in verification / logic / automated reasoning
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Research Associate position in Automated Verification, Logic and Theorem Proving (ref:1439542) Dept. of Computer Science, University College London, UK The UCL Dept. of Computer Science invites applications for a postdoctoral Research Associate to work on the EPSRC-funded project Boosting Automated Verification using Cyclic Proof. The core of the project is the use of *cyclic proof*, a relatively new technique in inductive theorem proving, to add general inductive reasoning capability to the various components of interprocedural program analysis and thereby, hopefully, to extend the reach of current verification methods. The main experimental tool is the cyclic theorem prover Cyclist (see https://github.com/ngorogiannis/cyclist ). The project is under the supervision of Dr. James Brotherston in the Programming Principles, Logic and Verification (PPLV) group at UCL; others involved in the project include Prof. Byron Cook and Dr. Reuben Rowe at UCL, and Dr. Nikos Gorogiannis at Middlesex University. For further information about the PPLV group, see http://pplv.cs.ucl.ac.uk . The Research Associate post is funded full-time until *10 May 2017*, and is available immediately. Applicants must hold, or be about to hold, a PhD in computer science or a closely related field, and should have a strong background in verification, automated reasoning, and/or program logics, as evidenced by their work history and/or publication record. Expertise in inductive theorem proving, separation logic and program analysis techniques is particularly welcome, and prior experience in OcaML programming would also be beneficial. The application closing date is *Fri 14 Nov, 2014*, with interviews expected to be held in the week beginning *Mon 1 Dec*. Further information on the position, including salary information and how to apply, may be found at: http://tinyurl.com/mgvvdbu Informal enquiries may also be made toJames by email at j.brothers...@ucl.ac.uk .
[TYPES/announce] RA position in automated verification, logic and theorem proving at UCL
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] *Research Associate positions in Automated Verification, Logic and Theorem Proving * *Dept. of Computer Science, University College London, UK * The UCL Dept. of Computer Science invites applications for a postdoctoral Research Associate to work on the EPSRC-funded project Boosting Automated Verification using Cyclic Proof. Automatic verification tools based on separation logic have recently enabled the verification of code bases that scale into the millions of lines. Such analyses rely heavily on the use of inductive predicates to describe data structures held in memory. However, these predicates must currently be hard-coded into the analysis, which means the analysis must fail when encountering a data structure not described by a hard-coded predicate. This project is about using *cyclic proof*, a relatively new technique in inductive theorem proving, to add general inductive reasoning capability to the various components of interprocedural program analysis and thereby, hopefully, to extend the reach of current verification methods. The project will be run under the supervision of Dr. James Brotherston and Prof. Byron Cook, in the Programming Principles, Logic and Verification (PPLV) group at UCL. Other permanent PPLV members include Prof. David Pym, Dr. Jade Alglave and Dr. Juan Navarro Perez. See pplv.cs.ucl.ac.uk for details. The Research Associate post is funded full-time for 3 years, and is available immediately. Applicants must hold, or be about to hold, a PhD in computer science or a closely related field, and should have a strong background in verification, automated reasoning, or program logics, as evidenced by their work history and/or publication record. Expertise in inductive theorem proving, separation logic and/or program analysis techniques is particularly welcome, and prior experience in OcaML programming would also be beneficial. The application closing date is *14 Feb 2014*, with interviews expected to be held in the period 25-28 February. Further information on the position, including salary information and how to apply, may be found at: http://tinyurl.com/naqk5ze * *Informal enquiries may be made toJames Brotherston by email at **j.brothers...@ucl.ac.uk . With apologies for any duplication of messages. JB
[TYPES/announce] Research positions in Verification, Logic and Theorem Proving at University College London
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Research Associate positions in Verification, Logic and Theorem Proving The University College London (UCL) Dept. of Computer Science invites applications for two postdoctoral Research Associates (RAs) to work on the EPSRC-funded project "Boosting Automated Verification using Cyclic Proof". Automatic verification tools based on separation logic have recently enabled the verification of code bases that scale into the millions of lines. Such analyses rely heavily on the use of inductive predicates to describe data structures held in memory. However, these predicates must currently be hard-coded into the analysis, which means the analysis must fail when encountering a data structure not described by a hard-coded predicate. This project is about using cyclic proof, a relatively new technique in inductive theorem proving, to add general inductive reasoning capability to the various components of interprocedural program analysis and thereby, hopefully, to extend the reach of current verification methods. The project will be run under the supervision of James Brotherston and Byron Cook, in the Programming Principles, Logic and Verification (PPLV) group at UCL, which conducts world-leading research in the area of logic-based program verification. Other researchers in this group include Peter O'Hearn, Thomas Dillig, Juan Navarro Perez and Jade Alglave. For further details go to: http://pplv.cs.ucl.ac.uk The two RA posts are funded at full-time for 3 years, subject to satisfactory performance, and are available immediately. We anticipate that one of the RAs will be more theoretically-focused, and the other more implementation-focused. Applicants must hold, or be about to hold, a PhD in computer science or a closely related field, and should have a strong background in verification, automated reasoning, or program logics, as evidenced by their work history and/or publication record. Expertise in inductive theorem proving, separation logic and/or program analysis techniques is particularly welcome, and prior experience in OcaML programming would also be beneficial. Information on the two postdoctoral RA positions, including how to apply (closing date: 22 August 2013), may be found at: http://tinyurl.com/k5c4x8v Informal enquiries may be made to James Brotherston by email at j.brothers...@ucl.ac.uk
