[Om-announce] [fm-announcements] NFM 2013 Call for participation

[Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGT Inc.)]]

==================================================================
           5th NASA Formal Methods Symposium (NFM) 2013

                     NASA Ames Research Center
                      Moffett Field, CA, USA
                          May 14-16, 2013 
              http://ti.arc.nasa.gov/events/nfm-2013/
==================================================================

Theme of the Conference: 

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, for
example, such systems include autonomous robots, separation assurance
algorithms for aircraft, Next Generation Air Transportation (NextGen),
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.

Topics of Interest: 

    * Formal verification, including theorem proving, model checking,
      and static analysis
    * Techniques and algorithms for scaling formal methods, including
      but not restricted to abstraction and symbolic methods,
      compositional techniques, as well as parallel and distributed
      techniques
    * Use of formal methods in automated software engineering and
      testing Model-based development
    * Formal program synthesis
    * Runtime monitoring and verification
    * Formal approaches to fault tolerance
    * Formal analysis of cyber-physical systems, including hybrid and
      embedded systems
    * Formal methods in systems engineering, modeling, requirements
      and specifications
    * Applications of formal methods to aerospace systems
    * Use of formal methods in safety cases
    * Use of formal methods in human-machine interaction analysis
    * Formal methods for multi-core, GPU-based implementations
    * Application of formal methods to emerging technologies, e.g.,
      mobile applications, autonomous systems, web-based application

==================================================================
			 Chairs
==================================================================

Guillaume Brat, CMU/NASA Ames Research Center, USA
Neha Rungta, SGT Inc/NASA Ames Research Center, USA
Arnaud Venet, CMU/NASA Ames Research Center, USA

==================================================================
			Registration
==================================================================

NFM 2013 will be held at NASA Ames Research Center, Moffett Field, CA
on May 14 to 16, 2013. There will not be a registration fee charged to
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. Note that the 
registration site will close on April 16th, 2013. This is a firm
deadline. There will be no on-site registrations as a badge is
required to access the conference site. 

http://ti.arc.nasa.gov/events/nfm-2013/registration/

==================================================================
			Invited Speakers
==================================================================

Alex Aiken, Stanford University, USA
"Using Learning Techniques in Invariant Inference"

John Rushby, SRI International, USA
"The Challenge of High-Assurance Software"

Ken McMillan, Microsoft Research, USA
"The Importance of Generalization in Automated Proof"

Rajeev Joshi, Jet Propulsion Laboratory, USA
 "Managing data for Curiosity, Fun and Profit"

Michael DeWalt, Federal Aviation Administration, USA
"Certification challenges when using formal methods, including
 needs and issues"


==================================================================
			Accepted Papers
==================================================================

Regular:

"Freshness and Reactivity Analysis in Globally Asynchronous Locally
Time-Triggered Systems" Frédéric Boniol, Michaël Lauer, Claire Pagetti
and Jérôme Ermont.

"A Probabilistic Quantitative Analysis of
Probabilistic-Write/Copy-Select" Christel Baier, Benjamin Engel,
Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp.


"Formal Stability Analysis of Optical Resonators" Umair Siddique,
Vincent Aravantinos and Sofiene Tahar.

"Enclosing Temporal Evolution of Dynamical Systems Using Numerical
Methods" Olivier Bouissou, Alexandre Chapoutot and Adel Djoudi.


"Automated Verification of Chapel Programs Using Model Checking and
Symbolic Execution" Timothy K. Zirkel, Stephen F. Siegel and Timothy
McClory.

"Formal Analysis of GPU Programs with Atomics via Conflict-Directed
Delay-Bounding" Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li and
Zvonimir Rakamaric.

"Statistical Model Checking of Wireless Mesh Routing Protocols" Peter
Höfner Annabelle McIver.

