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.
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.
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
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-requ...@lists.nasa.gov
with the word 'unsubscribe' as subject or in the body. You can also make the
request by contacting
fm-announcements-ow...@lists.nasa.gov
_______________________________________________
Om mailing list
Om@openmath.org
http://openmath.org/mailman/listinfo/om
