<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:x="urn:schemas-microsoft-com:office:excel" xmlns:p="urn:schemas-microsoft-com:office:powerpoint" xmlns:a="urn:schemas-microsoft-com:office:access" xmlns:dt="uuid:C2F41010-65B3-11d1-A29F-00AA00C14882" xmlns:s="uuid:BDC6E3F0-6DA3-11d1-A2A3-00AA00C14882" xmlns:rs="urn:schemas-microsoft-com:rowset" xmlns:z="#RowsetSchema" xmlns:b="urn:schemas-microsoft-com:office:publisher" xmlns:ss="urn:schemas-microsoft-com:office:spreadsheet" xmlns:c="urn:schemas-microsoft-com:office:component:spreadsheet" xmlns:odc="urn:schemas-microsoft-com:office:odc" xmlns:oa="urn:schemas-microsoft-com:office:activation" xmlns:html="http://www.w3.org/TR/REC-html40" xmlns:q="http://schemas.xmlsoap.org/soap/envelope/" xmlns:rtc="http://microsoft.com/officenet/conferencing" xmlns:D="DAV:" xmlns:Repl="http://schemas.microsoft.com/repl/" xmlns:mt="http://schemas.microsoft.com/sharepoint/soap/meetings/" xmlns:x2="http://schemas.microsoft.com/office/excel/2003/xml" xmlns:ppda="http://www.passport.com/NameSpace.xsd" xmlns:ois="http://schemas.microsoft.com/sharepoint/soap/ois/" xmlns:dir="http://schemas.microsoft.com/sharepoint/soap/directory/" xmlns:ds="http://www.w3.org/2000/09/xmldsig#" xmlns:dsp="http://schemas.microsoft.com/sharepoint/dsp" xmlns:udc="http://schemas.microsoft.com/data/udc" xmlns:xsd="http://www.w3.org/2001/XMLSchema" xmlns:sub="http://schemas.microsoft.com/sharepoint/soap/2002/1/alerts/" xmlns:ec="http://www.w3.org/2001/04/xmlenc#" xmlns:sp="http://schemas.microsoft.com/sharepoint/" xmlns:sps="http://schemas.microsoft.com/sharepoint/soap/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:udcs="http://schemas.microsoft.com/data/udc/soap" xmlns:udcxf="http://schemas.microsoft.com/data/udc/xmlfile" xmlns:udcp2p="http://schemas.microsoft.com/data/udc/parttopart" xmlns:wf="http://schemas.microsoft.com/sharepoint/soap/workflow/" xmlns:dsss="http://schemas.microsoft.com/office/2006/digsig-setup" xmlns:dssi="http://schemas.microsoft.com/office/2006/digsig" xmlns:mdssi="http://schemas.openxmlformats.org/package/2006/digital-signature" xmlns:mver="http://schemas.openxmlformats.org/markup-compatibility/2006" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns:mrels="http://schemas.openxmlformats.org/package/2006/relationships" xmlns:spwp="http://microsoft.com/sharepoint/webpartpages" xmlns:ex12t="http://schemas.microsoft.com/exchange/services/2006/types" xmlns:ex12m="http://schemas.microsoft.com/exchange/services/2006/messages" xmlns:pptsl="http://schemas.microsoft.com/sharepoint/soap/SlideLibrary/" xmlns:spsl="http://microsoft.com/webservices/SharePointPortalServer/PublishedLinksService" xmlns:Z="urn:schemas-microsoft-com:" xmlns:st="" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=us-ascii"><meta name=Generator content="Microsoft Word 12 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-US link=blue vlink=purple><div class=WordSection1><p class=MsoNormal>SECOND CALL FOR PAPERS<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>NFM 2012<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Fourth NASA Formal Methods Symposium<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Norfolk, Virginia, USA<o:p></o:p></p><p class=MsoNormal>April 3 - 5, 2012<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>http://shemesh.larc.nasa.gov/nfm2012/<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>nasa-nfm2012@mail.nasa.gov<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Theme of Conference:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The NASA Formal Methods Symposium is a forum for theoreticians and<o:p></o:p></p><p class=MsoNormal>practitioners from academia, industry, and government, with the goals of<o:p></o:p></p><p class=MsoNormal>identifying challenges and providing solutions to achieving assurance<o:p></o:p></p><p class=MsoNormal>in mission- and safety-critical systems. Within NASA, for example, such systems <o:p></o:p></p><p class=MsoNormal>include autonomous robots, separation assurance algorithms for aircraft,<o:p></o:p></p><p class=MsoNormal>Next Generation Air Transportation (NextGen), and autonomous rendezvous and <o:p></o:p></p><p class=MsoNormal>docking for spacecraft. Moreover, emerging paradigms such as code generation<o:p></o:p></p><p class=MsoNormal>and safety cases are bringing with them new challenges and opportunities.<o:p></o:p></p><p class=MsoNormal>The focus of the symposium will be on formal techniques, their theory,<o:p></o:p></p><p class=MsoNormal>current capabilities, and limitations, as well as their application to <o:p></o:p></p><p class=MsoNormal>aerospace, robotics, and other safety-critical systems. <o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Topics of Interest:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>* Formal verification, including theorem proving, model checking,<o:p></o:p></p><p class=MsoNormal> and static analysis<o:p></o:p></p><p class=MsoNormal>* Automated test generation and testing techniques for safety-critical systems<o:p></o:p></p><p class=MsoNormal>* Model-based development<o:p></o:p></p><p class=MsoNormal>* Techniques and algorithms for scaling formal methods, such as abstraction<o:p></o:p></p><p class=MsoNormal> and symbolic methods, compositional techniques, as well as parallel and<o:p></o:p></p><p class=MsoNormal> distributed techniques<o:p></o:p></p><p class=MsoNormal>* Monitoring and runtime verification<o:p></o:p></p><p class=MsoNormal>* Code generation from formally verified models<o:p></o:p></p><p class=MsoNormal>* Significant applications of formal methods to aerospace systems<o:p></o:p></p><p class=MsoNormal>* Modeling and verification aspects of cyber-physical systems<o:p></o:p></p><p class=MsoNormal>* Safety cases<o:p></o:p></p><p class=MsoNormal>* Accident/safety analysis<o:p></o:p></p><p class=MsoNormal>* Formal approaches to fault tolerance<o:p></o:p></p><p class=MsoNormal>* Theoretical advances and empirical evaluations of formal methods<o:p></o:p></p><p class=MsoNormal>* Techniques for safety-critical systems, including hybrid and embedded systems<o:p></o:p></p><p class=MsoNormal>* Formal methods in systems engineering<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Invited Speakers:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>* Andrew Appel, Princeton University<o:p></o:p></p><p class=MsoNormal>* Patrick Cousot, Ecole Normale Superieure, Paris and New York University<o:p></o:p></p><p class=MsoNormal>* Cesare Tinelli, University of Iowa<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Submissions:<o:p></o:p></p><p class=MsoNormal>--------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>There are two categories of submissions:<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>* Regular papers describing fully developed work and complete<o:p></o:p></p><p class=MsoNormal> results (15 pages/30 minute talks)<o:p></o:p></p><p class=MsoNormal>* Short papers describing tools, experience reports, or descriptions <o:p></o:p></p><p class=MsoNormal> of work in progress or preliminary results (6 pages/15 minute talks)<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal> All papers should be in English and describe original work that has not <o:p></o:p></p><p class=MsoNormal> been published or submitted elsewhere. All submissions will be fully reviewed<o:p></o:p></p><p class=MsoNormal> by members of the program committee and the Symposium proceedings (including <o:p></o:p></p><p class=MsoNormal> regular papers and short papers) will appear as a volume in Lecture Notes<o:p></o:p></p><p class=MsoNormal> in Computer Science. Papers must use the LNCS style, and be in PDF format.<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal> Papers should be submitted through the following <o:p></o:p></p><p class=MsoNormal> link: http://www.easychair.org/conferences/?conf=nfm2012 <o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Program Chairs:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Alwyn Goodloe, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Suzette Person, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Program Committee:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Nikolaj Bjoerner, Microsoft Research, USA<o:p></o:p></p><p class=MsoNormal>Jonathan Bowen, London South Bank Univ, UK <o:p></o:p></p><p class=MsoNormal>Julia Braman, NASA Johnson Space Center, USA<o:p></o:p></p><p class=MsoNormal>Ricky Butler, NASA Langley Research Center, USA<o:p></o:p></p><p class=MsoNormal>Rance Cleaveland, Univ of Maryland, USA <o:p></o:p></p><p class=MsoNormal>Darren Cofer, Rockwell Collins, USA<o:p></o:p></p><p class=MsoNormal>Ewen Denney, NASA Ames Research Center, USA <o:p></o:p></p><p class=MsoNormal>Dino Distefano, Queen Mary Univ of London and Monoidics Ltd., UK<o:p></o:p></p><p class=MsoNormal>Jin Song Dong, Univ of Singapore, Singapore<o:p></o:p></p><p class=MsoNormal>Jean-Christophe Filliatre, CNRS, France <o:p></o:p></p><p class=MsoNormal>Dimitra Giannakopoulou, NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Eric Goubault, CEA LIST, France <o:p></o:p></p><p class=MsoNormal>George Hagen, NASA Langley Research Center, USA<o:p></o:p></p><p class=MsoNormal>John Hatcliff, Kansas State Univ, USA <o:p></o:p></p><p class=MsoNormal>Klaus Havelund, NASA/JPL, USA <o:p></o:p></p><p class=MsoNormal>Mats Heimdahl, Univ of Minnesota, USA<o:p></o:p></p><p class=MsoNormal>Gerard Holzmann, NASA/JPL, USA<o:p></o:p></p><p class=MsoNormal>Joe Hurd, Galois, USA <o:p></o:p></p><p class=MsoNormal>Bart Jacobs, Katholieke Univ Leuven, Belgium<o:p></o:p></p><p class=MsoNormal>Kenneth McMillan, Microsoft Research, USA<o:p></o:p></p><p class=MsoNormal>Eric Mercer, Brigham Young University, USA<o:p></o:p></p><p class=MsoNormal>Cesar Munoz, NASA Langley Research Center, USA<o:p></o:p></p><p class=MsoNormal>Anthony Narkawicz, NASA Langley Research Center, USA<o:p></o:p></p><p class=MsoNormal>Natasha Neogi, National Institute of Aerospace, USA<o:p></o:p></p><p class=MsoNormal>Corina Pasareanu, NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Charles Pecheur, Univ de Louvain, Belgium<o:p></o:p></p><p class=MsoNormal>Kristin Rozier, NASA Ames Research Center, USA<o:p></o:p></p><p class=MsoNormal>Natarajan Shankar, SRI, International, USA<o:p></o:p></p><p class=MsoNormal>Oleg Sokolsky, Univ of Pennsylvania, USA<o:p></o:p></p><p class=MsoNormal>Sofiene Tahar, Concordia Univ, Canada<o:p></o:p></p><p class=MsoNormal>Oksana Tkachuk, NASA Ames Research Center, USA <o:p></o:p></p><p class=MsoNormal>Willem Visser, Univ of Stellenbosch, South Africa<o:p></o:p></p><p class=MsoNormal>Mike Whalen, Univ of Minnesota, USA<o:p></o:p></p><p class=MsoNormal>Virginie Wiels, ONERA, France<o:p></o:p></p><p class=MsoNormal>Jim Woodcock, University of York, UK<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Steering Committee:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Ewen Denney, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>Ben Di Vito, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Dimitra Giannakopoulou, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>Klaus Havelund, NASA/Jet Propulsion Laboratory<o:p></o:p></p><p class=MsoNormal>Gerard Holzmann, NASA/Jet Propulsion Laboratory<o:p></o:p></p><p class=MsoNormal>Cesar Munoz, NASA Langley Research Center<o:p></o:p></p><p class=MsoNormal>Corina Pasareanu, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal>James Rash, NASA Goddard<o:p></o:p></p><p class=MsoNormal>Kristin Y. Rozier, NASA Ames Research Center<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Important Dates:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Submission: 11 December 2011<o:p></o:p></p><p class=MsoNormal>Notification: 21 January 2012<o:p></o:p></p><p class=MsoNormal>Final Version: 4 February 2012<o:p></o:p></p><p class=MsoNormal>Conference: 3 - 5 April 2012<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal>Location and Cost:<o:p></o:p></p><p class=MsoNormal>-------------------------------------------------------<o:p></o:p></p><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>The symposium will take place at the Norfolk Waterside Marriott in<o:p></o:p></p><p class=MsoNormal>Norfolk, Virginia, USA. April 3-5, 2012. There will not be a registration<o:p></o:p></p><p class=MsoNormal>fee charged to participants. All interested individuals, including non-US<o:p></o:p></p><p class=MsoNormal>citizens, are welcome to attend, to listen to the talks, and to participate<o:p></o:p></p><p class=MsoNormal>in discussions; however, all attendees must register.<o:p></o:p></p></div></body></html>