"From UML to Process Algebra and Back: An Automated Approach to
Model-Checking Software Design Artifacts of Concurrent Systems"
Daniela Remenska, Henri Bal, Jeff Templon, Kees Verstoep, Tim
Willemse, Philip Homburg and Adrià Casajús.

"Evaluating Human-human Communication Protocols with Miscommunication
Generation and Model Checking" Matthew Bolton and Ellen Bass.

"Incremental Invariant Generation using Logic-based Automatic Abstract
Transformers" Pierre-Loic Garoche, Temesghen Kahsai and Cesare
Tinelli.

"Improved State Space Reductions for LTL Model Checking of C & C++
Programs" Petr Rockai, Jiri Barnat and Lubos Brim.

"On-the-fly Confluence Detection for Statistical Model Checking" Arnd
Hartmanns and Mark Timmer.

"Optmizing Control Strategy using Statistical Model Checking"
Alexandre David, Kim Guldstrand Larsen, Marius Mikučionis, Axel Legay
and Dehui Du.

"Numerical Abstract Domain using Support Functions" Yassamine Seladji
and Olivier Bouissou.

"Widening as Abstract Domain" Bogdan Mihaila, Alexander Sepp and Axel
Simon.

"Using Model-Checking to Reveal a Vulnerability of Tamper-Evident
Pairing" Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak
Smeters and Marko Van Eekelen.

"Regular Model Checking Using Solver Technologies and Automata
Learning" Daniel Neider and Nils Jansen.

"Automatically Detecting Inconsistencies in Program Specifications"
Aditi Tagore and Bruce Weide.

"Inferring Automata with State-local Alphabet Abstractions" Malte
Isberner, Falk Howar and Bernhard Steffen.

"Verifying a Privacy CA Remote Attestation Protocol" Brigid Halling
and Perry Alexander.

"Improved On-The-Fly Livelock Detection: Combining Partial Order
Reduction and Parallelism for DFS-FIFO" Alfons Laarman and David
Farago.

"LiquidPi: Inferrable Dependent Session Types" Dennis Griffith and
Elsa Gunter.

"SMT-based analysis of biological computation" Boyan Yordanov,
Christoph M. Wintersteiger, Youssef Hamadi and Hillel Kugler.

"Formalization of Infinite Dimension Linear Spaces with Application to
Quantum Theory" Mohamed Yousri Mahmoud, Vincent Aravantinos and
Sofienne Tahar.

"BLESS: Formal Specification and Verification of Behaviors for
Embedded Systems with Software" Brian Larson, Patrice Chalin and John
Hatcliff.

"Towards Complete Specifications with an Error Calculus" Quang Loc Le,
Asankhaya Sharma, Florin Craciun and Wei-Ngan Chin.

"Bounded Lazy Initialization" Jaco Geldenhuys, Nazareno Aguirre,
Marcelo Frias and Willem Visser.

Short:

"Formal Verification of a Parameterized Data Aggregation Protocol"
Sergio Feo-Arenis and Bernd Westphal.

"OnTrack: An Open Tooling Environment For Railway Verification"
Phillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach and
Steve Schneider.

"Verification of Floating Point Programs:From Real Numbers to Floating
Point Numbers" Alwyn Goodloe, Cesar Munoz, Florent Kirchner and Loic
Correnson.

"Extracting Hybrid Automata from Control Code" Steven Lyde and Matthew
Might.

"PyNuSMV: NuSMV as a Python Library" Simon Busard and Charles Pecheur.

"jUnitRV - Adding Runtime Verification to jUnit" Normann Decker,
Martin Leucker and Daniel Thoma.

"Using Language Engineering to Lift Languages and Analyses at the
Domain Level" Daniel Ratiu, Markus Voleter, Bernhard Schaetz and Bernd
Kolb.

"On Designing an ACL2 C Integer Type Safety Checking Tool" Kevin
Krause and Jim Alves-Foss.

"Hierarchical Safety Cases" Ewen Denney, Ganesh Pai and Iain
Whiteside.



---
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