NASA formal methods : 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings / Guillaume Brat, Neha Rungta, Arnaud Venet (eds.)
This book constitutes the refereed proceedings of the 5th International Symposium on NASA Formal Methods, NFM 2013, held in Moffett Field, CA, USA, in May 2013. The 28 revised regular papers presented together with 9 short papers talks were carefully reviewed and selected from 99 submissions. The to...
Saved in:
| Online Access: |
Full Text (via Springer) |
|---|---|
| Corporate Author: | |
| Other Authors: | , , |
| Other title: | NFM 2013. |
| Format: | Conference Proceeding eBook |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
[2013]
|
| Series: | Lecture notes in computer science ;
7871. LNCS sublibrary. Programming and software engineering. |
| Subjects: |
MARC
| LEADER | 00000cam a2200000xi 4500 | ||
|---|---|---|---|
| 001 | b7398988 | ||
| 006 | m o d | ||
| 007 | cr ||||||||||| | ||
| 008 | 130521s2013 gw a ob 101 0 eng d | ||
| 005 | 20240418145209.5 | ||
| 019 | |a 844687412 | ||
| 020 | |a 9783642380884 |q (electronic bk.) | ||
| 020 | |a 3642380883 |q (electronic bk.) | ||
| 020 | |a 3642380875 |q (Print) | ||
| 020 | |a 9783642380877 |q (Print) | ||
| 020 | |z 9783642380877 | ||
| 024 | 7 | |a 10.1007/978-3-642-38088-4 | |
| 035 | |a (OCoLC)spr843880996 | ||
| 035 | |a (OCoLC)843880996 |z (OCoLC)844687412 | ||
| 037 | |a spr10.1007/978-3-642-38088-4 | ||
| 040 | |a GW5XE |b eng |e rda |e pn |c GW5XE |d YDXCP |d ZMC |d COO |d NLGGC |d OCLCQ |d NUI |d OHS |d OCLCF |d IAD |d VLB |d OCLCQ |d OCLCO |d OCLCQ |d OCLCO |d OCL |d OCLCO |d EBLCP |d DIBIB |d OCLCO |d YDX | ||
| 049 | |a GWRE | ||
| 050 | 4 | |a QA76.9.F67 |b N46 2013 | |
| 111 | 2 | |a NFM (Symposium) |n (5th : |d 2013 : |c Moffett Field, Calif.) |0 http://id.loc.gov/authorities/names/nb2013016516. | |
| 245 | 1 | 0 | |a NASA formal methods : |b 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings / |c Guillaume Brat, Neha Rungta, Arnaud Venet (eds.) |
| 246 | 3 | |a NFM 2013. | |
| 264 | 1 | |a Berlin ; |a New York : |b Springer, |c [2013] | |
| 264 | 4 | |c ©2013. | |
| 300 | |a 1 online resource (xxiv, 486 pages) : |b illustrations. | ||
| 336 | |a text |b txt |2 rdacontent. | ||
| 337 | |a computer |b c |2 rdamedia. | ||
| 338 | |a online resource |b cr |2 rdacarrier. | ||
| 490 | 1 | |a Lecture notes in computer science, |x 0302-9743 ; |v 7871. | |
| 490 | 1 | |a LNCS sublibrary. SL 2, Programming and software engineering. | |
| 505 | 0 | 0 | |g Session 1: |t Model Checking. |t Improved State Space Reductions for LTL Model Checking of C and C++ Programs / |r Petr Ročkai, Jiří Barnat, Luboš Brim -- |t Regular Model Checking Using Solver Technologies and Automata Learning / |r Daniel Neider, Nils Jansen -- |t Improved on-the-Fly Livelock Detection / |r Alfons Laarman, David Faragó |
| 505 | 8 | 0 | |g Session 2: |t Applications of Formal Methods. |t Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model Checking / |r Matthew L. Bolton, Ellen J. Bass -- |t Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing / |r Rody Kersten [and others] -- |t SMT-Based Analysis of Biological Computation / |r Boyan Yordanov [and others] |
| 505 | 8 | 0 | |g Session 3: |t Complex Systems. |t Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered Systems / |r Frédéric Boniol [and others] -- |t Enclosing Temporal Evolution of Dynamical Systems Using Numerical Methods / |r Olivier Bouissou, Alexandre Chapoutot, Adel Djoudi -- |t Inferring Automata with State-Local Alphabet Abstractions / |r Malte Isberner, Falk Howar, Bernhard Steffen. |
| 505 | 8 | 0 | |g Session 4: |t Static Analysis. |t Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers / |r Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli -- |t Numerical Abstract Domain Using Support Functions / |r Yassamine Seladji, Olivier Bouissou -- |t Widening as Abstract Domain / |r Bogdan Mihaila, Alexander Sepp, Axel Simon -- |t LiquidPi: Inferrable Dependent Session Types / |r Dennis Griffith, Elsa L. Gunter. |
| 505 | 8 | 0 | |g Session 5: |t Symbolic Execution. |t Automated Verification of Chapel Programs Using Model Checking and Symbolic Execution / |r Timothy K. Zirkel, Stephen F. Siegel, Timothy McClory -- |t Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding / |r Wei-Fan Chiang [and others] -- |t Bounded Lazy Initialization / |r Jaco Geldenhuys [and others] |
| 505 | 8 | 0 | |g Session 6: |t Requirements and Specifications. |t From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems / |r Daniela Remenska [and others] -- |t Automatically Detecting Inconsistencies in Program Specifications / |r Aditi Tagore, Bruce W. Weide -- |t BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with Software / |r Brian R. Larson, Patrice Chalin, John Hatcliff -- |t Towards Complete Specifications with an Error Calculus / |r Quang Loc Le [and others] |
| 505 | 8 | 0 | |g Session 7: |t Probabilistic and Statistical Analysis. |t A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select / |r Christel Baier [and others] -- |t Statistical Model Checking of Wireless Mesh Routing Protocols / |r Peter Höfner, Annabelle McIver -- |t On-the-Fly Confluence Detection for Statistical Model Checking / |r Arnd Hartmanns, Mark Timmer -- |t Optimizing Control Strategy Using Statistical Model Checking / |r Alexandre David [and others] |
| 505 | 8 | 0 | |g Session 8: |t Theorem Proving. |t Formal Stability Analysis of Optical Resonators / |r Umair Siddique, Vincent Aravantinos, Sofiène Tahar -- |t Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations / |r Alexey Solovyev, Thomas C. Hales -- |t Verifying a Privacy CA Remote Attestation Protocol / |r Brigid Halling, Perry Alexander -- |t Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory / |r Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar. |
| 505 | 8 | 0 | |t Short Papers. |t Formal Verification of a Parameterized Data Aggregation Protocol / |r Sergio Feo-Arenis, Bernd Westphal -- |t OnTrack: An Open Tooling Environment for Railway Verification / |r Phillip James [and others] -- |t Verification of Numerical Programs: From Real Numbers to Floating Point Numbers / |r Alwyn E. Goodloe [and others] -- |t Extracting Hybrid Automata from Control Code / |r Steven Lyde, Matthew Might -- |t PyNuSMV: NuSMV as a Python Library / |r Simon Busard, Charles Pecheur -- |t jUnitRV-Adding Runtime Verification to jUnit / |r Normann Decker, Martin Leucker, Daniel Thoma -- |t Using Language Engineering to Lift Languages and Analyses at the Domain Level / |r Daniel Ratiu [and others] -- |t On Designing an ACL2-Based C Integer Type Safety Checking Tool / |r Kevin Krause, Jim Alves-Foss -- |t Hierarchical Safety Cases / |r Ewen Denney, Ganesh Pai, Iain Whiteside. |
| 500 | |a International conference proceedings. | ||
| 504 | |a Includes bibliographical references and author index. | ||
| 520 | |a This book constitutes the refereed proceedings of the 5th International Symposium on NASA Formal Methods, NFM 2013, held in Moffett Field, CA, USA, in May 2013. The 28 revised regular papers presented together with 9 short papers talks were carefully reviewed and selected from 99 submissions. The topics are organized in topical sections on model checking; applications of formal methods; complex systems; static analysis; symbolic execution; requirements and specifications; probabilistic and statistical analysis; and theorem proving. | ||
| 588 | 0 | |a Print version record. | |
| 650 | 0 | |a Formal methods (Computer science) |v Congresses. |0 http://id.loc.gov/authorities/subjects/sh2008104061. | |
| 650 | 7 | |a Formal methods (Computer science) |2 fast |0 (OCoLC)fst00932926. | |
| 655 | 7 | |a Conference papers and proceedings. |2 fast |0 (OCoLC)fst01423772. | |
| 700 | 1 | |a Brat, Guillaume, |e editor. |0 http://id.loc.gov/authorities/names/nb2013016519. | |
| 700 | 1 | |a Rungta, Neha S. |q (Neha Shyam), |d 1979- |e editor. |0 http://id.loc.gov/authorities/names/no2007126294 |1 http://isni.org/isni/0000000047421188. | |
| 700 | 1 | |a Venet, Arnaud, |e editor. |0 http://id.loc.gov/authorities/names/no2009037735. | |
| 776 | 0 | 8 | |i Print version: |a NFM (Symposium) (5th : 2013 : Moffett Field, Calif.). |t NASA formal methods. NFM (Symposium) (5th : 2013 : Moffett Field, Calif.). |d Berlin ; New York : Springer, [2013] |z 9783642380877 |w (OCoLC)856339498. |
| 830 | 0 | |a Lecture notes in computer science ; |v 7871. |0 http://id.loc.gov/authorities/names/n42015162. | |
| 830 | 0 | |a LNCS sublibrary. |n SL 2, |p Programming and software engineering. |0 http://id.loc.gov/authorities/names/no2007033954. | |
| 856 | 4 | 0 | |u https://colorado.idm.oclc.org/login?url=http://link.springer.com/10.1007/978-3-642-38088-4 |z Full Text (via Springer) |
| 907 | |a .b73989885 |b 03-19-20 |c 06-20-13 | ||
| 998 | |a web |b 05-01-17 |c g |d b |e - |f eng |g gw |h 0 |i 1 | ||
| 907 | |a .b73989885 |b 07-02-19 |c 06-20-13 | ||
| 944 | |a MARS - RDA ENRICHED | ||
| 907 | |a .b73989885 |b 07-06-17 |c 06-20-13 | ||
| 907 | |a .b73989885 |b 05-23-17 |c 06-20-13 | ||
| 915 | |a I | ||
| 956 | |a Springer e-books | ||
| 956 | |b Springer Nature - Springer Computer Science eBooks 2013 English International | ||
| 956 | |b Springer Nature - Springer Computer Science eBooks 2013 English International | ||
| 999 | f | f | |i ce34d7ec-b0b5-5a34-a8f4-a62b68b59263 |s 40b08052-5e33-5363-bffe-fe6915378a8e |
| 952 | f | f | |p Can circulate |a University of Colorado Boulder |b Online |c Online |d Online |e QA76.9.F67 N46 2013 |h Library of Congress classification |i Ebooks, Prospector |n 1 |