Muutke küpsiste eelistusi

E-raamat: NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012, Proceedings

Edited by , Edited by
  • Formaat: PDF+DRM
  • Sari: Lecture Notes in Computer Science 7226
  • Ilmumisaeg: 30-Mar-2012
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: eng
  • ISBN-13: 9783642288913
  • Formaat - PDF+DRM
  • Hind: 55,56 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
  • Formaat: PDF+DRM
  • Sari: Lecture Notes in Computer Science 7226
  • Ilmumisaeg: 30-Mar-2012
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: eng
  • ISBN-13: 9783642288913

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

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.
SMT-Based Model Checking
1(1)
Cesare Tinelli
Verified Software Toolchain (Abstract)
2(1)
Andrew W. Appel
Formal Verification by Abstract Interpretation
3(5)
Patrick Cousot
Quantitative Timed Analysis of Interactive Markov Chains
8(16)
Dennis Guck
Tingting Han
Joost-Pieter Katoen
Martin R. Neuhaußer
Lessons Learnt from the Adoption of Formal Model-Based Development
24(15)
Alessio Ferrari
Alessandro Fantechi
Stefania Gnesi
Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines
39(15)
Karolina Zurowska
Juergen Dingel
Inferring Definite Counterexamples through Under-Approximation
54(16)
Jorg Brauer
Axel Simon
Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical Debugging
70(15)
Ross Gore
Paul F. Reynolds Jr.
Rigorous Polynomial Approximation Using Taylor Models in COQ
85(15)
Nicolas Brisebarre
Mioara Joldes
Erik Martin-Dorel
Micaela Mayero
Jean-Michel Muller
Ioana Pasca
Laurence Rideau
Laurent Thery
Enhancing the Inverse Method with State Merging
100(6)
Etienne Andre
Laurent Fribourg
Romain Soulat
Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented Languages
106(14)
Alexander Herz
Kalmer Apinis
Testing Static Analyzers with Randomly Generated Programs
120(6)
Pascal Cuoq
Benjamin Monate
Anne Pacalet
Virgile Prevosto
John Regehr
Boris Yakobowski
Xuejun Yang
Compositional Verification of Architectural Models
126(15)
Darren Cofer
Andrew Gacek
Steven Miller
Michael W. Whalen
Brian LaValley
Lui Sha
A Safety Case Pattern for Model-Based Development Approach
141(6)
Anaheed Ayoub
Baek-Gyu Kim
Insup Lee
Oleg Sokolsky
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL
147(15)
Heber Herencia-Zapana
Romain Jobredeaux
Sam Owre
Pierre-Loic Garoche
Eric Feron
Gilberto Perez
Pablo Ascariz
Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements (Preliminary Results)
162(6)
Wenbin Li
Jane Huffman Hayes
Miroslaw Truszczynski
Some Steps into Verification of Exact Real Arithmetic
168(6)
Norbert Th. Muller
Christian Uhrhan
Runtime Verification Meets Android Security
174(7)
Andreas Bauer
Jan-Christoph Kuster
Gil Vegliach
Specification in PDL with Recursion
181(14)
Xinxin Liu
Bingtian Xue
Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study
195(15)
Aditi Tagore
Diego Zaccai
Bruce W. Weide
Sound Formal Verification of Linux's USB BP Keyboard Driver
210(6)
Willem Penninckx
Jan Tobias Muhlberg
Jan Smans
Bart Jacobs
Frank Piessens
Learning Markov Models for Stationary System Behaviors
216(15)
Yingke Chen
Hua Mao
Manfred Jaeger
Thomas Dyhre Nielsen
Kim Guldstrand Larsen
Brian Nielsen
The Use of Rippling to Automate Event-B Invariant Preservation Proofs
231(6)
Yuhui Lin
Alan Bundy
Gudmund Grov
Thread-Modular Model Checking with Iterative Refinement
237(15)
Wenrui Meng
Fei He
Bow-Yaw Wang
Qiang Liu
Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs
252(15)
Jiri Barnat
Lubos Brim
Petr Rockai
Integrating Statechart Components in Polyglot
267(6)
Daniel Balasubramanian
Corina S. Pasareanu
Jason Biatek
Thomas Pressburger
Gabor Karsai
Michael Lowry
Michael W. Whalen
Using PVS to Investigate Incidents through the Lens of Distributed Cognition
273(6)
Paolo Masci
Huayi Huang
Paul Curzon
Michael D. Harrison
Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms
279(16)
Roberto Bruttomesso
Alessandro Carioni
Silvio Ghilardi
Silvio Ranise
Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems
295(15)
Jason Belt
Robby
Patrice Chalin
John Hatcliff
Xianghua Deng
Generating Verifiable Java Code from Verified PVS Specifications
310(16)
Leonard Lensink
Sjaak Smetsers
Marko van Eekelen
Belief Bisimulation for Hidden Markov Models: Logical Characterisation and Decision Algorithm
326(15)
David N. Jansen
Flemming Nielson
Lijun Zhang
Abstract Model Repair
341(15)
George Chatzieleftheriou
Borzoo Bonakdarpour
Scott A. Smolka
Panagiotis Katsaros
CLSE: Closed-Loop Symbolic Execution
356(15)
Rupak Majumdar
Indranil Saha
K. C. Shashidhar
Zilong Wang
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
371(17)
Michael Backes
Alex Busenius
Catalin Hritcu
Incremental Verification with Mode Variable Invariants in State Machines
388(15)
Temesghen Kahsai
Pierre-Loic Garoche
Cesare Tinelli
Mike Whalen
A Semantic Analysis of Wireless Network Security Protocols
403(15)
Damiano Macedonio
Massimo Merro
Runtime Verification with Predictive Semantics
418(15)
Xian Zhang
Martin Leucker
Wei Dong
A Case Study in Verification of Embedded Network Software
433(16)
Kalyan C. Regula
Hampton Smith
Heather Harton Keown
Jason O. Hallstrom
Nigamanth Sridhar
Murali Sitaraman
Checking and Distributing Statistical Model Checking
449(16)
Peter Bulychev
Alexandre David
Kim Guldstrand Larsen
Axel Legay
Marius Mikucionis
Danny Bogsted Poulsen
Author Index 465