[TYPES/announce] IWS 2010: Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] - CALL FOR PARTICIPATION: IWS 2010 International Workshop on Strategies in Rewriting, Proving, and Programming Edinburgh, Scotland, July 9, 2010 http://iws2010.inria.fr iws2010 AT inria DOT fr Affiliated with FLoC (July 9-21, 2010) http://www.floc-conference.org EARLY REGISTRATION DEADLINE: May 17 - Strategies are ubiquitous in programming languages, automated deduction and reasoning systems. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engines (Provers, Assistants, Solvers) on the other side, workshops have been launched to make progress towards a deeper understanding of the nature of strategies, their descriptions, their properties, and their usage, in all kinds of computing and reasoning systems. Since more recently, strategies are also playing an important role in rewrite-based programming languages, verification tools and techniques like SAT/SMT engines or termination provers. Moreover strategies have come to be viewed more generally as expressing complex designs for control in computing, modeling, proof search, program transformation, and access control. FLoC 2010 provides an excellent opportunity to foster exchanges between the communities of Rewriting and Programming on one side, and of Deduction and Proof engines on the other side. This workshop is a joint follow-up of two series of workshops, held since 1997: the Strategies workshops held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community. INVITED TALKS Dan Dougherty, Worcester Polytechnic Institute: Game Strategies and Rule-Based Systems Assia Mahboubi, INRIA: Organizing and Using Algebraic Structures in Large Developments of Formalized Mathematics TECHNICAL PROGRAM Pascal Fradet, Jean-Louis Giavitto and Marnes Hoff: Refinement of Chemical Programs Using Strategies Alvaro Garcia, Pablo Nogueira and Emilio Jesus Gallego Arias: The Beta Cube Alex Gerdes, Bastiaan Heeren and Johan Jeuring: Properties of Exercise Strategies Bernhard Gramlich and Felix Schernhammer: Termination of Rewriting with - and Automated Synthesis of - Forbidden Patterns Ian Mackie: Closed Cut-Elimination in Linear Logic Olivier Namet and Maribel Fernandez: A Strategy Language for Graph Rewriting Systems Detlef Plump: Graph Programs Rene Thiemann, Jurgen Giesl, Peter Schneider-Kamp and Christian Sternagel: Loops under Strategies ... Continued PROGRAM COMMITTEE Maria Paola Bonacina, Universita degli Studi di Verona, Italy Jean-Christophe Filliatre, CNRS, France Bernhard Gramlich, Technische Universitaet Wien, Austria Salvador Lucas, Universidad Politecnica de Valencia, Spain Pierre-Etienne Moreau, INRIA-LORIA Nancy, France Natarajan Shankar, SRI International, United States Eelco Visser, Delft University of Technology, Netherlands Christoph Weidenbach, Max Planck Institute for Informatics, Germany ORGANIZERS and CHAIRS Helene Kirchner, INRIA, France Cesar Munoz, NASA, US REGISTRATION (Through FLoC 2010) http://www.floc-conference.org/registration.html
[TYPES/announce] Call for Participation NFM 2010
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PARTICIPATION: 2nd NASA Formal Methods Symposium - The NASA Formal Methods community invites you to attend the Second NASA Formal Methods Symposium (NFM 2010) http://shemesh.larc.nasa.gov/NFM2010 nfm2...@lists.nasa.gov April 13-15, 2010 Washington D.C. Theme of Conference The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. Invited Speakers Nikolaj Bjorner, Microsoft Guillaume Brat, NASA John Harrison, Intel John Kelly, NASA http://shemesh.larc.nasa.gov/NFM2010/speakers.html Program The program committee selected 20 regular papers and 4 short papers for presentation, covering various aspects of the theory and practice of formal methods in safety-critical domains. http://shemesh.larc.nasa.gov/NFM2010/program.html Registration Attendance to the symposium is free, but all attendees must register in order to participate. Registration closes April 9, 2010. http://shemesh.larc.nasa.gov/NFM2010/registration.html Travel and Local Information The conference will take place in the James Webb Memorial Auditorium at NASA Headquarters in Washington D.C. http://shemesh.larc.nasa.gov/NFM2010/local.html Note that there are room blocks reserved at two hotels. These reservations will expire in the March 13-15 time frame. http://shemesh.larc.nasa.gov/NFM2010/travel.html Contact Mike Hinchey, Conference Chair Cesar Munoz, Program Chair nfm2...@lists.nasa.gov
[TYPES/announce] 2nd Call for Papers IWS2010
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 2nd CALL FOR PAPERS International Workshop on Strategies in Rewriting, Proving, and Programming IWS 2010 iws2010.inria.fr (A satellite workshop of FLoC 2010) July 9 2010, Edinburgh, UK *** IMPORTANT DATES *** Abstract submission: March 26, 2010 Notification date: April 11, 2010 Abstract final version: April 25, 2010 Workshop: July 9, 2010 Submission of full paper for the proceedings: September 5, 2010 Strategies are ubiquitous in programming languages, automated deduction and reasoning systems, yet only since about ten years have they been studied in their own right. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engines (Provers, Assistants, Solvers) on the other side, workshops have been launched to make progress towards a deeper understanding of the nature of strategies, their descriptions, their properties, and their usage, in all kinds of computing and reasoning systems. Since more recently, strategies are also playing an important role in rewrite-based programming languages, verification tools and techniques like SAT/SMT engines or termination provers. Moreover strategies have come to be viewed more generally as expressing complex designs for control in computing, modeling, proof search, program transformation, and access control. Possible topics to address in this workshop include: * Foundations for the definition and semantic description of strategies: models of search spaces, logical or mathematical formalisms to define strategies and prove properties about them. * Properties of strategies and corresponding computations: logical or mathematical formalisms to prove properties about them. * Analysis and optimization techniques for strategies: analysis of the search space, evaluation and comparison of strategies. * Integration of strategic deductions and/or strategic computations: interrelations, combinations and applications of deduction and computation under different strategies, control issues and strategies in the integration of systems, strategies in decision procedures for SMT. * Strategy languages: essential constructs, meta-level features. Definition, design, implementation and application. Comparison of strategies in (existing) systems. * Concrete types of (reduction/evaluation) strategies in rewriting and programming, lambda calculi, normalization, narrowing, constraint solving, as well as their properties and characteristics (complexity, decidability, ...). * Applications and case studies in which strategies play a major role. FLoC 2010 provides an excellent opportunity to foster exchanges between the communities of Rewriting and Programming on one side, and of Deduction and Proof engines on the other side. This workshop is a joint follow-up of two series of workshops, held since 1997: the Strategies workshops held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community. Submissions -- The submission process is in two stages. 1) Before the workshop, authors are invited to submit an extended abstract (max. 5 pages) to be formatted in the EasyChair class style http://www.easychair.org/easychair.zip through the EasyChair submission site: http://www.easychair.org/conferences/?conf=iws2010 Accepted abstracts will be presented at the workshop and included in the preliminary proceedings, available at the workshop. 2) After the workshop, authors will be invited to submit a full paper of their presentation (typically a 15-pages paper), which will be refereed and considered for publication in the electronic journal: Electronic Proceedings in Theoretical Computer Science (http://eptcs.org). Beyond original ideas and recent results not published nor submitted elsewhere, we also invite authors to submit a 5-pages abstract describing relevant work that has been or will be published elsewhere, or work in progress. These submissions will be only considered for presentation at the workshop and inclusion in the preliminary proceedings but not in the final proceedings. Invited Speakers - Dan Dougherty, Worcester Polytechnic Institute http://web.cs.wpi.edu/~dd/ Assia Mahboubi, INRIA Saclay http://www.lix.polytechnique.fr/~assia/index-eng.html Organizers - Helene Kirchner, INRIA Bordeaux - Sud-Ouest, France Cesar Munoz, NASA Langley Research Center, Hampton, USA Program Committee - Maria Paola Bonacina, Univ. degli Studi di Verona, Italy Jean-Christophe Filliatre, CNRS, France Bernhard Gramlich, Technische Universitat Wien, Austria Salvador Lucas, Universidad Politecnica de Valencia, Spain Pierre-Etienne Moreau, LORIA-INRIA Nancy, France Natarajan Shankar, SRI
[TYPES/announce] NFM 2010 (Last Call for Papers)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] --- LAST CALL FOR PAPERS: 2nd NASA Formal Methods Symposium --- The NASA Formal Methods community invites you to submit a paper to: The Second NASA Formal Methods Symposium (NFM 2010) Web: http://shemesh.larc.nasa.gov/NFM2010 Email: nfm2...@lists.nasa.gov April 13-15, 2010 Washington D.C. -- IMPORTANT DATES: -- *** Submission (abstract): January 8, 2010 *** *** Submission (final): January 15, 2010 *** Notification: February 26, 2010 Final version: March 19, 2010 -- Theme of Conference: -- The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. Within NASA, for example, such systems include autonomous robots, separation assurance algorithms for aircraft, and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as code generation and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. The symposium aims to introduce researchers, graduate students, and partners in industry to those topics that are of interest, to survey current research, and to identify unsolved problems and directions for future research. NFM 2010 is the second edition of the NASA Formal Methods Symposium, which started in 2009 and was organized by NASA Ames Research Center in Moffet Field, California. The symposium originated from the earlier Langley Formal Methods Workshop series and aims to foster collaboration between NASA researchers and engineers, as well as the wider aerospace, safety-critical, and formal methods communities. -- Topics of Interest: -- * Formal verification, including theorem proving, model checking, and static analysis * Automated test generation and formal testing of critical systems * Model-based development * Techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and distributed techniques * Monitoring and run-time verification * Code generation from formally verified models * Safety cases * Accident/safety analysis * Formal approaches to fault tolerance * Theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems * Formal methods in systems engineering -- Submissions: -- There are two categories of submissions, to be formatted in the EasyChair class style (http://www.easychair.org/coolnews.cgi): * Regular papers describing fully developed work and complete results (10 pages / 30 minute talks) * Short papers describing interesting work in progress and/or preliminary results (5 pages / 15 minute talks) All papers should describe original work that has not been published elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a NASA Conference Publication. Authors of selected papers will then be invited to submit extended versions to a special issue of Innovations in Systems and Software Engineering: a NASA Journal (Springer). Papers should be submitted through the following link: http://www.easychair.org/conferences/?conf=nfm2010 -- For further information: -- http://shemesh.larc.nasa.gov/NFM2010/ nfm2...@lists.nasa.gov Mike Hinchey NFM 2010 Conference Chair Cesar A. Munoz NFM 2010 Program Chair
[TYPES/announce] Call for Papers: IWS 2010
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PAPERS International Workshop on Strategies in Rewriting, Proving, and Programming IWS 2010 iws2010.inria.fr (A satellite workshop of FLoC 2010) July 9 2010, Edinburgh, UK Abstract submission: March 26, 2010 Notification date: April 11, 2010 Abstract final version: April 25, 2010 Workshop: July 9, 2010 Submission of full paper for the proceedings: September 5, 2010 Strategies are ubiquitous in programming languages, automated deduction and reasoning systems, yet only since about ten years have they been studied in their own right. In the two communities of Rewriting and Programming on one side, and of Deduction and Proof engines (Provers, Assistants, Solvers) on the other side, workshops have been launched to make progress towards a deeper understanding of the nature of strategies, their descriptions, their properties, and their usage, in all kinds of computing and reasoning systems. Since more recently, strategies are also playing an important role in rewrite-based programming languages, verification tools and techniques like SAT/SMT engines or termination provers. Moreover strategies have come to be viewed more generally as expressing complex designs for control in computing, modeling, proof search, program transformation, and access control. Possible topics to address in this workshop include: * Foundations for the definition and semantic description of strategies: models of search spaces, logical or mathematical formalisms to define strategies and prove properties about them. * Properties of strategies and corresponding computations: logical or mathematical formalisms to prove properties about them. * Analysis and optimization techniques for strategies: analysis of the search space, evaluation and comparison of strategies. * Integration of strategic deductions and/or strategic computations: interrelations, combinations and applications of deduction and computation under different strategies, control issues and strategies in the integration of systems, strategies in decision procedures for SMT. * Strategy languages: essential constructs, meta-level features. Definition, design, implementation and application. Comparison of strategies in (existing) systems. * Concrete types of (reduction/evaluation) strategies in rewriting and programming, lambda calculi, normalization, narrowing, constraint solving, as well as their properties and characteristics (complexity, decidability, ...). * Applications and case studies in which strategies play a major role. FLoC 2010 provides an excellent opportunity to foster exchanges between the communities of Rewriting and Programming on one side, and of Deduction and Proof engines on the other side. This workshop is a joint follow-up of two series of workshops, held since 1997: the Strategies workshops held by the CADE-IJCAR community and the Workshops on Reduction Strategies (WRS) held by the RTA-RDP community. Submissions -- The submission process is in two stages. 1) Before the workshop, authors are invited to submit an extended abstract (max. 5 pages) to be formatted in the EasyChair class style http://www.easychair.org/easychair.zip through the EasyChair submission site: http://www.easychair.org/conferences/?conf=iws2010 Accepted abstracts will be presented at the workshop and included in the preliminary proceedings, available at the workshop. 2) After the workshop, authors will be invited to submit a full paper of their presentation (typically a 15-pages paper), which will be refereed and considered for publication in the electronic journal: Electronic Proceedings in Theoretical Computer Science (http://eptcs.org). Beyond original ideas and recent results not published nor submitted elsewhere, we also invite authors to submit a 5-pages abstract describing relevant work that has been or will be published elsewhere, or work in progress. These submissions will be only considered for presentation at the workshop and inclusion in the preliminary proceedings but not in the final proceedings. Organizers - Helene Kirchner, INRIA Bordeaux - Sud-Ouest, France Cesar Munoz, NASA Langley Research Center, Hampton, USA Program Committee - Maria Paola Bonacina, Univ. degli Studi di Verona, Italy Jean-Christophe Filliatre, CNRS, France Bernhard Gramlich, Technische Universitat Wien, Austria Salvador Lucas, Universidad Politecnica de Valencia, Spain Pierre-Etienne Moreau, LORIA-INRIA Nancy, France Natarajan Shankar, SRI International, Menlo Park, CA, USA Eelco Visser, Delft Univ. of Technology, The Netherlands Christoph Weidenbach, MPI-INF, Saarbrucken, Germany Web: iws2010.inria.fr Email: iws2...@inria.fr
[TYPES/announce] CFP: NASA Formal Methods Symposium 2010
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We apologize if you receive this message more than once. Please circulate the information among your colleagues and students. -- CALL FOR PAPERS: 2nd NASA Formal Methods Symposium -- The NASA Formal Methods community invites you to submit a paper to: The Second NASA Formal Methods Symposium (NFM 2010) http://shemesh.larc.nasa.gov/NFM2010 April 13-15, 2010 Washington D.C. -- Important Dates: -- Submission (abstract): January 8, 2010 Submission (final): January 15, 2010 Notification: February 26, 2010 Final version: March 19, 2010 -- Theme of Conference: -- The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia and industry, with the goals of identifying challenges and providing solutions to achieving assurance in safety-critical systems. Within NASA, for example, such systems include autonomous robots, separation assurance algorithms for aircraft, and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as code generation and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other safety-critical systems. The symposium aims to introduce researchers, graduate students, and partners in industry to those topics that are of interest, to survey current research, and to identify unsolved problems and directions for future research. NFM 2010 is the second edition of the NASA Formal Methods Symposium, which started in 2009 and was organized by NASA Ames Research Center in Moffet Field, California. The symposium originated from the earlier Langley Formal Methods Workshop series and aims to foster collaboration between NASA researchers and engineers, as well as the wider aerospace, safety-critical, and formal methods communities. -- Topics of Interest: -- * Formal verification, including theorem proving, model checking, and static analysis * Automated test generation and formal testing of critical systems * Model-based development * Techniques and algorithms for scaling formal methods, such as abstraction and symbolic methods, compositional techniques, as well as parallel and distributed techniques * Monitoring and run-time verification * Code generation from formally verified models * Safety cases * Accident/safety analysis * Formal approaches to fault tolerance * Theoretical advances and empirical evaluations of formal methods techniques for safety-critical systems, including hybrid and embedded systems * Formal methods in systems engineering -- Submissions: -- Submitted papers must be formatted in the EasyChair class style (http://www.easychair.org/coolnews.cgi). There are two categories of submissions (to be in NASA conference style): * Regular papers describing fully developed work and complete results (10 pages / 30 minute talks) * Short papers describing interesting work in progress and/or preliminary results (5 pages / 15 minute talks) All papers should describe original work that has not been published elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a NASA Conference Publication. Authors of selected papers will then be invited to submit extended versions to a special issue of Innovations in Systems and Software Engineering: a NASA Journal (Springer). Papers should be submitted through the following link: http://www.easychair.org/conferences/?conf=nfm2010 -- For further information: -- http://shemesh.larc.nasa.gov/NFM2010/ nfm2...@lists.nasa.gov Mike Hinchey NFM 2010 Conference Chair Cesar Munoz NFM 2010 Program Chair
