Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Formal methods for industrial critical systems : 15th international workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010, proceedings / / Stefan Kowalewski, Marco Roveri (eds.)
| Formal methods for industrial critical systems : 15th international workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010, proceedings / / Stefan Kowalewski, Marco Roveri (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2010 |
| Descrizione fisica | 1 online resource (XII, 231 p. 82 illus.) |
| Disciplina | 005.131 |
| Altri autori (Persone) |
KowalewskiS (Stefan)
RoveriMarco |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 2, Programming and software engineering |
| Soggetto topico |
Formal methods (Computer science)
Software engineering Computer programs - Verification |
| ISBN |
1-280-38921-4
9786613567130 3-642-15898-6 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Metrô Rio ATP Case Study -- Practical Issues with Formal Specifications -- Formal Analysis of BPMN Models Using Event-B -- Developing Mode-Rich Satellite Software by Refinement in Event B -- Automatic Error Correction of Java Programs -- Range Analysis of Microcontroller Code Using Bit-Level Congruences -- An Automated Translator for Model Checking Time Constrained Workflow Systems -- Correctness of Sensor Network Applications by Software Bounded Model Checking -- Model Checking the FlexRay Physical Layer Protocol -- SMT-Based Formal Verification of a TTEthernet Synchronization Function -- Embedded Network Protocols for Mobile Devices -- A Study of Shared-Memory Mutual Exclusion Protocols Using CADP -- A Formal Model of Identity Mixer -- Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept. |
| Altri titoli varianti | FMICS 2010 |
| Record Nr. | UNINA-9910484301203321 |
| Berlin, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and algorithms for the construction and analysis of systems : 15th International Conference, TACAS 2009, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22 - 29, 2009 : proceedings / / Stefan Kowalewski, Anna Philippou (eds.)
| Tools and algorithms for the construction and analysis of systems : 15th International Conference, TACAS 2009, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22 - 29, 2009 : proceedings / / Stefan Kowalewski, Anna Philippou (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2009 |
| Descrizione fisica | 1 online resource (XVI, 456 p.) |
| Disciplina | 005.1 |
| Altri autori (Persone) |
KowalewskiS (Stefan)
PhilippouAnna |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Development
System analysis System design |
| ISBN | 3-642-00768-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model Checking I -- Hierarchical Set Decision Diagrams and Regular Models -- Büchi Complementation and Size-Change Termination -- Learning Minimal Separating DFA’s for Compositional Verification -- Tools I -- RBAC-PAT: A Policy Analysis Tool for Role Based Access Control -- ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets -- Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches -- Alpaga: A Tool for Solving Parity Games with Imperfect Information -- Game-Theoretic Approaches -- Compositional Predicate Abstraction from Game Semantics -- Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications -- Computing Weakest Strategies for Safety Games of Imperfect Information -- Verification of Concurrent Programs -- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads -- Semantic Reduction of Thread Interleavings in Concurrent Programs -- Inferring Synchronization under Limited Observability -- The Complexity of Predicting Atomicity Violations -- Tools II -- MoonWalker: Verification of .NET Programs -- Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays -- The Yogi Project: Software Property Checking via Static Analysis and Testing -- TaPAS: The Talence Presburger Arithmetic Suite -- Model Checking II -- Transition-Based Directed Model Checking -- Memoised Garbage Collection for Software Model Checking -- Hierarchical Adaptive State Space Caching Based on Level Sampling -- Parametric Analysis -- Static Analysis Techniques for Parameterised Boolean Equation Systems -- Parametric Trace Slicing and Monitoring -- Generative Approaches -- From Tests to Proofs -- Test Input Generation for Programs with Pointers -- Specification Mining with Few False Positives -- Program Analysis -- Path Feasibility Analysis for String-Manipulating Programs -- Symbolic String Verification: Combining String Analysis and Size Analysis -- Iterating Octagons -- Verifying Reference Counting Implementations -- Hybrid Systems -- Falsification of LTL Safety Properties in Hybrid Systems -- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints -- Decision Procedures and Theorem Proving -- All-Termination(T) -- Ground Interpolation for the Theory of Equality -- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets -- Invited Contribution -- Bridging the Gap Between Model-Based Development and Model Checking. |
| Altri titoli varianti |
ETAPS 2009
TACAS 2009 |
| Record Nr. | UNINA-9910483253403321 |
| Berlin ; ; New York, : Springer, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||