[ecoop-info] [fm-announcements] NFM 2014: Second Call for Participation

[Kristin Yvonne Rozier]

Please find the NFM 2014 Call for Participation below. With no 
registration fee and very reasonable costs for accommodations this 
conference is an excellent value to attend even without presenting a 
paper. It is also a great place to bring students for exposure to 
real-world applications!


**************************************************
      The Sixth NASA Formal Methods Symposium

         http://www.NASAFormalMethods.org/

               29 April - 1 May 2014
   NASA Johnson Space Center, Houston, Texas, USA
**************************************************

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

Registration URL: http://www.nasaformalmethods.org/?page_id=160

We strongly encourage participants to register early and reserve 
accomodations. A block of hotel rooms are available at $98.00 per night 
for reservations made before April 7. The registration deadline is April 22.


Keynote Speakers:
-----------------
* "NASA Future Challenges in Formal Methods" by Bill McAllister, Chief, 
Safety and Mission Assurance, International Space Station Safety Panels, 
Avionics and Software Branch
* "Theorem Proving and the Real Numbers: Overview and Challenges" by 
Larry Paulson, University of Cambridge, UK
* "Compositional Temporal Synthesis" by Moshe Y. Vardi, Rice University, USA


Panel: "Future Directions of Specifications for Formal Methods"
---------------------------------------------------------------
Panelists:
     Matt Dwyer, University of Nebraska, USA
     Hadas Kress-Gazit, Cornell University, USA
     Moshe Y. Vardi, Rice University, USA
Panel Description: Specifications are required for all applications of 
formal methods yet extracting specifications for real-life safety 
critical systems often proves to be a huge bottleneck or even an 
insurmountable hurdle to the application of formal methods in practice. 
This is the state for safety-critical systems today and as these systems 
grow more complex, more pervasive, and more powerful in the future, 
there is not a clear path even for maintaining the bleak status quo. 
Therefore, we propose highlighting this issue in the home of an 
important critical system, the Mission Control Center of NASA's most 
famous critical systems, and asking our panelists where we can go from here.


Accepted Papers:
----------------
*   Darren Cofer and Steven Miller
     "DO-333 Certification Case Studies"
*   André De Matos Pedro, David Pereira, Luís Miguel Pinho and Jorge 
Sousa Pinto
     "A Compositional Monitoring Framework for Hard Real-Time Systems"
*   Pedro Antonino, Marcel Vinicius Medeiros Oliveira, Augusto Sampaio, 
Klaus Kristensen and Jeremy W. Bryans
     "Leadership Election: an Industrial SoS Application of 
Compositional Deadlock Verification"
*   Lars Noschinski, Christine Rizkallah and Kurt Mehlhorn
     "Verification of Certifying Computations through AutoCorres and Simpl"
*   Robert M. Hierons and Uraz Cengiz Turker
     "Distinguishing Sequences for Partially Specified FSMs"
*   Seppo Horsmanheimo, Maryam Kamali, Mikko Kolehmainen, Mats Neovius, 
  Luigia Petre, Mauno Rönkkö and Petter Sandvik
     "On Proving Recoverability of Smart Electrical Grids"
*   Dustin Hoffman, Aditi Tagore, Diego Zaccai and Bruce Weide
     "Providing Early Warnings of Specification Problems"
*   Björn Bartels
     "Mechanized, Compositional Verification of Low-Level Code"
*   Fabian Immler
     "Formally Verified Enclosures of Solutions of Ordinary Differential 
Equations"
*   Mohamed Yousri and Sofiene Tahar
     "On the Quantum Formalization of Coherent Light in HOL"
*   Hernán Vanzetto and Stephan Merz
     "Type Inference with Refinements Types for TLA+"
*   Matthew Danish and Hongwei Xi
     "Using lightweight theorem proving in an asynchronous systems context"
*   Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, 
Shmuel Tyszberowicz and Mana Taghdiri
     "JKelloy: A Proof Assistant for Relational Specifications of Java 
Programs"
*   Andrew Sogokon, Paul Jackson, Lawrence Paulson and James Bridge
     "Verifying Hybrid Systems Involving Transcendental Functions"
*   William Denman
     Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction 
and Automated Theorem Proving"
*   Paolo Masci, Yi Zhang, Patrick Oladimeji, Enrico D’Urso, Paul Jones, 
Harold Thimbleby, Paul Curzon and Cinzia Bernardeschi
     "Combining PVSio with Stateflow"
*   Loïc Correnson
     "Qed: Computing what Remains to be Proved"
*   Ethel Bardsley and Alastair Donaldson
     "Warps and Atomics: Beyond Barrier Synchronization in the 
Verification of GPU Kernels"
*   Temesghen Kahsai, Pierre-Loic Garoche, Falk Howar and Xavier Thirioux
     "Testing-based compiler validation for synchronous languages"
*   Johann Schumann and Stefan-Alexander Schneider
     "Automated Testcase Generation for Numerical Support Functions in 
Embedded Systems"
*   Luc Engelen and Anton Wijs
     "REFINER: Towards Formal Verification of Model Transformations"
*   Franco Mazzanti, Giorgio Oronzo Spagnolo and Alessio Ferrari
     "Design of a Deadlock-free Train Scheduler: a Model Checking Approach"
*   Adrià Gascón and Ashish Tiwari
     "A Synthesized Algorithm for Interactive Consistency"
*   Christel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein and 
Sascha Klueppelholz
     "Energy-Utility Quantiles"
*   Grigory Fedyukovich, Arie Gurfinkel and Natasha Sharygina
     "Incremental Verification of Compiler Optimizations"
*   Peter Gjøl Jensen, Kim Guldstrand Larsen, Jiri Srba, Mathias Grund 
Sørensen and Jakob Haahr Taankvist
     "Memory Efficient Data Structures for Explicit Verification of 
Timed Systems"
*   Stephan Arlt, Cindy Rubio-González, Philipp Ruemmer, Martin Schäf 
and Natarajan Shankar
     "The Gradual Verifier"
*   Bogdan Mihaila and Axel Simon.
     "Synthesizing Predicates from Abstract Domain Losses"
*   Nuno Carvalho, Cristiano Da Silva Sousa, Jorge Sousa Pinto and Aaron 
Tomb
     "Formal Verification of kLIBC with the WP Frama-C plug-in"

-- 
  ____________________________________________________________
                                     __
            /\                       \ \_____
           /  \                   ###[==_____>
          /    \                     /_/      __
         /  __  \                             \ \_____
         | (  ) |                          ###[==_____>
        /| /\/\ |\                            /_/
       / | |  | | \
      /  |=|==|=|  \       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