As a follow-up to this announcement, we have now secured funding for a 24-month period for this post-doctoral position. The other information given in the original posting is still accurate. Apologies for resending.
Stephan Merz On 10 Sep 2014, at 17:32, Stephan Merz <stephan.m...@loria.fr> wrote: > Research team: Tools for Proofs, MSR-INRIA Joint Centre > ======================================================= > > The Microsoft Research-INRIA Joint Centre is offering a 14-month position for > a research engineer to contribute to the ADN4SE project. We hope the position > will be extended to 18 months, but are not yet sure this will be possible. > > The engineer will contribute to extending the TLA+ Proof System (TLAPS, > http://msr-inria.com/projects/tools-for-proofs) and will assist domain > experts in applying TLAPS for proving fundamental properties of PharOS, a > real-time operating system. > > > Research Context > ================ > > TLA+ is a language for specifying and reasoning about systems, including > concurrent and distributed systems. It is based on first-order logic, set > theory, and temporal logic. TLA+ and its tools have been used in industry for > over a decade. More recently, we have extended TLA+ by a language for > writing structured formal proofs and have developed TLAPS, a proof checker > that contains an interpreter for the proof language and integrates different > back-end provers. TLAPS is integrated into the TLA+ Toolbox, an IDE for TLA+ > (http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html). > > Although it is still under active development, TLAPS is already quite > powerful and has been used for a few verification projects, in particular in > the realm of distributed algorithms (e.g., > http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html). > > The current version of TLAPS handles the "action" part of TLA+: first-order > formulas with primed and unprimed variables that represent the values of a > variable before and after a transition. It also supports the propositional > fragment of temporal logic. This fragment is enough for proving safety > properties (invariants and step simulation). We are currently refactoring the > code base and preparing support for full temporal logic of TLA+, which will > allow us to prove liveness and refinement properties. > > > Description of the activity of the research engineer > ==================================================== > > The research engineer (post-doctoral) position is funded by the PIA ADN4SE > project (http://www.systematic-paris-region.org/en/projets/adn4se) that > develops a real-time operating system and development tools for embedded > systems based on PharOS. The system aims at providing certifiable correctness > and performance guarantees, and fundamental properties of the operating > system, such as determinacy, are formally verified using the TLA+ notation > and tools. > > Your work will make a key contribution to this verification effort. In > particular, you will work with members of the TLA+ project at the Microsoft > Research - INRIA Joint Centre, including Damien Doligez, Leslie Lamport, and > Stephan Merz on extending the TLA+ Proof System and its libraries. You will > also work with the project partners of ADN4SE, and in particular members of > CEA List, on modeling the protocols subject to verification and on carrying > out the proofs. Your contributions will be conceptual, by identifying > theories and patterns that underly the verification of the operating system, > and practical, by implementing formal libraries and software in order to > carry out the verification task. > > You will also have the opportunity to contribute to further improving the > proof checker, for example by adding support for certain TLA+ features that > are not yet handled by TLAPS, integrating new back-end provers, or extending > the capabilities for proof validation. > > > Skills and profile of the candidate > =================================== > > You should hold a PhD in computer science and have solid knowledge of > mathematical logic as well as implementation skills related to symbolic > theorem proving. Our tools are mainly implemented in OCaml. Some basic > familiarity with concepts of real-time systems is a plus. Experience with > temporal and modal logics, with interactive theorem provers or with Eclipse > could be valuable. > > Working on the project provides the opportunity to learn about the issues of > using verification in practice, and it has in the past and may continue in > the future to produce published research. However, the main focus is on > practical applications and on the implementation of components of our tool > chain that are missing or need improvement. > > Given the geographical distribution of the members of the team, we highly > value a good balance between the ability to work in a team and the capacity > to propose initiatives. > > Location > ======== > > The research engineer will be based at the INRIA research center in Nancy > (http://www.inria.fr/en/centre/nancy). Located in the North-East of France, > Nancy is a university town whose metropolitan area has about 400,000 > inhabitants. It is 1-1/2 hours from Paris by TGV. > > > Contact > ======= > > Candidates should send a resume and the names and e-mail addresses of two > references to Damien Doligez <damien.doli...@inria.fr>, preferably by > September 22, 2014. > > We intend to hire the research engineer by November 2014, although the exact > date is negotiable. > > This announcement is available at > http://www.msr-inria.com/open_positions/research-engineer-position-on-tla-tools/ > ------------------------------------------------------------------------------ Want excitement? Manually upgrade your production database. When you want reliability, choose Perforce. Perforce version control. Predictably reliable. http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
