Limit search to available items
Book Cover
E-book
Author NFM 2012 (2012 : Norfolk, Va.)

Title NASA formal methods : 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings / Alwyn E. Goodloe, Suzette Person (eds.)
Published Berlin ; New York : Springer, ©2012

Copies

Description 1 online resource (xii, 466 pages)
Series Lecture notes in computer science, 0302-9743 ; 7226
LNCS sublibrary. SL 2, Programming and software engineering
Lecture notes in computer science ; 7226.
LNCS sublibrary. SL 2, Programming and software engineering.
Contents 880-01 SMT-Based Model Checking / Cesare Tinelli -- Verified Software Toolchain / Andrew W. Appel -- Formal Verification by Abstract Interpretation / Patrick Cousot -- Quantitative Timed Analysis of Interactive Markov Chains / Dennis Guck, Tingting Han, Joost-Pieter Katoen and Martin R. Neuhäußer -- Lessons Learnt from the Adoption of Formal Model-Based Development / Alessio Ferrari, Alessandro Fantechi and Stefania Gnesi -- Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines / Karolina Zurowska and Juergen Dingel -- Inferring Definite Counterexamples through Under-Approximation / Jörg Brauer and Axel Simon -- Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging / Ross Gore and Paul F. Reynolds -- Rigorous Polynomial Approximation Using Taylor Models in Coq / Nicolas Brisebarre, Mioara Joldeş, Érik Martin-Dorel, Micaela Mayero and Jean-Michel Muller, et al. -- Enhancing the Inverse Method with State Merging / Étienne André, Laurent Fribourg and Romain Soulat -- Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages / Alexander Herz and Kalmer Apinis -- Testing Static Analyzers with Randomly Generated Programs / Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto and John Regehr, et al. -- Compositional Verification of Architectural Models / Darren Cofer, Andrew Gacek, Steven Miller, Michael W. Whalen and Brian LaValley, et al. -- A Safety Case Pattern for Model-Based Development Approach / Anaheed Ayoub, BaekGyu Kim, Insup Lee and Oleg Sokolsky
880-01/(3/r Using PVS to Investigate Incidents through the Lens of Distributed Cognition / Paolo Masci, Huayi Huang, Paul Curzon and Michael D. Harrison -- Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms / Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi and Silvio Ranise -- Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems / Jason Belt, Robby, Patrice Chalin, John Hatcliff and Xianghua Deng -- Generating Verifiable Java Code from Verified PVS Specifications / Leonard Lensink, Sjaak Smetsers and Marko van Eekelen -- Belief Bisimulation for Hidden Markov Models / Logical Characterisation and Decision Algorithm / David N. Jansen, Flemming Nielson and Lijun Zhang -- Abstract Model Repair / George Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka and Panagiotis Katsaros -- CLSE: Closed-Loop Symbolic Execution / Rupak Majumdar, Indranil Saha, K.C. Shashidhar and Zilong Wang -- On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols / Michael Backes, Alex Busenius and Cătălin Hri€ثcu -- Incremental Verification with Mode Variable Invariants in State Machines / Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli and Mike Whalen -- A Semantic Analysis of Wireless Network Security Protocols / Damiano Macedonio and Massimo Merro -- Runtime Verification with Predictive Semantics / Xian Zhang, Martin Leucker and Wei Dong -- A Case Study in Verification of Embedded Network Software / Kalyan C. Regula, Hampton Smith, Heather Harton Keown, Jason O. Hallstrom and Nigamanth Sridhar, et al. -- Checking and Distributing Statistical Model Checking / Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay and Marius Mikučionis, et al
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL / Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche and Eric Feron, et al. -- Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements / (Preliminary Results) / Wenbin Li, Jane Huffman Hayes and Mirosław Truszczyński -- Some Steps into Verification of Exact Real Arithmetic / Norbert Th. Müller and Christian Uhrhan -- Runtime Verification Meets Android Security / Andreas Bauer, Jan-Christoph Küster and Gil Vegliach -- Specification in PDL with Recursion / Xinxin Liu and Bingtian Xue -- Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study / Aditi Tagore, Diego Zaccai and Bruce W. Weide -- Sound Formal Verification of Linux's USB BP Keyboard Driver / Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs and Frank Piessens -- Learning Markov Models for Stationary System Behaviors / Yingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen and Kim Guldstrand Larsen, et al. -- The Use of Rippling to Automate Event-B Invariant Preservation Proofs / Yuhui Lin, Alan Bundy and Gudmund Grov -- Thread-Modular Model Checking with Iterative Refinement / Wenrui Meng, Fei He, Bow-Yaw Wang and Qiang Liu -- Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs / Jiři Barnat, Luboš Brim and Petr Ročkai -- Integrating Statechart Components in Polyglot / Daniel Balasubramanian, Corina S. Păsăreanu, Jason Biatek, Thomas Pressburger and Gabor Karsai, et al
Using PVS to Investigate Incidents through the Lens of Distributed Cognition / Paolo Masci, Huayi Huang, Paul Curzon and Michael D. Harrison -- Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms / Roberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi and Silvio Ranise -- Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems / Jason Belt, Robby, Patrice Chalin, John Hatcliff and Xianghua Deng -- Generating Verifiable Java Code from Verified PVS Specifications / Leonard Lensink, Sjaak Smetsers and Marko van Eekelen -- Belief Bisimulation for Hidden Markov Models / Logical Characterisation and Decision Algorithm / David N. Jansen, Flemming Nielson and Lijun Zhang -- Abstract Model Repair / George Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka and Panagiotis Katsaros -- CLSE: Closed-Loop Symbolic Execution / Rupak Majumdar, Indranil Saha, K.C. Shashidhar and Zilong Wang -- On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols / Michael Backes, Alex Busenius and Cătălin Hrițcu -- Incremental Verification with Mode Variable Invariants in State Machines / Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli and Mike Whalen -- A Semantic Analysis of Wireless Network Security Protocols / Damiano Macedonio and Massimo Merro -- Runtime Verification with Predictive Semantics / Xian Zhang, Martin Leucker and Wei Dong -- A Case Study in Verification of Embedded Network Software / Kalyan C. Regula, Hampton Smith, Heather Harton Keown, Jason O. Hallstrom and Nigamanth Sridhar, et al. -- Checking and Distributing Statistical Model Checking / Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay and Marius Mikučionis, et al
Summary This book constitutes the refereed proceedings of the Fourth International Symposium on NASA Formal Methods, NFM 2012, held in Norfolk, VA, USA, in April 2012. The 36 revised regular papers presented together with 10 short papers, 3 invited talks were carefully reviewed and selected from 93 submissions. The topics are organized in topical sections on theorem proving, symbolic execution, model-based engineering, real-time and stochastic systems, model checking, abstraction and abstraction refinement, compositional verification techniques, static and dynamic analysis techniques, fault protection, cyber security, specification formalisms, requirements analysis and applications of formal techniques
Analysis Computer science
Software engineering
Operating systems (Computers)
Logic design
Programming Languages, Compilers, Interpreters
Operating Systems
Logics and Meanings of Programs
Software Engineering/Programming and Operating Systems
Programming Techniques
Bibliography Includes bibliographical references and author index
In Springer eBooks
Subject Formal methods (Computer science) -- Congresses
Fault-tolerant computing -- Congresses
Computer software -- Verification -- Congresses
System analysis -- Congresses
Operating systems (Computers)
Electronic Data Processing
computer science.
data processing.
operating systems.
Informatique.
Computer software -- Verification
Fault-tolerant computing
Formal methods (Computer science)
System analysis
Genre/Form proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
Form Electronic book
Author Goodloe, Alwyn E
Person, Suzette
ISBN 9783642288913
364228891X
Other Titles NFM 2012