Muutke küpsiste eelistusi

E-raamat: FM 2011: Formal Methods: 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings

Edited by , Edited by
  • 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.

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 17th International Symposium on Formal Methods, FM 2011, held in Limerick, Ireland, in June 2011. The 29 revised full papers presented together with 3 invited talks were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on cyber-physical systems, runtime analysis, case studies/tools, experience, program compilation and transformation, security, progress algebra, education, concurrency, dynamic structures, and model checking.
Invited Talks
Model Integration and Cyber Physical Systems: A Semantics Perspective
1(1)
Janos Sztipanovits
Some Thoughts on Behavioral Programming
2(1)
David Harel
The Only Way Is Up
3(9)
Jasmin Fisher
Nir Piterman
Moshe Y. Vardi
Cyber-Physical Systems
Does It Pay to Extend the Perimeter of a World Model?
12(15)
Werner Damm
Bernd Finkbeiner
System Verification through Program Verification
27(15)
Daniel Dietsch
Bernd Westphal
Andreas Podelski
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified
42(15)
Sarah M. Loos
Andre Platzer
Ligia Nistor
Runtime Analysis
TraceContract: A Scala DSL for Trace Analysis
57(16)
Howard Barringer
Klaus Havelund
Using Debuggers to Understand Failed Verification Attempts
73(15)
Peter Mutter
Joseph N. Ruskiewicz
Sampling-Based Runtime Verification
88(15)
Borzoo Bonakdarpour
Samaneh Navabpour
Sebastian Fischmeister
Case Studies / Tools
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
103(15)
Fabienne Boyer
Olivier Gruber
Gwen Salaun
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems
118(15)
Anne E. Haxthausen
Andreas A. Kjae
Marie Le Bliguet
Relational Reasoning via SMT Solving
133(16)
Aboubakr Achraf El Ghazi
Mana Taghdiri
Building VCL Models and Automatically Generating Z Specifications from Them
149(5)
Nuno Amalio
Christian Glodt
Pierre Kelsen
Experience
The 1st Verified Software Competition: Experience Report
154(15)
Vladimir Klebanov
Peter Muller
Natarajan Shankar
Gary T. Leavens
Valentin Wustholz
Eyad Alkassar
Rob Arthan
Derek Bronish
Rod Chapman
Ernie Cohen
Mark Hillebrand
Bart Jacobs
K. Rustan
M. Leino
Rosemary Monahan
Frank Piessens
Nadia Polikarpova
Tom Ridge
Jan Smans
Stephan Tobies
Thomas Tuerk
Mattias Ulbrich
Benjamin Weiß
Program Compilation and Transformation
Validated Compilation through Logic
169(15)
Guodong Li
Certification of Safe Polynomial Memory Bounds
184(16)
Javier de Dios
Ricardo Pena
Relational Verification Using Product Programs
200(15)
Gilles Barthe
Juan Manuel Crespo
Cesar Kunz
Security
Specifying Confidentiality in Circus
215(16)
Michael J. Banks
Jeremy L. Jacob
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization
231(15)
Gilles Barthe
Gustavo Betarte
Juan Diego Campo
Carlos Luna
The Safety-Critical Java Memory Model: A Formal Account
246(16)
Ana Cavalcanti
Andy Wellings
Jim Woodcock
Process Algebra
Failure-Divergence Refinement of Compensating Communicating Processes
262(16)
Zhenbang Chen
Zhiming Liu
Ji Wang
Termination without in CSP
278(15)
Steve Dunne
Timed Migration and Interaction with Access Permissions
293(15)
Gabriel Ciobanu
Maciej Koutny
Education
From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community
308(15)
Jonathan P. Bowen
Steve Reeves
Concurrency
Verifying Linearisability with Potential Linearisation Points
323(15)
John Derrick
Gerhard Schellhorn
Heike Wehrheim
Refinement-Based Verification of Local Synchronization Algorithms
338(15)
Dominique Mery
Mohamed Mosbah
Mohamed Tounsi
Simulating Concurrent Behaviors with Worst-Case Cost Bounds
353(16)
Elvira Albert
Samir Genaim
Miguel Gomez-Zamalloa
Einar Broch Johnsen
Rudolf Schlatte
S. Lizeth Tapia Tarifa
Dynamic Structures
Automatically Refining Partial Specifications for Program Verification
369(17)
Shengchao Qin
Chenguang Luo
Wei-Ngan Chin
Guanhua He
Structured Specifications for Better Verification of Heap-Manipulating Programs
386(16)
Cristian Gherghina
Cristina David
Shengchao Qin
Wei-Ngan Chin
Verification of Unloadable Modules
402(15)
Bart Jacobs
Jan Smans
Frank Piessens
Model Checking
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking
417(15)
Kristin Y. Rozier
Moshe Y. Vardi
On Combining State Space Reductions with Global Fairness Assumptions
432(17)
Shao Jie Zhang
Jun Sun
Jun Pang
Yang Liu
Jin Song Dong
Author Index 449