Formal Methods: Applications and Technology [[electronic resource] ] : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol
| Formal Methods: Applications and Technology [[electronic resource] ] : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (371 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Special purpose computers Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
| ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
| Record Nr. | UNISA-996466247603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Methods: Applications and Technology : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol
| Formal Methods: Applications and Technology : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (371 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Computers, Special purpose Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
| ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
| Record Nr. | UNINA-9910483608403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Integrated formal methods : 5th international conference, IFM 2005, Eindhoven, The Netherlands, November 29-December 2, 2005 : proceedings / / Judi Romijn, Graeme Smith, Jaco van de Pol (eds.)
| Integrated formal methods : 5th international conference, IFM 2005, Eindhoven, The Netherlands, November 29-December 2, 2005 : proceedings / / Judi Romijn, Graeme Smith, Jaco van de Pol (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
| Descrizione fisica | 1 online resource (XI, 407 p.) |
| Disciplina | 004.01/51 |
| Altri autori (Persone) |
RomijnJudi
SmithGraeme <1966-> PolJaco van de |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- A Family of Mathematical Methods for Professional Software Documentation -- Generating Path Conditions for Timed Systems -- Software Model Checking: Searching for Computations in the Abstract or the Concrete -- Session: Components -- Adaptive Techniques for Specification Matching in Embedded Systems: A Comparative Study -- Session: State/Event-Based Verification -- State/Event Software Verification for Branching-Time Specifications -- Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods -- Chunks: Component Verification in CSP ? B -- Session: System Development -- Agile Formal Method Engineering -- An Automated Failure Mode and Effect Analysis Based on High-Level Design Specification with Behavior Trees -- Enabling Security Testing from Specification to Code -- Session: Applications of B -- Development of Fault Tolerant Grid Applications Using Distributed B -- Formal Methods Meet Domain Specific Languages -- Synthesizing B Specifications from eb 3 Attribute Definitions -- Session: Tool Support -- CZT Support for Z Extensions -- Embedding the Stable Failures Model of CSP in PVS -- Model-Based Prototyping of an Interoperability Protocol for Mobile Ad-Hoc Networks -- Session: Non-software Domains -- Translating Hardware Process Algebras into Standard Process Algebras: Illustration with CHP and LOTOS -- Formalising Interactive Voice Services with SDL -- Session: Semantics -- A Fixpoint Semantics of Event Systems With and Without Fairness Assumptions -- Session: UML and Statecharts -- Consistency Checking of Sequence Diagrams and Statechart Diagrams Using the ?-Calculus -- An Integrated Framework for Scenarios and State Machines -- Consistency in UML and B Multi-view Specifications. |
| Altri titoli varianti | IFM 2005 |
| Record Nr. | UNINA-9910484068803321 |
| Berlin ; ; New York, : Springer, c2005 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model checking software : 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, proceedings / / Jaco van de Pol, Michael Weber, (eds.)
| Model checking software : 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010, proceedings / / Jaco van de Pol, Michael Weber, (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer, 2010 |
| Descrizione fisica | 1 online resource (X, 263 p. 70 illus.) |
| Disciplina | 005.1 |
| Altri autori (Persone) |
PolJaco van de
WeberMichael (Michael F.) |
| Collana |
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Lecture notes in computer science |
| Soggetto topico |
Computer software - Verifications
Spin (Computer program language) |
| ISBN |
9786613567512
9781280389597 1280389591 9783642161643 3642161642 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Satisfiability Modulo Theories for Model Checking -- SMT-Based Software Model Checking -- Symbolic Object Code Analysis -- Model Checking in Context -- Experimental Comparison of Concolic and Random Testing for Java Card Applets -- Combining SPIN with ns-2 for Protocol Optimization -- Automatic Generation of Model Checking Scripts Based on Environment Modeling -- Implementation and Performance of Model Checking -- Model Checking: Cleared for Take Off -- Context-Enhanced Directed Model Checking -- Efficient Explicit-State Model Checking on General Purpose Graphics Processors -- The SpinJa Model Checker -- LTL and Büchi Automata -- On the Virtue of Patience: Minimizing Büchi Automata -- Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance -- Nevertrace Claims for Model Checking -- Infinite State Models -- A False History of True Concurrency: From Petri to Tools -- Analysing Mu-Calculus Properties of Pushdown Systems -- Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains -- An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models -- Concurrent Software -- Context-Bounded Translations for Concurrent Software: An Empirical Evaluation -- One Stack to Run Them All. |
| Record Nr. | UNINA-9910484805403321 |
| Berlin ; ; Heidelberg, : Springer, 2010 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||