Automated Technology for Verification and Analysis [[electronic resource] ] : Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings / / edited by Farn Wang |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XII, 510 p.) |
Disciplina | 004.015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer-aided engineering
Computer logic Computers Computer communication systems Special purpose computers Software engineering Computer-Aided Engineering (CAD, CAE) and Design Logics and Meanings of Programs Information Systems and Communication Service Computer Communication Networks Special Purpose and Application-Based Systems Software Engineering |
ISBN | 3-540-30476-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Speech -- Games for Formal Design and Verification of Reactive Systems -- Evolution of Model Checking into the EDA Industry -- Abstraction Refinement -- Invited Speech -- Tools for Automated Verification of Web Services -- Theorem Proving Languages for Verification -- An Automated Rigorous Review Method for Verifying and Validating Formal Specifications -- Papers -- Toward Unbounded Model Checking for Region Automata -- Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity -- Synthesising Attacks on Cryptographic Protocols -- Büchi Complementation Made Tighter -- SAT-Based Verification of Safe Petri Nets -- Disjunctive Invariants for Numerical Systems -- Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas -- Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts -- Exploiting Symmetries for Testing Equivalence in the Spi Calculus -- Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors -- Abstraction-Based Model Checking Using Heuristical Refinement -- A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata -- Design and Evaluation of a Symbolic and Abstraction-Based Model Checker -- Component-Wise Instruction-Cache Behavior Prediction -- Validating the Translation of an Industrial Optimizing Compiler -- Composition of Accelerations to Verify Infinite Heterogeneous Systems -- Hybrid System Verification Is Not a Sinecure -- Providing Automated Verification in HOL Using MDGs -- Specification, Abduction, and Proof -- Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets -- Typeness for ?-Regular Automata -- Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits -- Mutation Coverage Estimation for Model Checking -- Modular Model Checking of Software Specifications with Simultaneous Environment Generation -- Rabin Tree and Its Application to Group Key Distribution -- Using Overlay Networks to Improve VoIP Reliability -- Integrity-Enhanced Verification Scheme for Software-Intensive Organizations -- RCGES: Retargetable Code Generation for Embedded Systems -- Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets -- First-Order LTL Model Checking Using MDGs -- Localizing Errors in Counterexample with Iteratively Witness Searching -- Verification of WCDMA Protocols and Implementation -- Efficient Representation of Algebraic Expressions -- Development of RTOS for PLC Using Formal Methods -- Reducing Parametric Automata: A Multimedia Protocol Service Case Study -- Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems -- Solving Box-Pushing Games via Model Checking with Optimizations -- CLP Based Static Property Checking -- A Temporal Assertion Extension to Verilog. |
Record Nr. | UNINA-9910144341103321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Automated Technology for Verification and Analysis [[electronic resource] ] : Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings / / edited by Farn Wang |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XII, 510 p.) |
Disciplina | 004.015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer-aided engineering
Computer logic Computers Computer communication systems Special purpose computers Software engineering Computer-Aided Engineering (CAD, CAE) and Design Logics and Meanings of Programs Information Systems and Communication Service Computer Communication Networks Special Purpose and Application-Based Systems Software Engineering |
ISBN | 3-540-30476-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Speech -- Games for Formal Design and Verification of Reactive Systems -- Evolution of Model Checking into the EDA Industry -- Abstraction Refinement -- Invited Speech -- Tools for Automated Verification of Web Services -- Theorem Proving Languages for Verification -- An Automated Rigorous Review Method for Verifying and Validating Formal Specifications -- Papers -- Toward Unbounded Model Checking for Region Automata -- Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity -- Synthesising Attacks on Cryptographic Protocols -- Büchi Complementation Made Tighter -- SAT-Based Verification of Safe Petri Nets -- Disjunctive Invariants for Numerical Systems -- Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas -- Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts -- Exploiting Symmetries for Testing Equivalence in the Spi Calculus -- Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors -- Abstraction-Based Model Checking Using Heuristical Refinement -- A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata -- Design and Evaluation of a Symbolic and Abstraction-Based Model Checker -- Component-Wise Instruction-Cache Behavior Prediction -- Validating the Translation of an Industrial Optimizing Compiler -- Composition of Accelerations to Verify Infinite Heterogeneous Systems -- Hybrid System Verification Is Not a Sinecure -- Providing Automated Verification in HOL Using MDGs -- Specification, Abduction, and Proof -- Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets -- Typeness for ?-Regular Automata -- Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits -- Mutation Coverage Estimation for Model Checking -- Modular Model Checking of Software Specifications with Simultaneous Environment Generation -- Rabin Tree and Its Application to Group Key Distribution -- Using Overlay Networks to Improve VoIP Reliability -- Integrity-Enhanced Verification Scheme for Software-Intensive Organizations -- RCGES: Retargetable Code Generation for Embedded Systems -- Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets -- First-Order LTL Model Checking Using MDGs -- Localizing Errors in Counterexample with Iteratively Witness Searching -- Verification of WCDMA Protocols and Implementation -- Efficient Representation of Algebraic Expressions -- Development of RTOS for PLC Using Formal Methods -- Reducing Parametric Automata: A Multimedia Protocol Service Case Study -- Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems -- Solving Box-Pushing Games via Model Checking with Optimizations -- CLP Based Static Property Checking -- A Temporal Assertion Extension to Verilog. |
Record Nr. | UNISA-996465750603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Techniques for Networked and Distributed Systems - FORTE 2005 [[electronic resource] ] : 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings / / edited by Farn Wang |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XII, 558 p.) |
Disciplina | 004.6/2 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer communication systems
Software engineering Computer logic Operating systems (Computers) Computer Communication Networks Software Engineering Logics and Meanings of Programs Operating Systems |
Classificazione | 54.32 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | KEYNOTE SPEECHES -- Ranking Abstraction as Companion to Predicate Abstraction -- Developing High Quality Software with Formal Methods: What Else Is Needed? -- A Testing Architecture for Designing High-Reliable MANET Protocols -- REGULAR PAPERS -- A Composition Operator for Systems with Active and Passive Actions -- A Formal Semantics of UML StateCharts by Means of Timed Petri Nets -- A Hierarchy of Implementable MSC Languages -- Combining Static Analysis and Model Checking for Systems Employing Commutative Functions -- Fast Generic Model-Checking for Data-Based Systems -- Logic and Model Checking for Hidden Markov Models -- Proving ??-Calculus Properties with SAT-Based Model Checking -- Ad Hoc Routing Protocol Verification Through Broadcast Abstraction -- Discovering Chatter and Incompleteness in the Datagram Congestion Control Protocol -- Thread Allocation Protocols for Distributed Real-Time and Embedded Systems -- A Petri Net View of Mobility -- Modular Verification of Petri Nets Properties: A Structure-Based Approach -- An Improved Conformance Testing Method -- Resolving Observability Problems in Distributed Test Architectures -- Automatic Generation of Conflict-Free IPsec Policies -- A Framework Based Approach for Formal Modeling and Analysis of Multi-level Attacks in Computer Networks -- Model Checking for Timed Statecharts -- Abstraction-Guided Model Checking Using Symbolic IDA* and Heuristic Synthesis -- Modeling and Verification of Safety-Critical Systems Using Safecharts -- Structure Preserving Data Abstractions for Statecharts -- Amortised Bisimulations -- Proof Methodologies for Behavioural Equivalence in Dpi -- Deriving Non-determinism from Conjunction and Disjunction -- Abstract Operational Semantics for Use Case Maps -- ArchiTRIO: A UML-Compatible Language for Architectural Description and Its Formal Semantics -- Submodule Construction for Extended State Machine Models -- Towards Synchronizing Linear Collaborative Objects with Operational Transformation -- Designing Efficient Fail-Safe Multitolerant Systems -- Hierarchical Decision Diagrams to Exploit Model Structure -- Computing Subgraph Probability of Random Geometric Graphs: Quantitative Analyses of Wireless Ad Hoc Networks -- Formalising Web Services -- From Automata Networks to HMSCs: A Reverse Model Engineering Perspective -- Properties as Processes: Their Specification and Verification -- SHORT PAPERS -- Epoch Distance of the Random Waypoint Model in Mobile Ad Hoc Networks -- Automatic Partitioner for Behavior Level Distributed Logic Simulation -- Expressive Completeness of an Event-Pattern Reactive Programming Language -- Formalizing Interoperability Testing: Quiescence Management and Test Generation -- Formal Description of Mobile IPv6 Protocol -- Incremental Modeling Under Large-Scale Distributed Interaction -- The Inductive Approach to Strand Space -- Compositional Modelling and Verification of IPv6 Mobility. |
Record Nr. | UNISA-996466221803316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Techniques for Networked and Distributed Systems - FORTE 2005 [[electronic resource] ] : 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings / / edited by Farn Wang |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XII, 558 p.) |
Disciplina | 004.6/2 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer communication systems
Software engineering Computer logic Operating systems (Computers) Computer Communication Networks Software Engineering Logics and Meanings of Programs Operating Systems |
Classificazione | 54.32 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | KEYNOTE SPEECHES -- Ranking Abstraction as Companion to Predicate Abstraction -- Developing High Quality Software with Formal Methods: What Else Is Needed? -- A Testing Architecture for Designing High-Reliable MANET Protocols -- REGULAR PAPERS -- A Composition Operator for Systems with Active and Passive Actions -- A Formal Semantics of UML StateCharts by Means of Timed Petri Nets -- A Hierarchy of Implementable MSC Languages -- Combining Static Analysis and Model Checking for Systems Employing Commutative Functions -- Fast Generic Model-Checking for Data-Based Systems -- Logic and Model Checking for Hidden Markov Models -- Proving ??-Calculus Properties with SAT-Based Model Checking -- Ad Hoc Routing Protocol Verification Through Broadcast Abstraction -- Discovering Chatter and Incompleteness in the Datagram Congestion Control Protocol -- Thread Allocation Protocols for Distributed Real-Time and Embedded Systems -- A Petri Net View of Mobility -- Modular Verification of Petri Nets Properties: A Structure-Based Approach -- An Improved Conformance Testing Method -- Resolving Observability Problems in Distributed Test Architectures -- Automatic Generation of Conflict-Free IPsec Policies -- A Framework Based Approach for Formal Modeling and Analysis of Multi-level Attacks in Computer Networks -- Model Checking for Timed Statecharts -- Abstraction-Guided Model Checking Using Symbolic IDA* and Heuristic Synthesis -- Modeling and Verification of Safety-Critical Systems Using Safecharts -- Structure Preserving Data Abstractions for Statecharts -- Amortised Bisimulations -- Proof Methodologies for Behavioural Equivalence in Dpi -- Deriving Non-determinism from Conjunction and Disjunction -- Abstract Operational Semantics for Use Case Maps -- ArchiTRIO: A UML-Compatible Language for Architectural Description and Its Formal Semantics -- Submodule Construction for Extended State Machine Models -- Towards Synchronizing Linear Collaborative Objects with Operational Transformation -- Designing Efficient Fail-Safe Multitolerant Systems -- Hierarchical Decision Diagrams to Exploit Model Structure -- Computing Subgraph Probability of Random Geometric Graphs: Quantitative Analyses of Wireless Ad Hoc Networks -- Formalising Web Services -- From Automata Networks to HMSCs: A Reverse Model Engineering Perspective -- Properties as Processes: Their Specification and Verification -- SHORT PAPERS -- Epoch Distance of the Random Waypoint Model in Mobile Ad Hoc Networks -- Automatic Partitioner for Behavior Level Distributed Logic Simulation -- Expressive Completeness of an Event-Pattern Reactive Programming Language -- Formalizing Interoperability Testing: Quiescence Management and Test Generation -- Formal Description of Mobile IPv6 Protocol -- Incremental Modeling Under Large-Scale Distributed Interaction -- The Inductive Approach to Strand Space -- Compositional Modelling and Verification of IPv6 Mobility. |
Record Nr. | UNINA-9910484245403321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Theoretical Aspects of Computing – ICTAC 2016 [[electronic resource] ] : 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings / / edited by Augusto Sampaio, Farn Wang |
Edizione | [1st ed. 2016.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
Descrizione fisica | 1 online resource (XVII, 479 p. 108 illus.) |
Disciplina | 004 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Compilers (Computer programs) Computer science—Mathematics Discrete mathematics Software engineering Machine theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Discrete Mathematics in Computer Science Software Engineering Formal Languages and Automata Theory |
ISBN | 3-319-46750-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Topical sections on program verification -- Design, synthesis and testing -- Calculi -- Specifications -- Composition and transformation -- Automata -- Temporal logics -- Tool and short papers. |
Record Nr. | UNISA-996465666203316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Theoretical Aspects of Computing – ICTAC 2016 [[electronic resource] ] : 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings / / edited by Augusto Sampaio, Farn Wang |
Edizione | [1st ed. 2016.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
Descrizione fisica | 1 online resource (XVII, 479 p. 108 illus.) |
Disciplina | 004 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Compilers (Computer programs) Computer science—Mathematics Discrete mathematics Software engineering Machine theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Discrete Mathematics in Computer Science Software Engineering Formal Languages and Automata Theory |
ISBN | 3-319-46750-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Topical sections on program verification -- Design, synthesis and testing -- Calculi -- Specifications -- Composition and transformation -- Automata -- Temporal logics -- Tool and short papers. |
Record Nr. | UNINA-9910484470903321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|