Re: [Hol-info] VTSA 2018: call for applications
Although the deadline for application has passed, a few places remain available. If you are interested, please send the indicated documents to stephan.m...@loria.fr <mailto:stephan.m...@loria.fr>: registrations remain possible until the remaining slots have been filled. Thank you, Stephan Merz > On 6 Jun 2018, at 14:34, Stephan Merz wrote: > > UniGR Summer School on Verification Technology, Systems and Applications > (VTSA 2018) > > August 27-31, 2018, Nancy, France > > The summer school on verification technology, systems & applications focuses > on fundamental aspects of verification techniques, their implementation, and > their use for concrete applications. It is organized by Inria Nancy, the > Max-Planck-Institut für Informatik in Saarbrücken, and the Universities of > Liège and of Luxembourg, and will take place at the research center Inria > Nancy – Grand Est in Nancy, France, from August 27 to 31, 2018. > > The following speakers have agreed to lecture at the school: > > - David Basin: Formal Methods for Security Protocols > - Jean-Christophe Filliâtre: An Introduction to Deductive Program Verification > - Peter Lammich: Algorithm Verification with the Isabelle Refinement Framework > - Anca Muscholl: Distributed Synthesis > - Carsten Sinz: Bounded Model Checking of Software for Real-World Applications > > Participation to the school is free to anybody holding at least a bachelor > degree or equivalent; it includes the lectures, coffee and lunch breaks, and > a school dinner. Attendance is limited to 40 participants. Please apply > electronically by sending an email to Stephan Merz (stephan.m...@loria.fr) > including > > - a one-page CV, > - an application letter explaining your interest in the school and your > experience in the area, and > - a copy of your bachelor (or equivalent or higher) certificate. > > The deadline for application is July 8, 2018. Notification of acceptance will > be given by July 11, 2018. > > Full details can be found on the school Web page at > https://www.mpi-inf.mpg.de/vtsa18. > -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] VTSA 2018: call for applications
UniGR Summer School on Verification Technology, Systems and Applications (VTSA 2018) August 27-31, 2018, Nancy, France The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organized by Inria Nancy, the Max-Planck-Institut für Informatik in Saarbrücken, and the Universities of Liège and of Luxembourg, and will take place at the research center Inria Nancy – Grand Est in Nancy, France, from August 27 to 31, 2018. The following speakers have agreed to lecture at the school: - David Basin: Formal Methods for Security Protocols - Jean-Christophe Filliâtre: An Introduction to Deductive Program Verification - Peter Lammich: Algorithm Verification with the Isabelle Refinement Framework - Anca Muscholl: Distributed Synthesis - Carsten Sinz: Bounded Model Checking of Software for Real-World Applications Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to Stephan Merz (stephan.m...@loria.fr) including - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, and - a copy of your bachelor (or equivalent or higher) certificate. The deadline for application is July 8, 2018. Notification of acceptance will be given by July 11, 2018. Full details can be found on the school Web page at https://www.mpi-inf.mpg.de/vtsa18. -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] VTSA summer school
Dear colleagues, the VTSA summer school may be of interest to the interactive theorem proving community. Also note that it takes place in the week following ITP 2016, and that Liège, Belgium, is easily reached from Nancy, France. I would be most obliged if you could pass on this announcement to interested students and colleagues. Best regards, Stephan Merz == Summer School on Verification Technology, Systems & Applications http://www.mpi-inf.mpg.de/vtsa16/ The 9th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by the University of Liège, in cooperation with Inria Nancy - Grand Est, Max-Planck-Institut für Informatik Saarbrücken, Université du Luxembourg, and Universität Koblenz-Landau. The school will take place from August 29th to September 2nd, 2016 at the Montefiore Institute in Liège, Belgium. The following speakers have accepted to give courses at VTSA 2016: - Hubert Comon: Communication security: Formal models and proofs - Thomas Eiter: Answer set programming and extensions - Jean Krivine: Executable knowledge representation in systems biology: The rule-based approach - Tobias Nipkow: Introduction to interactive proof with Isabelle/HOL - Ruzica Piskac: SMT-based verification of heap-manipulating Programs Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science; it includes the lectures, daily coffee and lunchbreaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending to vts...@montefiore.ulg.ac.be: - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, - a copy of your bachelor certificate (or equivalent or a more significant certificate). The deadline for application is July 12th, 2016. Notification of acceptance will be given by July 15th, 2016. Full details are available at http://www.mpi-inf.mpg.de/vtsa16/ -- Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] opening for a research engineer (post-doc) at MSR-INRIA Centre
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 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 th
[Hol-info] opening for a research engineer (post-doctoral) position at MSR-INRIA centre
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 , preferably by
[Hol-info] Call for participation : VTSA 2014
Summer School on Verification Technology, Systems and Applications October 27-31, 2014, University of Luxembourg, Luxembourg The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organised by the Universities of Liège and of Luxembourg, the Max-Planck-Institut für Informatik in Saarbrücken, and the Inria Research Center in Nancy, and will take place at the Interdisciplinary Centre for Security, Reliability and Trust in University of Luxembourg, Luxembourg from October 27-31, 2014. This year it is a co-located event with ICFEM 2014, which will be held in Luxembourg from November 3-7, 2014. PhD students can apply scholarships in order to attend the conference ICFEM 2014 as well. More details are available on the Web site http://icfem2014.uni.lu. The following speakers have agreed to lecture at the school: - Nikolaj Bjorner: Software Verification by Solving Horn Clauses - Laura Kovács: Symbolic Computation and Theorem Proving in Program Analysis - Joel Ouaknine: A Survey of Program Termination: Practical and Theoretical Challenges - Jaco van de Pol: Scalable Multi-core Model Checking: Technology & Applications of Brute Force - Helmut Veith: Model Checking of Fault-Tolerant Distributed Algorithms Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, daily coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to Eugen Denerz (edenerz_AT_mpi-inf.mpg.de) including - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, and - a copy of your bachelor (or equivalent or higher) certificate. The deadline for application is September 05, 2014. Notification of acceptance will be given by September 12, 2014. Full details can be found on the school Web page at http://www.mpi-inf.mpg.de/VTSA14/. -- Slashdot TV. Video for Nerds. Stuff that matters. http://tv.slashdot.org/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] VTSA 2014 : school on verification technology, systems and applications
Summer School on Verification Technology, Systems and Applications October 27-31, 2014, University of Luxembourg, Luxembourg The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organised by the Universities of Liège and of Luxembourg, the Max-Planck-Institut für Informatik in Saarbrücken, and the Inria Research Center in Nancy, and will take place at the Interdisciplinary Centre for Security, Reliability and Trust in University of Luxembourg, Luxembourg from October 27-31, 2014. This year it is a co-located event with ICFEM 2014, which will be held in Luxembourg from November 3-7, 2014. PhD students can apply for scholarships in order to attend the conference ICFEM 2014 as well. More details will be available on the following website icfem2014.uni.lu. The following speakers have agreed to lecture at the school: - Nikolaj Bjorner: Software Verification by Solving Horn Clauses - Laura Kovács: Symbolic Computation and Theorem Proving in Program Analysis - Joel Ouaknine: A Survey of Program Termination: Practical and Theoretical Challenges - Jaco van de Pol: Scalable Multi-core Model Checking: Technology & Applications of Brute Force - Helmut Veith: Model Checking of Fault-Tolerant Distributed Algorithms Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, daily coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to Eugen Denerz (edenerz_AT_mpi-inf.mpg.de) including - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, and - a copy of your bachelor (or equivalent or higher) certificate. The deadline for application is September 05, 2014. Notification of acceptance will be given by September 12, 2014. Full details can be found on the school Web page at http://www.mpi-inf.mpg.de/VTSA14/. -- "Accelerate Dev Cycles with Automated Cross-Browser Testing - For FREE Instantly run your Selenium tests across 300+ browser/OS combos. Get unparalleled scalability from the best Selenium testing platform available Simple to use. Nothing to install. Get started now for free." http://p.sf.net/sfu/SauceLabs ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] call for applications summer school VTSA 2013
Summer School on Verification Technology, Systems and Applications September 2-6, 2013, Nancy, France The summer school on verification technology, systems & applications focuses on fundamental aspects of verification techniques, their implementation, and their use for concrete applications. It is organized by the Universities of Liège and of Luxembourg, the Max-Planck-Institut für Informatik in Saarbrücken, and the Inria Research Center in Nancy, and will take place at the Inria Center in Nancy, France from September 2-6, 2013. The following speakers have agreed to lecture at the school: - Xavier Leroy: Mechanized semantics with applications to program proof and compiler verification - Konstantin Korovin: Automated reasoning for first-order logic: theory, practice and challenges - Torsten Schaub: Answer Set Solving in Practice - Swen Jacobs: Reactive Synthesis - Kim Larsen: TBA Participation to the school is free to anybody holding at least a bachelor degree or equivalent; it includes the lectures, daily coffee and lunch breaks, and a school dinner. Attendance is limited to 40 participants. Please apply electronically by sending an email to lamotte (at) mpi-inf.mpg.de including - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, and - a copy of your bachelor (or equivalent or higher) certificate. The deadline for application is July 20, 2013. Notification of acceptance will be given by July 27, 2013. Full details can be found on the school Web page at http://www.mpi-inf.mpg.de/VTSA13/. -- AlienVault Unified Security Management (USM) platform delivers complete security visibility with the essential security capabilities. Easily and efficiently configure, manage, and operate all of your security controls from a single console and one unified framework. Download a free trial. http://p.sf.net/sfu/alienvault_d2d ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] iFM 2010: final CFP and deadline extension
[New information: extended deadlines, invited speakers, satellite events] Apologies for multiple copies of this CFP CALL FOR PAPERS 8th International Conference on Integrated Formal Methods (iFM 2010) October 11-14, 2010, Nancy, France http://ifm2010.loria.fr/ Applying formal methods may involve the modeling of different aspects of a system that are expressed through different paradigms. Correspondingly, different analysis techniques will be used to examine differently modeled system views, different kinds of properties, or simply in order to cope with the sheer complexity of the system. The iFM conference series seeks to further research into the combination of (formal and semi-formal) methods for system development, regarding modeling and analysis, and covering all aspects from language design through verification and analysis techniques to tools and their integration into software engineering practice. Areas of interest include but are not limited to: - Integration of formal modeling and analysis methods - Integration of formal and semi-formal modeling and analysis methods - Integration of formal methods into software engineering practice - Semantics, Logics, Type systems - Verification, Model checking, Static analysis, Theorem proving - Refinement, Model transformations - Tools, Experience reports, Case studies Invited Speakers: - Christel Baier, TU Dresden - John Fitzgerald, Newcastle University - Rajeev Joshi, Laboratory for Reliable Software, JPL iFM 2010 solicits high quality papers reporting research results and/or experience reports related to the overall theme of method integration. All papers must be original, unpublished, and not submitted for publication elsewhere. Submission will be electronically as PDF or Postscript, using the Springer LNCS format. Papers should not exceed 15 pages in length. Each paper will undergo a thorough review process. The conference proceedings will be published by Springer Verlag in the LNCS series. Important Dates: - Abstract submission: May 21, 2010 (* extended *) - Full paper submission: May 28, 2010 (*extended *) - Notification: July 4, 2010 - Final version: July 18, 2010 Satellite events: - Workshop "Formal Methods for Web Data Trust and Security" (WTS 2010) http://acxml.gforge.inria.fr/WTS10 - Tutorial "Verification of C# programs using Spec# and Boogie 2" by Rosemary Monahan - Tutorial "The TLA+ Proof System" by Denis Cousineau and Stephan Merz Contact: ifm2...@loria.fr -- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
