Info
Computer Aided Verification [[electronic resource] ] : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem
| Computer Aided Verification [[electronic resource] ] : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXXIV, 877 p. 205 illus.) |
| Disciplina | 005.1015113 |
| 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-08867-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Software Verification -- The Spirit of Ghost Code -- SMT-Based Model Checking for Recursive Programs -- Property-Directed Shape Analysis -- Shape Analysis via Second-Order Bi-Abduction -- ICE: A Robust Framework for Learning Invariants -- From Invariant Checking to Invariant Inference Using Randomized Search -- SMACK: Decoupling Source Language Details from Verifier Implementations -- Security -- Synthesis of Masking Countermeasures against Side Channel Attacks -- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies -- String Constraints for Verification -- A Conference Management System with Verified Document Confidentiality -- VAC - Verifier of Administrative Role-Based Access Control Policies -- Automata -- From LTL to Deterministic Automata: A Safraless Compositional Approach -- Symbolic Visibly Pushdown Automata -- Model Checking and Testing -- Engineering a Static Verification Tool for GPU Kernels -- Lazy Annotation Revisited -- Interpolating Property Directed Reachability -- Verifying Relative Error Bounds Using Symbolic Simulation -- Regression Test Selection for Distributed Software Histories -- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components -- Software Verification in the Google App-Engine Cloud -- The nuXmv Symbolic Model Checker -- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions -- Finding Instability in Biological Models -- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells -- Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions -- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections -- Verifying LTL Properties of Hybrid Systems with K-Liveness -- Games and Synthesis -- Safraless Synthesis for Epistemic Temporal Specifications -- Minimizing Running Costs in Consumption Systems -- CEGAR for Qualitative Analysis of Probabilistic Systems -- Optimal Guard Synthesis for Memory Safety -- Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion -- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications -- Solving Games without Controllable Predecessor -- G4LTL-ST: Automatic Generation of PLC Programs -- Concurrency -- Automatic Atomicity Verification for Clients of Concurrent Data Structures -- Regression-Free Synthesis for Concurrency -- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization -- An SMT-Based Approach to Coverability Analysis -- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes -- SMT and Theorem Proving -- Monadic Decomposition -- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions -- Bit-Vector Rewriting with Automatic Rule Generation -- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors -- AVATAR: The Architecture for First-Order Theorem Provers -- Automating Separation Logic with Trees and Data -- A Nonlinear Real Arithmetic Fragment -- Yices 2.2 -- Bounds and Termination -- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis -- Symbolic Resource Bound Inference for Functional Programs -- Proving Non-termination Using Max-SMT -- Termination Analysis by Learning Terminating Programs -- Causal Termination of Multi-threaded Programs -- Abstraction -- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) -- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction -- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. |
| Record Nr. | UNISA-996199992703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem
| Computer Aided Verification : 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings / / edited by Armin Biere, Roderick Bloem |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXXIV, 877 p. 205 illus.) |
| Disciplina | 005.1015113 |
| 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-08867-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Software Verification -- The Spirit of Ghost Code -- SMT-Based Model Checking for Recursive Programs -- Property-Directed Shape Analysis -- Shape Analysis via Second-Order Bi-Abduction -- ICE: A Robust Framework for Learning Invariants -- From Invariant Checking to Invariant Inference Using Randomized Search -- SMACK: Decoupling Source Language Details from Verifier Implementations -- Security -- Synthesis of Masking Countermeasures against Side Channel Attacks -- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies -- String Constraints for Verification -- A Conference Management System with Verified Document Confidentiality -- VAC - Verifier of Administrative Role-Based Access Control Policies -- Automata -- From LTL to Deterministic Automata: A Safraless Compositional Approach -- Symbolic Visibly Pushdown Automata -- Model Checking and Testing -- Engineering a Static Verification Tool for GPU Kernels -- Lazy Annotation Revisited -- Interpolating Property Directed Reachability -- Verifying Relative Error Bounds Using Symbolic Simulation -- Regression Test Selection for Distributed Software Histories -- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components -- Software Verification in the Google App-Engine Cloud -- The nuXmv Symbolic Model Checker -- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions -- Finding Instability in Biological Models -- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells -- Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions -- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections -- Verifying LTL Properties of Hybrid Systems with K-Liveness -- Games and Synthesis -- Safraless Synthesis for Epistemic Temporal Specifications -- Minimizing Running Costs in Consumption Systems -- CEGAR for Qualitative Analysis of Probabilistic Systems -- Optimal Guard Synthesis for Memory Safety -- Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion -- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications -- Solving Games without Controllable Predecessor -- G4LTL-ST: Automatic Generation of PLC Programs -- Concurrency -- Automatic Atomicity Verification for Clients of Concurrent Data Structures -- Regression-Free Synthesis for Concurrency -- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization -- An SMT-Based Approach to Coverability Analysis -- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes -- SMT and Theorem Proving -- Monadic Decomposition -- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions -- Bit-Vector Rewriting with Automatic Rule Generation -- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors -- AVATAR: The Architecture for First-Order Theorem Provers -- Automating Separation Logic with Trees and Data -- A Nonlinear Real Arithmetic Fragment -- Yices 2.2 -- Bounds and Termination -- A Simpleand Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis -- Symbolic Resource Bound Inference for Functional Programs -- Proving Non-termination Using Max-SMT -- Termination Analysis by Learning Terminating Programs -- Causal Termination of Multi-threaded Programs -- Abstraction -- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR) -- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction -- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. |
| Record Nr. | UNINA-9910484370003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of Model Checking / / edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem
| Handbook of Model Checking / / edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XXIV, 1210 p. 220 illus., 6 illus. in color.) |
| Disciplina | 004.0151 |
| Soggetto topico |
Computers
Software engineering Logic, Symbolic and mathematical Computer science—Mathematics Computer software—Reusability Quality control Reliability Industrial safety Theory of Computation Software Engineering/Programming and Operating Systems Mathematical Logic and Foundations Mathematics of Computing Performance and Reliability Quality Control, Reliability, Safety and Risk |
| ISBN |
9783319105758
3319105752 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction to Model Checking -- Temporal Logic and Fair Discrete Systems -- Modeling for Verification -- Automata Theory and Model Checking -- Explicit-State Model Checking -- Partial-Order Reduction -- Binary Decision Diagrams -- BDD-Based Symbolic Model Checking -- Propositional SAT Solving -- SAT-Based Model Checking -- Satisfiability Modulo Theories -- Compositional Reasoning -- Abstraction and Abstraction Refinement -- Interpolation and Model Checking -- Predicate Abstraction for Program Verification -- Combining Model Checking and Data-Flow Analysis -- Model Checking Procedural Programs -- Model Checking Concurrent Programs -- Combining Model Checking and Testing -- Combining Model Checking and Deduction -- Model Checking Parameterized Systems -- Model Checking Security Protocols -- Transfer of Model Checking to Industrial Practice -- Functional Specification of Hardware via Temporal Logic -- Symbolic Trajectory Evaluation -- The mu-calculus and Model Checking -- Graph Games and Reactive Synthesis -- Model Checking Probabilistic Systems -- Model Checking Real-Time Systems -- Verification of Hybrid Systems -- Symbolic Model Checking in Non-Boolean Domains -- Process Algebra and Model Checking. |
| Record Nr. | UNINA-9910299458803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Hardware and Software: Verification and Testing [[electronic resource] ] : 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings / / edited by Roderick Bloem, Eli Arbel
| Hardware and Software: Verification and Testing [[electronic resource] ] : 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings / / edited by Roderick Bloem, Eli Arbel |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVI, 211 p. 60 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Mathematical logic Artificial intelligence Computer communication systems Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages Artificial Intelligence Computer Communication Networks |
| ISBN | 3-319-49052-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Practice in verification -- Practice in testing -- Future directions of testing and verification for hardware, software, and complex hybrid systems. |
| Record Nr. | UNISA-996465611903316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Hardware and Software: Verification and Testing : 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings / / edited by Roderick Bloem, Eli Arbel
| Hardware and Software: Verification and Testing : 12th International Haifa Verification Conference, HVC 2016, Haifa, Israel, November 14-17, 2016, Proceedings / / edited by Roderick Bloem, Eli Arbel |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVI, 211 p. 60 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer science Compilers (Computer programs) Machine theory Artificial intelligence Computer networks Software Engineering Computer Science Logic and Foundations of Programming Compilers and Interpreters Formal Languages and Automata Theory Artificial Intelligence Computer Communication Networks |
| ISBN | 3-319-49052-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Practice in verification -- Practice in testing -- Future directions of testing and verification for hardware, software, and complex hybrid systems. |
| Record Nr. | UNINA-9910483592903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Trusted Systems [[electronic resource] ] : 5th International Conference, INTRUST 2013, Graz, Austria, December 4-5, 2013, Proceedings / / edited by Roderick Bloem, Peter Lipp
| Trusted Systems [[electronic resource] ] : 5th International Conference, INTRUST 2013, Graz, Austria, December 4-5, 2013, Proceedings / / edited by Roderick Bloem, Peter Lipp |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 103 p. 18 illus.) |
| Disciplina | 005.8 |
| Collana | Security and Cryptology |
| Soggetto topico |
Computer security
Data encryption (Computer science) Operating systems (Computers) Systems and Data Security Cryptology Operating Systems |
| ISBN | 3-319-03491-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Hardware-Based Security and Applications -- Para-Virtualizing the Trusted Platform Module: An Enterprise -- Framework Based on Version 2.0 Specification -- The PACE|CA Protocol for Machine Readable Travel Documents -- A Spatial Majority Voting Technique to Reduce Error Rate of Physically Unclonable Functions -- Access Control, Integrity and Policy Enforcement. |
| Record Nr. | UNISA-996465392803316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Trusted Systems : 5th International Conference, INTRUST 2013, Graz, Austria, December 4-5, 2013, Proceedings / / edited by Roderick Bloem, Peter Lipp
| Trusted Systems : 5th International Conference, INTRUST 2013, Graz, Austria, December 4-5, 2013, Proceedings / / edited by Roderick Bloem, Peter Lipp |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 103 p. 18 illus.) |
| Disciplina | 005.8 |
| Collana | Security and Cryptology |
| Soggetto topico |
Data protection
Cryptography Data encryption (Computer science) Operating systems (Computers) Data and Information Security Cryptology Operating Systems |
| ISBN | 3-319-03491-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Hardware-Based Security and Applications -- Para-Virtualizing the Trusted Platform Module: An Enterprise -- Framework Based on Version 2.0 Specification -- The PACE/CA Protocol for Machine Readable Travel Documents -- A Spatial Majority Voting Technique to Reduce Error Rate of Physically Unclonable Functions -- Access Control, Integrity and Policy Enforcement. |
| Record Nr. | UNINA-9910484865703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||