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] ] : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I / / edited by Swarat Chaudhuri, Azadeh Farzan
| Computer Aided Verification [[electronic resource] ] : 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I / / edited by Swarat Chaudhuri, Azadeh Farzan |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVII, 541 p. 125 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks |
| ISBN | 3-319-41528-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Probabilistic systems -- Synthesis -- Constraint solving -- Model checking -- Program analysis -- Timed and hybrid systems -- Verification in practice -- Concurrency -- Automata and games. |
| Record Nr. | UNINA-9910483951803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II / / edited by Daniel Kroening, Corina S. Păsăreanu
| Computer Aided Verification [[electronic resource] ] : 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II / / edited by Daniel Kroening, Corina S. Păsăreanu |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XVIII, 469 p. 107 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks |
| ISBN | 3-319-21668-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | SMT Techniques and Applications -- POLING: SMT Aided Linearizability Proofs -- Finding Bounded Path in Graph Using SMT for Automatic Clock Routing -- Cutting the Mix -- The Inez Mathematical Programming Modulo Theories Framework -- Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets -- Deciding Local Theory Extensions via E-matching -- HW Verification -- Modular Deductive Verification of Multiprocessor Hardware Designs -- Word-Level Symbolic Trajectory Evaluation -- Verifying Linearizability of Intel® Software Guard Extensions -- Synthesis Synthesis Through Unification -- From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis -- Counterexample-Guided Quantifier Instantiation for Synthesis in SMT -- Deductive Program Repair -- Quantifying Conformance Using the Skorokhod Metric -- Pareto Curves of Multidimensional Mean-Payoff Games -- Termination -- Conflict-Driven Conditional Termination -- Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs -- Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions -- Measuring with Timed Patterns -- Automatic Verification of Stability and Safety for Delay Differential Equations -- Time Robustness in MTL and Expressivity in Hybrid System Falsification -- Concurrency -- Adaptive Concretization for Parallel Program Synthesis -- Automatic Completion of Distributed Protocols with Symmetry -- An Axiomatic Specification for Sequential Memory Models -- Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems -- Automated and Modular Refinement Reasoning for Concurrent Programs. |
| Record Nr. | UNISA-996204727003316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II / / edited by Daniel Kroening, Corina S. Păsăreanu
| Computer Aided Verification [[electronic resource] ] : 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II / / edited by Daniel Kroening, Corina S. Păsăreanu |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XVIII, 469 p. 107 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks |
| ISBN | 3-319-21668-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | SMT Techniques and Applications -- POLING: SMT Aided Linearizability Proofs -- Finding Bounded Path in Graph Using SMT for Automatic Clock Routing -- Cutting the Mix -- The Inez Mathematical Programming Modulo Theories Framework -- Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets -- Deciding Local Theory Extensions via E-matching -- HW Verification -- Modular Deductive Verification of Multiprocessor Hardware Designs -- Word-Level Symbolic Trajectory Evaluation -- Verifying Linearizability of Intel® Software Guard Extensions -- Synthesis Synthesis Through Unification -- From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis -- Counterexample-Guided Quantifier Instantiation for Synthesis in SMT -- Deductive Program Repair -- Quantifying Conformance Using the Skorokhod Metric -- Pareto Curves of Multidimensional Mean-Payoff Games -- Termination -- Conflict-Driven Conditional Termination -- Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs -- Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions -- Measuring with Timed Patterns -- Automatic Verification of Stability and Safety for Delay Differential Equations -- Time Robustness in MTL and Expressivity in Hybrid System Falsification -- Concurrency -- Adaptive Concretization for Parallel Program Synthesis -- Automatic Completion of Distributed Protocols with Symmetry -- An Axiomatic Specification for Sequential Memory Models -- Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems -- Automated and Modular Refinement Reasoning for Concurrent Programs. |
| Record Nr. | UNINA-9910484945103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings / / edited by Natasha Sharygina, Helmut Veith
| Computer Aided Verification [[electronic resource] ] : 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings / / edited by Natasha Sharygina, Helmut Veith |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XXII, 1015 p. 237 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Computers, Special purpose Computer Science Logic and Foundations of Programming Software Engineering Special Purpose and Application-Based Systems |
| ISBN | 3-642-39799-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automata Networks -- Model-Checking Signal Transduction Networks through Decreasing Reachability Sets -- TTP: Tool for Tumor Progression -- Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking -- Parameterized Verification of Asynchronous Shared-Memory Systems -- Partial Orders for Efficient BMC of Concurrent Software -- Incremental, Inductive Coverability -- Automatic linearizability proofs of concurrent objects with cooperating -- Updates -- Duet: Static Analysis for Unbounded Parallelism -- SVA and PSL Local Variables -- A Practical Approach -- Formal Verification of Hardware Synthesis -- CacBDD: A BDD Package with Dynamic Cache Management -- Distributed Explicit State Model Checking of Deadlock Freedom -- Exponential-Condition-Based Barrier Certificate Generation for Safety -- Verification of Hybrid Systems -- Efficient Robust Monitoring for STL -- Abstraction based Model-Checking of Stability of Hybrid Systems -- Faster Algorithms for Markov Decision Processes with Low Tree width -- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis -- Importance Splitting for Statistical Model Checking Rare Properties -- Minimal Sets over Monotone Predicates in Boolean Formulae -- Smten: Automatic Translation of High-level Symbolic Computations into SMT Queries -- QUAIL: a quantitative security analyzer for imperative code -- Effectively Propositional Reasoning about Reachability in Linked Data Structures -- Learning Universally Quantified Invariants of Linear Data Structures -- GOAL for Games, Omega-Automata, and Logics -- Efficient synthesis for concurrency using semantics-preserving Transformations. |
| Record Nr. | UNISA-996466042903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings / / edited by Natasha Sharygina, Helmut Veith
| Computer Aided Verification [[electronic resource] ] : 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings / / edited by Natasha Sharygina, Helmut Veith |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XXII, 1015 p. 237 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Computers, Special purpose Computer Science Logic and Foundations of Programming Software Engineering Special Purpose and Application-Based Systems |
| ISBN | 3-642-39799-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automata Networks -- Model-Checking Signal Transduction Networks through Decreasing Reachability Sets -- TTP: Tool for Tumor Progression -- Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking -- Parameterized Verification of Asynchronous Shared-Memory Systems -- Partial Orders for Efficient BMC of Concurrent Software -- Incremental, Inductive Coverability -- Automatic linearizability proofs of concurrent objects with cooperating -- Updates -- Duet: Static Analysis for Unbounded Parallelism -- SVA and PSL Local Variables -- A Practical Approach -- Formal Verification of Hardware Synthesis -- CacBDD: A BDD Package with Dynamic Cache Management -- Distributed Explicit State Model Checking of Deadlock Freedom -- Exponential-Condition-Based Barrier Certificate Generation for Safety -- Verification of Hybrid Systems -- Efficient Robust Monitoring for STL -- Abstraction based Model-Checking of Stability of Hybrid Systems -- Faster Algorithms for Markov Decision Processes with Low Tree width -- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis -- Importance Splitting for Statistical Model Checking Rare Properties -- Minimal Sets over Monotone Predicates in Boolean Formulae -- Smten: Automatic Translation of High-level Symbolic Computations into SMT Queries -- QUAIL: a quantitative security analyzer for imperative code -- Effectively Propositional Reasoning about Reachability in Linked Data Structures -- Learning Universally Quantified Invariants of Linear Data Structures -- GOAL for Games, Omega-Automata, and Logics -- Efficient synthesis for concurrency using semantics-preserving Transformations. |
| Record Nr. | UNINA-9910483521103321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings / / edited by Warren A. Hunt, Jr., Fabio Somenzi
| Computer Aided Verification [[electronic resource] ] : 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings / / edited by Warren A. Hunt, Jr., Fabio Somenzi |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (XII, 462 p.) |
| Disciplina | 005.14 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Logic design Special purpose computers Software engineering Mathematical logic Theory of Computation Logics and Meanings of Programs Logic Design Special Purpose and Application-Based Systems Software Engineering Mathematical Logic and Formal Languages |
| ISBN | 3-540-45069-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extending Bounded Model Checking -- Interpolation and SAT-Based Model Checking -- Bounded Model Checking and Induction: From Refutation to Verification -- Symbolic Model Checking -- Reasoning with Temporal Logic on Truncated Paths -- Structural Symbolic CTL Model Checking of Asynchronous Systems -- A Work-Efficient Distributed Algorithm for Reachability Analysis -- Games, Trees, and Counters -- Modular Strategies for Infinite Games on Recursive Graphs -- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded -- Dense Counter Machines and Verification Problems -- Tool Presentations I -- TRIM: A Tool for Triggered Message Sequence Charts -- Model Checking Multi-Agent Programs with CASP -- Monitoring Temporal Rules Combined with Time Series -- FAST: Fast Acceleration of Symbolic Transition Systems -- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems -- Abstraction I -- Making Predicate Abstraction Efficient: -- A Symbolic Approach to Predicate Abstraction -- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods -- Dense Time -- Digitizing Interval Duration Logic -- Timed Control with Partial Observability -- Hybrid Acceleration Using Real Vector Automata -- Tool Presentations II -- Abstraction and BDDs Complement SAT-Based BMC in DiVer -- TLQSolver: A Temporal Logic Query Checker -- Evidence Explorer: A Tool for Exploring Model-Checking Proofs -- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols -- Infinite State Systems -- Iterating Transducers in the Large -- Algorithmic Improvements in Regular Model Checking -- Efficient Image Computation in Infinite State Model Checking -- Abstraction II -- Thread-Modular Abstraction Refinement -- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement -- Abstraction for Branching Time Properties -- Applications -- Certifying Optimality of State Estimation Programs -- Domain-Specific Optimization in Automata Learning -- Model Checking Conformance with Scenario-Based Specifications -- Theorem Proving -- Deductive Verification of Advanced Out-of-Order Microprocessors -- Theorem Proving Using Lazy Proof Explication -- Automata-Based Verification -- Enhanced Vacuity Detection in Linear Temporal Logic -- Bridging the Gap between Fair Simulation and Trace Inclusion -- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic -- Invariants -- Strengthening Invariants by Symbolic Consistency Testing -- Linear Invariant Generation Using Non-linear Constraint Solving -- Explicit Model Checking -- To Store or Not to Store -- Calculating ?-Confluence Compositionally. |
| Record Nr. | UNISA-996465898403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings / / edited by Warren A. Hunt, Jr., Fabio Somenzi
| Computer Aided Verification [[electronic resource] ] : 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings / / edited by Warren A. Hunt, Jr., Fabio Somenzi |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (XII, 462 p.) |
| Disciplina | 005.14 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Logic design Special purpose computers Software engineering Mathematical logic Theory of Computation Logics and Meanings of Programs Logic Design Special Purpose and Application-Based Systems Software Engineering Mathematical Logic and Formal Languages |
| ISBN | 3-540-45069-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extending Bounded Model Checking -- Interpolation and SAT-Based Model Checking -- Bounded Model Checking and Induction: From Refutation to Verification -- Symbolic Model Checking -- Reasoning with Temporal Logic on Truncated Paths -- Structural Symbolic CTL Model Checking of Asynchronous Systems -- A Work-Efficient Distributed Algorithm for Reachability Analysis -- Games, Trees, and Counters -- Modular Strategies for Infinite Games on Recursive Graphs -- Fast Mu-Calculus Model Checking when Tree-Width Is Bounded -- Dense Counter Machines and Verification Problems -- Tool Presentations I -- TRIM: A Tool for Triggered Message Sequence Charts -- Model Checking Multi-Agent Programs with CASP -- Monitoring Temporal Rules Combined with Time Series -- FAST: Fast Acceleration of Symbolic Transition Systems -- Rabbit: A Tool for BDD-Based Verification of Real-Time Systems -- Abstraction I -- Making Predicate Abstraction Efficient: -- A Symbolic Approach to Predicate Abstraction -- Unbounded, Fully Symbolic Model Checking of Timed Automata Using Boolean Methods -- Dense Time -- Digitizing Interval Duration Logic -- Timed Control with Partial Observability -- Hybrid Acceleration Using Real Vector Automata -- Tool Presentations II -- Abstraction and BDDs Complement SAT-Based BMC in DiVer -- TLQSolver: A Temporal Logic Query Checker -- Evidence Explorer: A Tool for Exploring Model-Checking Proofs -- HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols -- Infinite State Systems -- Iterating Transducers in the Large -- Algorithmic Improvements in Regular Model Checking -- Efficient Image Computation in Infinite State Model Checking -- Abstraction II -- Thread-Modular Abstraction Refinement -- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement -- Abstraction for Branching Time Properties -- Applications -- Certifying Optimality of State Estimation Programs -- Domain-Specific Optimization in Automata Learning -- Model Checking Conformance with Scenario-Based Specifications -- Theorem Proving -- Deductive Verification of Advanced Out-of-Order Microprocessors -- Theorem Proving Using Lazy Proof Explication -- Automata-Based Verification -- Enhanced Vacuity Detection in Linear Temporal Logic -- Bridging the Gap between Fair Simulation and Trace Inclusion -- An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic -- Invariants -- Strengthening Invariants by Symbolic Consistency Testing -- Linear Invariant Generation Using Non-linear Constraint Solving -- Explicit Model Checking -- To Store or Not to Store -- Calculating ?-Confluence Compositionally. |
| Record Nr. | UNINA-9910767533903321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer-aided verification : 11th International Conference, Cav '99, Trento, Italy, July 6-1-10, 1999 : proceedings / / Nicolas Halbwachs, Doron Peled (editors)
| Computer-aided verification : 11th International Conference, Cav '99, Trento, Italy, July 6-1-10, 1999 : proceedings / / Nicolas Halbwachs, Doron Peled (editors) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 506 p.) |
| Disciplina | 005.14 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Verification
Electronic digital computers - Evaluation |
| ISBN | 3-540-48683-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials and Invited Papers -- Alternative Approaches to Hardware Verification -- The Compositional Specification of Timed Systems — A Tutorial -- Timed Automata -- Ståalmarck’s Method with Extensions to Quantified Boolean Formulas -- Verification of Parameterized Systems by Dynamic Induction -- Formal Methods for Conformance Testing: Theory Can Be Practical -- Processor Verification -- Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach -- Verifying Safety Properties of a PowerPC? Microprocessor Using Symbolic Model Checking without BDDs -- Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists -- Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study -- Protocol Verification and Testing -- Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol -- Test Generation Derived from Model-Checking -- Latency Insensitive Protocols -- Infinite State Space -- Handling Global Conditions in Parametrized System Verification -- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis -- Experience with Predicate Abstraction -- Theory of Verification -- Model Checking of Safety Properties -- A Complete Finite Prefix for Process Algebra -- The Mathematical Foundation of Symbolic Trajectory Evaluation -- Assume-Guarantee Refinement between Different Time Scales -- Linear Temporal Logic -- Efficient Decision Procedures for Model Checking of Linear Time Logic Properties -- Stutter-Invariant Languages, ?-Automata, and Temporal Logic -- Improved Automata Generation for Linear Temporal Logic -- Modeling of Systems -- On the Representation of Probabilities over Structured Domains -- Model Checking Partial State Spaces with 3-Valued Temporal Logics -- Elementary Microarchitecture Algebra -- Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems -- Symbolic Model-Checking -- Stepwise CTL Model Checking of State/Event Systems -- Optimizing Symbolic Model Checking for Constraint-Rich Models -- Efficient Timed Reachability Analysis Using Clock Difference Diagrams -- Theorem Proving -- Mechanizing Proofs of Computation Equivalence -- Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation -- Automatic Verification of Combinational and Pipelined FFT Circuits -- Automata-Theoretic Methods -- Efficient Analysis of Cyclic Definitions -- A Theory of Restrictions for Logics and Automata -- Model Checking Based on Sequential ATPG -- Automatic Verification of Abstract State Machines -- Abstraction -- Abstract and Model Check while You Prove -- Deciding Equality Formulas by Small Domains Instantiations -- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions -- Tool Presentations -- A Toolbox for the Analysis of Discrete Event Dynamic Systems -- TIPPtool: Compositional Specification and Analysis of Markovian Performance Models -- Java Bytecode Verification by Model Checking -- NuSMV: A New Symbolic Model Verifier -- PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. |
| Record Nr. | UNINA-9910143460703321 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer-aided verification : 11th International Conference, Cav '99, Trento, Italy, July 6-1-10, 1999 : proceedings / / Nicolas Halbwachs, Doron Peled (editors)
| Computer-aided verification : 11th International Conference, Cav '99, Trento, Italy, July 6-1-10, 1999 : proceedings / / Nicolas Halbwachs, Doron Peled (editors) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 506 p.) |
| Disciplina | 005.14 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Verification
Electronic digital computers - Evaluation |
| ISBN | 3-540-48683-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials and Invited Papers -- Alternative Approaches to Hardware Verification -- The Compositional Specification of Timed Systems — A Tutorial -- Timed Automata -- Ståalmarck’s Method with Extensions to Quantified Boolean Formulas -- Verification of Parameterized Systems by Dynamic Induction -- Formal Methods for Conformance Testing: Theory Can Be Practical -- Processor Verification -- Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach -- Verifying Safety Properties of a PowerPC? Microprocessor Using Symbolic Model Checking without BDDs -- Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists -- Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study -- Protocol Verification and Testing -- Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol -- Test Generation Derived from Model-Checking -- Latency Insensitive Protocols -- Infinite State Space -- Handling Global Conditions in Parametrized System Verification -- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis -- Experience with Predicate Abstraction -- Theory of Verification -- Model Checking of Safety Properties -- A Complete Finite Prefix for Process Algebra -- The Mathematical Foundation of Symbolic Trajectory Evaluation -- Assume-Guarantee Refinement between Different Time Scales -- Linear Temporal Logic -- Efficient Decision Procedures for Model Checking of Linear Time Logic Properties -- Stutter-Invariant Languages, ?-Automata, and Temporal Logic -- Improved Automata Generation for Linear Temporal Logic -- Modeling of Systems -- On the Representation of Probabilities over Structured Domains -- Model Checking Partial State Spaces with 3-Valued Temporal Logics -- Elementary Microarchitecture Algebra -- Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems -- Symbolic Model-Checking -- Stepwise CTL Model Checking of State/Event Systems -- Optimizing Symbolic Model Checking for Constraint-Rich Models -- Efficient Timed Reachability Analysis Using Clock Difference Diagrams -- Theorem Proving -- Mechanizing Proofs of Computation Equivalence -- Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation -- Automatic Verification of Combinational and Pipelined FFT Circuits -- Automata-Theoretic Methods -- Efficient Analysis of Cyclic Definitions -- A Theory of Restrictions for Logics and Automata -- Model Checking Based on Sequential ATPG -- Automatic Verification of Abstract State Machines -- Abstraction -- Abstract and Model Check while You Prove -- Deciding Equality Formulas by Small Domains Instantiations -- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions -- Tool Presentations -- A Toolbox for the Analysis of Discrete Event Dynamic Systems -- TIPPtool: Compositional Specification and Analysis of Markovian Performance Models -- Java Bytecode Verification by Model Checking -- NuSMV: A New Symbolic Model Verifier -- PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols. |
| Record Nr. | UNISA-996465752303316 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Concise Guide to Software Testing [[electronic resource] /] / by Gerard O'Regan
| Concise Guide to Software Testing [[electronic resource] /] / by Gerard O'Regan |
| Autore | O'Regan Gerard |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXIV, 293 p. 92 illus., 84 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Undergraduate Topics in Computer Science |
| Soggetto topico |
Software engineering
Quality control Reliability Industrial safety Software Engineering Quality Control, Reliability, Safety and Risk |
| ISBN | 3-030-28494-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Fundamentals of Software Quality -- Fundamentals of Software Engineering -- Fundamentals of Software Testing -- Static Testing -- Software Test Planning -- Test Case Analysis and Design -- Test Execution and Management -- Test Outsourcing -- Test Metrics and Problem Solving -- Software Testing Tools -- Test Process Improvement -- Testing in the Agile World -- Verification of Safety Critical Systems -- Legal, Ethical and Professional Aspects of Testing -- Configuration Management -- Epilogue. |
| Record Nr. | UNINA-9910349277903321 |
O'Regan Gerard
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
