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.
Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 8th International Conference, EvoMUSART 2019, Held as Part of EvoStar 2019, Leipzig, Germany, April 24–26, 2019, Proceedings / / edited by Anikó Ekárt, Antonios Liapis, María Luz Castro Pena
| Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 8th International Conference, EvoMUSART 2019, Held as Part of EvoStar 2019, Leipzig, Germany, April 24–26, 2019, Proceedings / / edited by Anikó Ekárt, Antonios Liapis, María Luz Castro Pena |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (X, 249 p. 113 illus., 78 illus. in color.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Algorithms
Artificial intelligence Data mining Computer arithmetic and logic units Artificial Intelligence Data Mining and Knowledge Discovery Arithmetic and Logic Structures |
| ISBN | 3-030-16667-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Deep Learning Concepts for Evolutionary Art -- Adversarial Evolution and Deep Learning – How Does An Artist Play with Our Visual System -- Autonomy, Authenticity, Authorship and Intention in Computer Generated Art -- Camera Obscurer: Generative Art for Design Inspiration -- Swarm-Based Identification of Animation Key Points from 2D-medialness Maps -- Paintings, Polygons and Plant Propagation -- Evolutionary Games for Audiovisual Works: Exploring the Demographic Prisoner's Dilemma -- Emojinating: Evolving Emoji Blends -- Automatically Generating Engaging Presentation Slide Decks -- Tired of choosing? Just Add Structure and Virtual Reality -- EvoChef: Show Me What to Cook! Artificial Evolution of Culinary Arts -- Comparing Models for Harmony Prediction in An Interactive Audio Looper -- Stochastic Synthesizer Patch Exploration in Edisyn -- Evolutionary Multi-Objective Training Set Selection of Data Instances and Augmentations for Vocal Detection -- Automatic Jazz Melody Composition Through a Learning-Based Genetic Algorithm -- Exploring Transfer Functions in Evolved CTRNNs for Music Generation. . |
| Record Nr. | UNINA-9910337850703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 6th International Conference, EvoMUSART 2017, Amsterdam, The Netherlands, April 19–21, 2017, Proceedings / / edited by João Correia, Vic Ciesielski, Antonios Liapis
| Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 6th International Conference, EvoMUSART 2017, Amsterdam, The Netherlands, April 19–21, 2017, Proceedings / / edited by João Correia, Vic Ciesielski, Antonios Liapis |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (X, 371 p. 169 illus.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Algorithms
Data mining Artificial intelligence Computer vision Computer science—Mathematics Mathematical statistics Digital humanities Data Mining and Knowledge Discovery Artificial Intelligence Computer Vision Probability and Statistics in Computer Science Digital Humanities |
| ISBN | 3-319-55750-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Algorithmic Songwriting with ALYSIA -- On Symmetry, Aesthetics and Quantifying Symmetrical Complexity -- Towards Polyphony Reconstruction Using Multidimensional Multiple Sequence Alignment -- Melody Retrieval and Classification Using Biologically-Inspired Techniques -- Evolved Aesthetic Analogies to Improve Artistic Experience -- Deep Artificial Composer: A Creative Neural Network Model for Automated Melody Generation -- A Kind of Bio-inspired Learning of mUsic stylE -- Using Autonomous Agents to Improvise Music Compositions in Real-time -- Generating Polyphonic Music Using Tied Parallel Networks -- Mixed-initiative Creative Drawing with webIconoscope -- Clustering Agents for the Evolution of Autonomous Musical Fitness -- EvoFashion: Customising Fashion Through Evolution -- A Swarm Environment for Experimental Performance and Improvisation -- Niche Constructing Drawing Robots -- Automated Shape Design by Grammatical Evolution -- Evolutionary Image Transition Using Random Walks -- Evaluation Rules for Evolutionary Generation of Drum Patterns in Jazz Solos -- Assessing Augmented Creativity: Putting a Lovelace Machine for Interactive Title Generation through a Human Creativity Test -- Play It again: Evolved Audio Effects and Synthesizer Programming -- Fashion Design Aid System with Application of Interactive Genetic Algorithms -- Generalization Performance of Western Instrument Recognition Models in Polyphonic Mixtures with Ethnic Samples -- Exploring the Exactitudes Portrait Series with Restricted Boltzmann Machines -- Evolving Mondrian-Style Artworks -- Predicting Expressive Bow Controls for Violin and Viola. . |
| Record Nr. | UNISA-996466202903316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 6th International Conference, EvoMUSART 2017, Amsterdam, The Netherlands, April 19–21, 2017, Proceedings / / edited by João Correia, Vic Ciesielski, Antonios Liapis
| Computational Intelligence in Music, Sound, Art and Design [[electronic resource] ] : 6th International Conference, EvoMUSART 2017, Amsterdam, The Netherlands, April 19–21, 2017, Proceedings / / edited by João Correia, Vic Ciesielski, Antonios Liapis |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (X, 371 p. 169 illus.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Algorithms
Data mining Artificial intelligence Computer vision Computer science—Mathematics Mathematical statistics Digital humanities Data Mining and Knowledge Discovery Artificial Intelligence Computer Vision Probability and Statistics in Computer Science Digital Humanities |
| ISBN | 3-319-55750-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Algorithmic Songwriting with ALYSIA -- On Symmetry, Aesthetics and Quantifying Symmetrical Complexity -- Towards Polyphony Reconstruction Using Multidimensional Multiple Sequence Alignment -- Melody Retrieval and Classification Using Biologically-Inspired Techniques -- Evolved Aesthetic Analogies to Improve Artistic Experience -- Deep Artificial Composer: A Creative Neural Network Model for Automated Melody Generation -- A Kind of Bio-inspired Learning of mUsic stylE -- Using Autonomous Agents to Improvise Music Compositions in Real-time -- Generating Polyphonic Music Using Tied Parallel Networks -- Mixed-initiative Creative Drawing with webIconoscope -- Clustering Agents for the Evolution of Autonomous Musical Fitness -- EvoFashion: Customising Fashion Through Evolution -- A Swarm Environment for Experimental Performance and Improvisation -- Niche Constructing Drawing Robots -- Automated Shape Design by Grammatical Evolution -- Evolutionary Image Transition Using Random Walks -- Evaluation Rules for Evolutionary Generation of Drum Patterns in Jazz Solos -- Assessing Augmented Creativity: Putting a Lovelace Machine for Interactive Title Generation through a Human Creativity Test -- Play It again: Evolved Audio Effects and Synthesizer Programming -- Fashion Design Aid System with Application of Interactive Genetic Algorithms -- Generalization Performance of Western Instrument Recognition Models in Polyphonic Mixtures with Ethnic Samples -- Exploring the Exactitudes Portrait Series with Restricted Boltzmann Machines -- Evolving Mondrian-Style Artworks -- Predicting Expressive Bow Controls for Violin and Viola. . |
| Record Nr. | UNINA-9910484653603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
| Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XV, 722 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer systems Software engineering Computer science Machine theory Programming Techniques Computer System Implementation Software Engineering Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-642-02658-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving. |
| Record Nr. | UNISA-996465423003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
| Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XV, 722 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer systems Software engineering Computer science Machine theory Programming Techniques Computer System Implementation Software Engineering Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-642-02658-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving. |
| Record Nr. | UNINA-9910483039603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik
| Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (XVII, 558 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer systems Computer science Software engineering Machine theory Artificial intelligence Programming Techniques Computer System Implementation Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence |
| ISBN | 3-540-70545-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools – Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools – Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools – Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using “Crucial Events” -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools – Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for (?)-Regular Model Checking -- Faster Than Uppaal?. |
| Record Nr. | UNISA-996466098703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik
| Computer Aided Verification [[electronic resource] ] : 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings / / edited by Aarti Gupta, Sharad Malik |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (XVII, 558 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer systems Computer science Software engineering Machine theory Artificial intelligence Programming Techniques Computer System Implementation Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence |
| ISBN | 3-540-70545-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools – Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools – Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools – Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using “Crucial Events” -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools – Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for (?)-Regular Model Checking -- Faster Than Uppaal?. |
| Record Nr. | UNINA-9910483216903321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Concurrency in programming and database systems / Arthur J. Bernstein, Philip M. Lewis
| Concurrency in programming and database systems / Arthur J. Bernstein, Philip M. Lewis |
| Autore | Bernstein, Arthur J. |
| Pubbl/distr/stampa | Boston [MA] : Jones and Bartlett, c1993 |
| Descrizione fisica | XVII, 548 p. ; 24 cm |
| Disciplina | 005.11 |
| Soggetto non controllato |
Databases - Teoria
Programmazione parallela |
| ISBN | 0-86720-205-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-990001323360403321 |
Bernstein, Arthur J.
|
||
| Boston [MA] : Jones and Bartlett, c1993 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Constraint handling in metaheuristics and applications / / Anand J. Kulkarni [and four others], editors
| Constraint handling in metaheuristics and applications / / Anand J. Kulkarni [and four others], editors |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (336 pages) |
| Disciplina | 005.11 |
| Soggetto topico |
Constraint programming (Computer science)
Metaheuristics |
| ISBN | 981-336-710-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910483057703321 |
| Singapore : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Constraint handling in metaheuristics and applications / / Anand J. Kulkarni [and four others], editors
| Constraint handling in metaheuristics and applications / / Anand J. Kulkarni [and four others], editors |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (336 pages) |
| Disciplina | 005.11 |
| Soggetto topico |
Constraint programming (Computer science)
Metaheuristics |
| ISBN | 981-336-710-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464492003316 |
| Singapore : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
