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.
Computer Aided Verification [[electronic resource] ] : 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings / / edited by Ed Brinksma, Kim G. Larsen
| Computer Aided Verification [[electronic resource] ] : 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings / / edited by Ed Brinksma, Kim G. Larsen |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (X, 362 p.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Software engineering Mathematical logic Artificial intelligence Special purpose computers Theory of Computation Logics and Meanings of Programs Software Engineering Mathematical Logic and Formal Languages Artificial Intelligence Special Purpose and Application-Based Systems |
| ISBN | 3-540-45657-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Software Analysis and Model Checking -- The Quest for Efficient Boolean Satisfiability Solvers -- Invited Tutorials -- On Abstraction in Software Verification -- The Symbolic Approach to Hybrid Systems -- Infinite Games and Verification -- Symbolic Model Checking -- Symbolic Localization Reduction with Reconstruction Layering and Backtracking -- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions -- Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking -- Abstraction/Refinement and Model Checking -- Liveness with (0,1, ?)- Counter Abstraction -- Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking -- Automatic Abstraction Using Generalized Model Checking -- Compositional/Structural Verification -- Property Checking via Structural Analysis -- Conformance Checking for Models of Asynchronous Message Passing Software -- A Modular Checker for Multithreaded Programs -- Timing Analysis -- Automatic Derivation of Timing Constraints by Failure Analysis -- Deciding Separation Formulas with SAT -- Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling -- SAT Based Methods -- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT -- Applying SAT Methods in Unbounded Symbolic Model Checking -- SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques -- Semi-formal Bounded Model Checking -- Symbolic Model Checking -- Algorithmic Verification of Invalidation-Based Protocols -- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving -- Automated Unbounded Verification of Security Protocols -- Tool Presentations -- Exploiting Behavioral Hierarchy for Efficient Model Checking -- IF-2.0: A Validation Environment for Component-Based Real-Time Systems -- The AVISS Security Protocol Analysis Tool -- SPeeDI — A Verification Tool for Polygonal Hybrid Systems -- NuSMV 2: An OpenSource Tool for Symbolic Model Checking -- The d/dt Tool for Verification of Hybrid Systems -- Infinite Model Checking -- Model Checking Linear Properties of Prefix-Recognizable Systems -- Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking -- On Discrete Modeling and Model Checking for Nonlinear Analog Systems -- Compositional/Structural Verification -- Synchronous and Bidirectional Component Interfaces -- Interface Compatibility Checking for Software Modules -- Practical Methods for Proving Program Termination -- Extended Model Checking -- Evidence-Based Model Checking -- Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification -- Vacuum Cleaning CTL Formulae -- Tool Presentations -- CVC: A Cooperating Validity Checker -- ?Chek: A Multi-valued Model-Checker -- PathFinder: A Tool for Design Exploration -- Abstracting C with abC -- AMC: An Adaptive Model Checker -- Code Verification -- Temporal-Safety Proofs for Systems Code -- Regular Model Checking and Acceleration -- Extrapolating Tree Transformations -- Regular Tree Model Checking -- Compressing Transitions for Model Checking -- Model Reduction -- Canonical Prefixes of Petri Net Unfoldings -- State Space Reduction by Proving Confluence -- Fair Simulation Minimization. |
| Record Nr. | UNISA-996466361703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings / / edited by Ed Brinksma, Kim G. Larsen
| Computer Aided Verification : 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings / / edited by Ed Brinksma, Kim G. Larsen |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (X, 362 p.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Software engineering Logic, Symbolic and mathematical Artificial intelligence Computers, Special purpose Theory of Computation Logics and Meanings of Programs Software Engineering Mathematical Logic and Formal Languages Artificial Intelligence Special Purpose and Application-Based Systems |
| ISBN | 3-540-45657-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Software Analysis and Model Checking -- The Quest for Efficient Boolean Satisfiability Solvers -- Invited Tutorials -- On Abstraction in Software Verification -- The Symbolic Approach to Hybrid Systems -- Infinite Games and Verification -- Symbolic Model Checking -- Symbolic Localization Reduction with Reconstruction Layering and Backtracking -- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions -- Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking -- Abstraction/Refinement and Model Checking -- Liveness with (0,1, ?)- Counter Abstraction -- Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking -- Automatic Abstraction Using Generalized Model Checking -- Compositional/Structural Verification -- Property Checking via Structural Analysis -- Conformance Checking for Models of Asynchronous Message Passing Software -- A Modular Checker for Multithreaded Programs -- Timing Analysis -- Automatic Derivation of Timing Constraints by Failure Analysis -- Deciding Separation Formulas with SAT -- Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling -- SAT Based Methods -- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT -- Applying SAT Methods in Unbounded Symbolic Model Checking -- SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques -- Semi-formal Bounded Model Checking -- Symbolic Model Checking -- Algorithmic Verification of Invalidation-Based Protocols -- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving -- Automated Unbounded Verification of Security Protocols -- Tool Presentations -- Exploiting Behavioral Hierarchy for Efficient Model Checking -- IF-2.0: A Validation Environment for Component-Based Real-Time Systems -- The AVISS Security Protocol Analysis Tool -- SPeeDI — A Verification Tool for Polygonal Hybrid Systems -- NuSMV 2: An OpenSource Tool for Symbolic Model Checking -- The d/dt Tool for Verification of Hybrid Systems -- Infinite Model Checking -- Model Checking Linear Properties of Prefix-Recognizable Systems -- Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking -- On Discrete Modeling and Model Checking for Nonlinear Analog Systems -- Compositional/Structural Verification -- Synchronous and Bidirectional Component Interfaces -- Interface Compatibility Checking for Software Modules -- Practical Methods for Proving Program Termination -- Extended Model Checking -- Evidence-Based Model Checking -- Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification -- Vacuum Cleaning CTL Formulae -- Tool Presentations -- CVC: A Cooperating Validity Checker -- ?Chek: A Multi-valued Model-Checker -- PathFinder: A Tool for Design Exploration -- Abstracting C with abC -- AMC: An Adaptive Model Checker -- Code Verification -- Temporal-Safety Proofs for Systems Code -- Regular Model Checking and Acceleration -- Extrapolating Tree Transformations -- Regular Tree Model Checking -- Compressing Transitions for Model Checking -- Model Reduction -- Canonical Prefixes of Petri Net Unfoldings -- State Space Reduction by Proving Confluence -- Fair Simulation Minimization. |
| Record Nr. | UNINA-9910767569403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Lectures on Formal Methods and Performance Analysis [[electronic resource] ] : First EEF/Euro Summer School on Trends in Computer Science Berg en Dal, The Netherlands, July 3-7, 2000. Revised Lectures / / edited by Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen
| Lectures on Formal Methods and Performance Analysis [[electronic resource] ] : First EEF/Euro Summer School on Trends in Computer Science Berg en Dal, The Netherlands, July 3-7, 2000. Revised Lectures / / edited by Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (VII, 434 p.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer engineering Computer logic Computer system failures Computer communication systems Software Engineering/Programming and Operating Systems Computer Engineering Logics and Meanings of Programs Software Engineering System Performance and Evaluation Computer Communication Networks |
| ISBN | 3-540-44667-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Methods for Performance Evaluation -- Markovian Models for Performance and Dependability Evaluation -- to Stochastic Petri Nets -- Non-Markovian Analysis -- Process Algebra and Markov Chains -- Verification of Randomized Distributed Algorithms -- Constructing Automata from Temporal Logic Formulas: A Tutorial? -- Exploiting Structure in Solution: Decomposing Compositional Models -- Stochastic Activity Networks: Formal Definitions and Concepts? -- Distributed and Structured Analysis Approaches to Study Large and Complex Systems? -- General Distributions in Process Algebra. |
| Record Nr. | UNISA-996465812203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Lectures on Formal Methods and Performance Analysis : First EEF/Euro Summer School on Trends in Computer Science Berg en Dal, The Netherlands, July 3-7, 2000. Revised Lectures / / edited by Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen
| Lectures on Formal Methods and Performance Analysis : First EEF/Euro Summer School on Trends in Computer Science Berg en Dal, The Netherlands, July 3-7, 2000. Revised Lectures / / edited by Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (VII, 434 p.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer engineering Computer logic Computer system failures Computer networks Software Engineering/Programming and Operating Systems Computer Engineering Logics and Meanings of Programs Software Engineering System Performance and Evaluation Computer Communication Networks |
| ISBN | 3-540-44667-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Methods for Performance Evaluation -- Markovian Models for Performance and Dependability Evaluation -- to Stochastic Petri Nets -- Non-Markovian Analysis -- Process Algebra and Markov Chains -- Verification of Randomized Distributed Algorithms -- Constructing Automata from Temporal Logic Formulas: A Tutorial? -- Exploiting Structure in Solution: Decomposing Compositional Models -- Stochastic Activity Networks: Formal Definitions and Concepts? -- Distributed and Structured Analysis Approaches to Study Large and Complex Systems? -- General Distributions in Process Algebra. |
| Record Nr. | UNINA-9910143595603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (X, 437 p.) |
| Disciplina | 004.2/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer engineering
Computers Software engineering Computer logic Computer communication systems Computer Engineering Theory of Computation Software Engineering Logics and Meanings of Programs Computer Communication Networks |
| ISBN | 3-540-68519-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Hardware and software synthesis, optimization, and verification from Esterel programs -- Manipulation algorithms for K*BMDs -- Combining partial order and symmetry reductions -- Partial model checking with ROBDDs -- Space efficient reachability analysis through use of pseudo-root states -- The reference component of PEP -- A tool to support formal reasoning about computer languages -- The term processor generator Kimwitu -- Graphs in MetaFrame: The unifying power of polymorphism -- A tableau system for linear-TIME temporal logic -- Model-checking for a subclass of event structures -- Real-time logics: Fictitious clock as an abstraction of dense time -- Mosel: A flexible toolset for monadic second-order logic -- A brief introduction to coloured Petri Nets -- Design/CPN — A computer tool for Coloured Petri Nets -- Formal verification of statecharts with instantaneous chain reactions -- Compositional state space generation from Lotos programs -- Syntactic detection of process divergence and non-local choice in message sequence charts -- An automata based verification environment for mobile processes -- Compositional performance analysis -- Incremental development of deadlock-free communicating systems -- Automatic synthesis of specifications from the dynamic observation of reactive programs -- Visual verification of reactive systems -- Theorem prover support for the refinement of stream processing functions -- Integration in PVS: Tables, types, and model checking -- Test generation for intelligent networks using model checking -- Mechanically verified self-stabilizing hierarchical algorithms -- The bounded retransmission protocol must be on time!. |
| Record Nr. | UNISA-996465533403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings / / edited by Ed Brinksma |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (X, 437 p.) |
| Disciplina | 004.2/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer engineering
Computers Software engineering Computer logic Computer networks Computer Engineering Theory of Computation Software Engineering Logics and Meanings of Programs Computer Communication Networks |
| ISBN | 3-540-68519-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Hardware and software synthesis, optimization, and verification from Esterel programs -- Manipulation algorithms for K*BMDs -- Combining partial order and symmetry reductions -- Partial model checking with ROBDDs -- Space efficient reachability analysis through use of pseudo-root states -- The reference component of PEP -- A tool to support formal reasoning about computer languages -- The term processor generator Kimwitu -- Graphs in MetaFrame: The unifying power of polymorphism -- A tableau system for linear-TIME temporal logic -- Model-checking for a subclass of event structures -- Real-time logics: Fictitious clock as an abstraction of dense time -- Mosel: A flexible toolset for monadic second-order logic -- A brief introduction to coloured Petri Nets -- Design/CPN — A computer tool for Coloured Petri Nets -- Formal verification of statecharts with instantaneous chain reactions -- Compositional state space generation from Lotos programs -- Syntactic detection of process divergence and non-local choice in message sequence charts -- An automata based verification environment for mobile processes -- Compositional performance analysis -- Incremental development of deadlock-free communicating systems -- Automatic synthesis of specifications from the dynamic observation of reactive programs -- Visual verification of reactive systems -- Theorem prover support for the refinement of stream processing functions -- Integration in PVS: Tables, types, and model checking -- Test generation for intelligent networks using model checking -- Mechanically verified self-stabilizing hierarchical algorithms -- The bounded retransmission protocol must be on time!. |
| Record Nr. | UNINA-9910768447303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : First International Workshop, TACAS '95, Aarhus, Denmark, May 19 - 20, 1995. Selected Papers / / edited by Ed Brinksma, W. Rance Cleaveland, Kim G. Larsen, Tiziana Margaria, Bernhard Steffen
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : First International Workshop, TACAS '95, Aarhus, Denmark, May 19 - 20, 1995. Selected Papers / / edited by Ed Brinksma, W. Rance Cleaveland, Kim G. Larsen, Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 1995.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 |
| Descrizione fisica | 1 online resource (VII, 298 p.) |
| Disciplina | 005.2 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer engineering
Operating systems (Computers) Computers Computer logic Software engineering Computer communication systems Computer Engineering Operating Systems Theory of Computation Logics and Meanings of Programs Software Engineering Computer Communication Networks |
| ISBN | 3-540-48509-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Combining model checking and deduction for I/O- automata -- A constraint oriented proof methodology based on modal transition systems -- A user guide to HyTech -- Modal ?-calculus, model checking and Gauß elimination -- Mona: Monadic second-order logic in practice -- Efficient simplification of bisimulation formulas -- Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock -- A front-end generator for verification tools -- Analytic and locally approximate solutions to properties of probabilistic processes -- Model checking of non-finite state processes by finite approximations -- On automatic and interactive design of communicating systems -- Layers as knowledge transitions in the design of distributed systems -- Parallelism for free: Bitvector analyses ? no state explosion!. |
| Record Nr. | UNISA-996465479303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||