[FM-India] NFM 2013 Call for participation

[Madhavan Mukund]

 From: "Rungta, Neha S. (ARC-TI)[Stinger Ghaffarian Technologies Inc. (SGT
  Inc.)]" <neha.s.rungta at nasa.gov>
 To: "fm-announcements at lists.nasa.gov" <fm-announcements at lists.nasa.gov>
 Date: Thu, 21 Mar 2013 23:40:24 -0500
 Subject: [fm-announcements] NFM 2013 Call for participation
 
 ==================================================================
            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.