Nela Cicmil | 17 Sep 14:14 2014
Picon
Picon

Re: advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

Thanks very much to Marco, Mark and Ramana for your replies. I may have made some progress using Nix:


 <at>  Marco: Following your suggestion I installed Nix and HOL Light with the following commands on terminal
(after creating a /nix directory under my user account): 

$ bash <(curl https://nixos.org/nix/install)

$ source /Users/nc/.nix-profile/etc/profile.d/nix.sh
$ nix-channel --add http://nixos.org/channels/nixpkgs-unstable

$ nix-channel --update
$ nix-env -i hol_light

and all seemed to complete without errors. My question is, if HOL Light is now installed on my machine,
what's the best way to run it? The standard way through ocaml doesn't seem to be able to find the hol.ml
file… should I fix some path, or is there another way to run the program when installed via nix?

$ ocaml
        OCaml version 4.01.0

# #use "hol.ml";;
Cannot find file hol.ml.

(NB. If I just type "hol_light" onto the command line, it spews a seemingly never-ending list of warnings
and errors… not sure why.)


 <at>  Mark:  I used the svn download command only this week so probably it has the most recent version of HOL Light.
On svn download, I get the output "Checked out revision 198", and the CHANGES document inside the
hol_light directory is dated 9th Sept 2014. Here are my ocaml and camlp5 versions:

(Continue reading)

"Mark Adams" | 17 Sep 05:23 2014

Flyspeck Project completion

For those to whom the news has not already reached, Tom Hales'
Flyspeck Project is now complete!  This establishes a formal proof of
Hales' 1998 Kepler Conjecture proof, and is a landmark in the
formalisation of mathematics.  The formal proof was mainly done in HOL
Light, but with one part (the classification of tame hypermaps) done
in Isabelle/HOL.  It involves hundreds of thousands of lines of proof
script, resulting in billions of primitive inferences.  I include
below Hales' original announcement from 5 weeks ago.

Mark.

-----------------------------------------

We are pleased to announce the completion of the Flyspeck project,
which has constructed a formal proof of the Kepler conjecture.  The
Kepler conjecture asserts that no packing of congruent balls in
Euclidean 3-space has density greater than the face-centered cubic
packing.  It is the oldest problem in discrete geometry.  The proof of
the Kepler conjecture was first obtained by Ferguson and Hales in
1998.  The proof relies on about 300 pages of text and on a large
number of computer calculations.

The formalization project covers both the text portion of the proof
and the computer calculations.  The blueprint for the project appears
in the book "Dense Sphere Packings," published by Cambridge University
Press.  The formal proof takes the same general approach as the
original proof, with modifications in the geometric partition of space
that have been suggested by Marchal.

----
(Continue reading)

"Mark Adams" | 17 Sep 05:50 2014

Re: advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

Hi Nela,

There have been various problems over the years, but I get no problems with
recent versions of HOL Light (downloaded since May 2014, including SVN
version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
running on Fedora 17.

Do you know the HOL Light SVN version (or otherwise, what date did you
download)?

And can you please check your OCaml and Camlp5 versions by executing the
following from the same terminal window from which you are trying the HOL
Light make?:
   ocaml -version
   camlp5 -v

Mark.

on 16/9/14 4:45 PM, Nela Cicmil <nela.cicmil <at> dpag.ox.ac.uk> wrote:

> Dear HOL Light users,
>
> Would anyone be able to please advise me on how to install HOL Light on my
> Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.
>
> My trouble is that I can't seem to get compatible versions of Ocaml,
camlp5
> and HOL Light installed on my system, mainly because the Ocaml version
that
> comes with OPAM, v 4.01.0, seems to be too recent to run with the slighter
(Continue reading)

Nela Cicmil | 16 Sep 16:31 2014
Picon
Picon

advice on installing Ocaml, camlp5 & HOL Light on Mac OS X 10.8.5?

Dear HOL Light users, 

Would anyone be able to please advise me on how to install HOL Light on my Mac? It's a MacBook Pro OS X 10.8.5
Intel core i5.

My trouble is that I can't seem to get compatible versions of Ocaml, camlp5 and HOL Light installed on my
system, mainly because the Ocaml version that comes with OPAM, v 4.01.0, seems to be too recent to run with
the slighter older camlp5 versions compatible with HOL Light. 

Has anyone recently installed HOL Light on a Mac, and has advice on which versions of Ocaml and camlp5 to
install, and which procedure to use to install them? In particular, is it possible to install an older
version of Ocaml, e.g. v 3.12, using OPAM?

The specific issues I've encountered are detailed below. Any advice would be much appreciated.

Thank you, 

Best wishes, 
Nela                
----
Nela Cicmil, D.Phil
Dept. Physiology, Anatomy & Genetics,
University of Oxford
----

After various attempts to install Ocaml on the Mac, I installed (using homebrew) the latest version of
OPAM, which comes with Ocaml version 4.01.0. On basic testing at the terminal, Ocaml seemed to be working
fine. I then installed camlp5 version 6.11, using ./configure --transitional mode, and that seemed to be
running fine as well. When I then attempted to install HOL Light, using the svn checkout
http://hol-light.googlecode.com/svn/trunk/ hol_light procedure, and got the following error on "make":
(Continue reading)

Stephan Merz | 10 Sep 17:33 2014
Picon

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.

(Continue reading)

Jiaqi Tan | 9 Sep 03:13 2014
Picon

Problems with METIS_TAC: Crashing with exception raised in CHOOSE

Hi,

I have a question about the internals of METIS_TAC, whether my proof succeeded, and whether there might be problems with trying to prove my theorem with METIS_TAC.

I set the trace for METIS_TAC to 5, and in the trace feedback, the last line of the proof from the METIS feedback was:

(11) |- F
     [Resolve
      {res = ~set_sep.SEP_IMP (set_sep.STAR (prog_arm.aPC offset'') r) s,
       pos = (9), neg = (10)}]
END OF PROOF

Does this mean that my proof succeeded?

At the same time, I also got the following error at the end of METIS_TAC:
metis: proof translation time: 0.233517
Exception-
   HOL_ERR
  {message = "", origin_function = "CHOOSE", origin_structure = "Thm"} raised

Is the error occurring during the proof process, or is the error occurring during the post-processing to generate the theorem after the proof was completed?

I also get the same problem when, instead of METIS_TAC, I use REWRITE_TAC or SIMP_TAC using the same theorem list passed to METIS_TAC, although I also received the same trace/feedback messages from METIS_TAC when I used REWRITE_TAC/SIMP_TAC so presumably it was because REWRITE_TAC/SIMP_TAC were also using METIS_TAC internally?

Thank you!

Regards,
Jiaqi



------------------------------------------------------------------------------
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 <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Jiaqi Tan | 8 Sep 08:20 2014
Picon

Problem trying to prove "A ==> A": Error from CHOOSE

Hi,

I have the following goal (using the theorems in examples/machine-code) in HOL4 which I am trying to prove:

val mw2 =
   ([([``SEP_IMP (aPC offset'' * r) (aPC offset'' * s')``,
       ``(s = aPC offset'' * s') ∧ SEP_IMP (aPC offset'' * r) s ⇒
  SPEC2 x (aPC offset' * q) c2 (aPC offset'' * s')``,
       ``(q' = aPC offset' * q) ∧ SEP_IMP (aPC offset' * q) q' ⇒
  SPEC2 x (aPC offset * p) c1 (aPC offset' * q)``,
       ``SEP_IMP (aPC offset'' * r) s``,
       ``s = aPC offset'' * s'``,
       ``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * r)``,
       ``q' = aPC offset' * q``],
      ``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
  SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')``)],
    fn): goal list * validation 

The goal is "SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
  SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')", which appears to be true (by one of the conjuncts in boolTheory.IMP_CLAUSES), but I am unable to prove it.

When I run "METIS_TAC []" on this goal interactively (by typing it in) from the HOL shell, I get "[.....] |- SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒ SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')", and when I run "METIS_TAC []" by pasting it into the shell (as the last tactic in my list of THEN'ed tactics), I get the error:
"Exception-
   HOL_ERR
  {message = "", origin_function = "CHOOSE", origin_structure = "Thm"} raised
"

Two of my tactics before reaching the above state are:

(Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset' * q) s ==> eee` 
 ((Q.X_CHOOSE_THEN `q` (Q.X_CHOOSE_TAC `offset'`)) o (Q.SPECL [`q'`])))

and

(Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset'' * r) s ==> eee` ((Q.X_CHOOSE_THEN `s'` (Q.X_CHOOSE_TAC `offset''`)) o (Q.SPECL [`s`])))

Could the Q.PAT_ASSUM (or X_CHOOSE_TAC) be causing problems? When I call Q.PAT_ASSUM and I use X_CHOOSE_TAC to instantiate existentially quantified variables with some variable, does that add extra assumptions to the theorem being selected from the assumptions before adding it to the goals? 

Thank you!

Regards,
Jiaqi



------------------------------------------------------------------------------
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 <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Klaus Havelund | 30 Aug 16:23 2014
Picon
Picon

[fm-announcements] Second call for papers: NASA Formal Methods - NFM 2015


CALL FOR PAPERS

The 7th NASA Formal Methods Symposium

http://www.NASAFormalMethods.org/nfm2015

27 – 29 April 2015
Pasadena, California, USA

THEME

The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, 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 mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.

TOPICS

Topics of interest include, but are not limited to:

  • Model checking
  • Theorem proving
  • SAT and SMT solving
  • Symbolic execution
  • Static analysis
  • Runtime verification
  • Program refinement
  • Compositional verification
  • Modeling and specification formalisms
  • Model-based development
  • Model-based testing
  • Requirement engineering
  • Formal approaches to fault tolerance
  • Security and intrusion detection
  • Applications of formal methods to aerospace systems
  • Applications of formal methods to cyber-physical systems
  • Applications of formal methods to human-machine interaction analysis

IMPORTANT DATES

Paper Submission: 10 Nov 2014
Paper Notifications: 12 Jan 2015
Camera-ready Papers: 9 Feb 2015
Symposium: 27 – 29 April 2015

LOCATION AND COST

The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.

SUBMISSION DETAILS

There are two categories of submissions:

  1. Regular papers describing fully developed work and complete results (15 pages)
  2. Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results (6 pages)

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer’s Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.

PC CHAIRS

Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Rajeev Joshi, NASA Jet Propulsion Laboratory

PROGRAMME COMMITTEE

Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Susanne Graf, VERIMAG, France
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Yvonne Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK

STEERING COMMITTEE

Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Yvonne Rozier, NASA Ames Research Center

---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 
------------------------------------------------------------------------------
Slashdot TV.  
Video for Nerds.  Stuff that matters.
http://tv.slashdot.org/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Ramana Kumar | 21 Aug 19:52 2014
Picon
Picon

SaveState

Hi all,

Yong Kiam showed me something very useful today, so I'd like to share it with you all. If you're using HOL with Poly/ML, then there are functions PolyML.SaveState.saveState and PolyML.SaveState.loadState, both of type string -> unit, which save the state of the REPL in a file (the string is the filename). This can be used in the middle of an interactive proof, in the middle of a long script file, to avoid the need to rebuild if the session is exited (accidentally or not).

Of course this doesn't help if there are logical reasons why things need to be rebuilt, but as long as those can be ignored...

Cheers,
Ramana
------------------------------------------------------------------------------
Slashdot TV.  
Video for Nerds.  Stuff that matters.
http://tv.slashdot.org/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Gwen.Salaun | 18 Aug 17:40 2014
Picon
Picon

Postdoc Position on Verification of Asynchronously Communicating Systems, Inria/LIG, Grenoble, France

The Convecs team (Inria Grenoble Rhône-Alpes research center / LIG
laboratory) recruits a postdoc. More information at:

http://convecs.inria.fr/jobs/2014b.html

Applications should be addressed directly to Gwen Salaün, preferably
by e-mail. Applications received after October 10th, 2014 might not be
considered if a candidate has been selected already. 

------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Kristin Yvonne Rozier | 16 Aug 07:23 2014
Picon

[fm-announcements] Call for Highlights: Aerospace America Intelligent Systems Year In Review

All,

Please consider submitting a highlight about your work! It is only 150 
words and it would really help to call attention to the important role 
of formal methods in the future of aerospace!

Cheers,
Kristin

	***********************************************
                       Call for Highlights

             Intelligent Systems 2014 Year In Review
                   Aerospace America magazine

                   Due date: August 25, 2014 (firm)
	***********************************************

This is a call for submissions for the "Year In Review" December, 2014 
issue of Aerospace America magazine. We are looking for summaries of 
interesting aerospace applications of intelligent systems, of 
approximately 150 words in length, with an accompanying graphic if 
possible. Each highlight will be integrated within an overall narrative, 
so key organizations/affiliations should be identified within the text 
to enable proper credit to be given; including a URL for further 
information on your work is required. The AIAA Intelligent Systems 
Technical Committee will select, from among all submissions received, 
six that will be highlighted in the year-end issue of Aerospace America 
magazine.

*********************************************************************
SUBMISSION:
----------
Deadline: Monday, August 25, 2014 (firm)
Submit through EasyChair: https://easychair.org/conferences/?conf=yir2014

*********************************************************************
HIGHLIGHT GUIDELINES:
---------------------
* 150 words
* describing an advancement in research relating to aerospace 
intelligent systems
* describing work that occurred or is projected to occur between January 
and December, 2014
* identifying key organizations/affiliations
* including a URL for further information and a word or phrase to 
hyperlink it to in the onine version of the article (Please list the 
word, phrase, or lab name to be hyperlinked after the highlight text, 
with the desired URL.)
* with an accompanying graphic, if possible: include after the highlight 
text a URL for a high-resolution JPG; include photo credit and caption

*********************************************************************
IMPORTANT DATES:
---------------------
* Submission Deadline: August 25, 2014 (firm)
* Notification of selection for Aerospace America article: September 1, 2014
* Proofs go out for author approval of AIAA ISTC newsletter: October 1, 2014
* Aerospace America article is published: December 1, 2014
* AIAA ISTC highlight newsletter is published: December 1, 2014

*********************************************************************
ARTICLE INFORMATION:
--------------------
This article will cover the most important developments this year in 
aerospace intelligent systems. Breakthroughs, setbacks, and industry 
trends that have occurred during the past year, the reasons they are 
important, and their impact on the aerospace community are also relevant.

More information on what types of aerospace systems qualify as 
intelligent is available here: 
https://info.aiaa.org/tac/isg/ISTC/Web%20Pages/What%20Is%20An%20Intelligent%20System.aspx.

Aerospace America reaches 40,000 people in a broad cross section of 
disciplines. highlights should be written so that all of them are able 
to understand the content, without acronyms if possible.

*********************************************************************
BACKGROUND:
-----------
The AIAA Intelligent Systems Technical Committee (ISTC) is concerned 
with the application of Intelligent System (IS) technologies and methods 
to aerospace systems, the verification and validation of these systems, 
and the education of the AIAA membership in the use of IS technologies 
in aerospace and other technical disciplines. See the Intelligent 
Systems Technical Committee website for more information on our 
technology focus: https://info.aiaa.org/tac/ISG/ISTC/default.aspx.

Previous years' print articles are available at 
https://ti.arc.nasa.gov/dev/profile/kyrozier/publications/#MagazineArticles. 

This year there will be two versions: a paper article with authors' 
designated hyperlink text bolded and an online article with the provided 
URL linked. Also, with author permission, all submitted highlights (not 
just the six selected for the article) will be included on the AIAA ISTC 
website and newsletter. Requests for permission and approval of 
camera-ready versions will go out on October 1, 2014.

-- 
  ____________________________________________________________
                                     __
            /\                       \ \_____
           /  \                   ###[==_____>
          /    \                     /_/      __
         /  __  \                             \ \_____
         | (  ) |                          ###[==_____>
        /| /\/\ |\                            /_/
       / | |  | | \
      /  |=|==|=|  \       Kristin Yvonne Rozier, Ph.D.
    /    | |  | |    \       Research Computer Scientist
   / USA | ~||~ |NASA \    NASA Ames Research Center
  |______|  ~~  |______|     Phone: (650) 604-3197
         (__||__)            Fax:   (650) 604-3594
         /_\  /_\
         !!!  !!!          http://ti.arc.nasa.gov/profile/kyrozier/

Any opinions expressed in this email are my own.
---
To opt-out from this mailing list, send an email to

fm-announcements-request <at> lists.nasa.gov

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> lists.nasa.gov 

------------------------------------------------------------------------------

Gmane