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] ] : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I / / edited by Hana Chockler, Georg Weissenbacher
| Computer Aided Verification [[electronic resource] ] : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I / / edited by Hana Chockler, Georg Weissenbacher |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIX, 703 p. 146 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Artificial intelligence Machine theory Algorithms Computer simulation Computer Science Logic and Foundations of Programming Software Engineering Artificial Intelligence Formal Languages and Automata Theory Computer Modelling |
| ISBN | 3-319-96145-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466443303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I / / edited by Hana Chockler, Georg Weissenbacher
| Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I / / edited by Hana Chockler, Georg Weissenbacher |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIX, 703 p. 146 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Artificial intelligence Machine theory Algorithms Computer simulation Computer Science Logic and Foundations of Programming Software Engineering Artificial Intelligence Formal Languages and Automata Theory Computer Modelling |
| ISBN | 3-319-96145-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349421703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II / / edited by Hana Chockler, Georg Weissenbacher
| Computer Aided Verification : 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II / / edited by Hana Chockler, Georg Weissenbacher |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XX, 545 p. 106 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Artificial intelligence Machine theory Algorithms Computer simulation Computer Science Logic and Foundations of Programming Software Engineering Artificial Intelligence Formal Languages and Automata Theory Computer Modelling |
| ISBN | 3-319-96142-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349421803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
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 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. | UNINA-9910484370003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings / / edited by Madhusudan Parthasarathy, Sanjit A. Seshia
| Computer Aided Verification [[electronic resource] ] : 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings / / edited by Madhusudan Parthasarathy, Sanjit A. Seshia |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XVI, 789 p. 192 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Artificial intelligence Computers, Special purpose Computers Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence Special Purpose and Application-Based Systems Computer Hardware |
| ISBN | 3-642-31424-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465526003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings / / edited by Ganesh Gopalakrishnan, Shaz Qadeer
| Computer Aided Verification [[electronic resource] ] : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings / / edited by Ganesh Gopalakrishnan, Shaz Qadeer |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XV, 763 p. 180 illus., 46 illus. in color.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Compilers (Computer programs) Machine theory Computer programming Artificial intelligence Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters Formal Languages and Automata Theory Programming Techniques Artificial Intelligence |
| ISBN | 3-642-22110-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465714203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson
| Computer Aided Verification [[electronic resource] ] : 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / / edited by Tayssir Touili, Byron Cook, Paul Jackson |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (XVI, 676 p. 169 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Compilers (Computer programs) Machine theory Artificial intelligence Computer networks Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters Formal Languages and Automata Theory Artificial Intelligence Computer Communication Networks |
| ISBN |
1-280-38785-8
9786613565778 3-642-14295-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Policy Monitoring in First-Order Temporal Logic -- Retrofitting Legacy Code for Security -- Quantitative Information Flow: From Theory to Practice? -- Memory Management in Concurrent Algorithms -- Invited Tutorials -- ABC: An Academic Industrial-Strength Verification Tool -- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code -- Constraint Solving for Program Verification: Theory and Practice by Example -- Session 1. Software Model Checking -- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data -- Termination Analysis with Compositional Transition Invariants -- Lazy Annotation for Program Testing and Verification -- The Static Driver Verifier Research Platform -- Dsolve: Safety Verification via Liquid Types -- Contessa: Concurrency Testing Augmented with Symbolic Analysis -- Session 2. Model Checking and Automata -- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing -- Efficient Emptiness Check for Timed Büchi Automata -- Session 3. Tools -- Merit: An Interpolating Model-Checker -- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems -- Jtlv: A Framework for Developing Verification Algorithms -- Petruchio: From Dynamic Networks to Nets -- Session 4. Counter and Hybrid Systems Verification -- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems -- Safety Verification for Probabilistic Hybrid Systems -- A Logical Product Approach to Zonotope Intersection -- Fast Acceleration of Ultimately Periodic Relations -- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks -- Session 5. Memory Consistency -- Fences in Weak Memory Models -- Generating Litmus Tests for Contrasting Memory Consistency Models -- Session 6. Verification of Hardware and Low Level Code -- Directed Proof Generation for Machine Code -- Verifying Low-Level Implementations of High-Level Datatypes -- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics -- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification -- Session 7. Tools -- LTSmin: Distributed and Symbolic Reachability -- libalf: The Automata Learning Framework -- Session 8. Synthesis -- Symbolic Bounded Synthesis -- Measuring and Synthesizing Systems in Probabilistic Environments -- Achieving Distributed Control through Model Checking -- Robustness in the Presence of Liveness -- RATSY – A New Requirements Analysis Tool with Synthesis -- Comfusy: A Tool for Complete Functional Synthesis -- Session 9. Concurrent Program Verification I -- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs -- Automatically Proving Linearizability -- Model Checking of Linearizability of Concurrent List Implementations -- Local Verification of Global Invariants in Concurrent Programs -- Abstract Analysis of Symbolic Executions -- Session 10. Compositional Reasoning -- Automated Assume-Guarantee Reasoning through Implicit Learning -- Learning Component Interfaces with May and Must Abstractions -- A Dash of Fairness for Compositional Reasoning -- SPLIT: A Compositional LTL Verifier -- Session 11. Tools -- A Model Checker for AADL -- PESSOA: A Tool for Embedded Controller Synthesis -- Session 12. Decision Procedures -- On Array Theory of Bounded Elements -- Quantifier Elimination by Lazy Model Enumeration -- Session 13. Concurrent Program Verification II -- Bounded Underapproximations -- Global Reachability in Bounded Phase Multi-stack Pushdown Systems -- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces -- Dynamic Cutoff Detection in Parameterized Concurrent Programs -- Session 14. Tools -- PARAM: A Model Checker for Parametric Markov Models -- Gist: A Solver for Probabilistic Games -- A NuSMV Extension for Graded-CTL Model Checking. |
| Record Nr. | UNISA-996465781203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer aided verification : 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 : proceedings / / Tayssir Touili, Byron Cook, Paul Jackson (eds.)
| Computer aided verification : 22nd international conference, CAV 2010, Edinburgh, UK, July 15-19, 2010 : proceedings / / Tayssir Touili, Byron Cook, Paul Jackson (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | New York, : Springer, 2010 |
| Descrizione fisica | 1 online resource (XVI, 676 p. 169 illus.) |
| Disciplina | 005.1015113 |
| Altri autori (Persone) |
TouiliTayssir
CookByron JacksonPaul |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Computer software - Verification
Integrated circuits - Verification |
| ISBN |
1-280-38785-8
9786613565778 3-642-14295-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Policy Monitoring in First-Order Temporal Logic -- Retrofitting Legacy Code for Security -- Quantitative Information Flow: From Theory to Practice? -- Memory Management in Concurrent Algorithms -- Invited Tutorials -- ABC: An Academic Industrial-Strength Verification Tool -- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code -- Constraint Solving for Program Verification: Theory and Practice by Example -- Session 1. Software Model Checking -- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data -- Termination Analysis with Compositional Transition Invariants -- Lazy Annotation for Program Testing and Verification -- The Static Driver Verifier Research Platform -- Dsolve: Safety Verification via Liquid Types -- Contessa: Concurrency Testing Augmented with Symbolic Analysis -- Session 2. Model Checking and Automata -- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing -- Efficient Emptiness Check for Timed Büchi Automata -- Session 3. Tools -- Merit: An Interpolating Model-Checker -- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems -- Jtlv: A Framework for Developing Verification Algorithms -- Petruchio: From Dynamic Networks to Nets -- Session 4. Counter and Hybrid Systems Verification -- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems -- Safety Verification for Probabilistic Hybrid Systems -- A Logical Product Approach to Zonotope Intersection -- Fast Acceleration of Ultimately Periodic Relations -- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks -- Session 5. Memory Consistency -- Fences in Weak Memory Models -- Generating Litmus Tests for Contrasting Memory Consistency Models -- Session 6. Verification of Hardware and Low Level Code -- Directed Proof Generation for Machine Code -- Verifying Low-Level Implementations of High-Level Datatypes -- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics -- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification -- Session 7. Tools -- LTSmin: Distributed and Symbolic Reachability -- libalf: The Automata Learning Framework -- Session 8. Synthesis -- Symbolic Bounded Synthesis -- Measuring and Synthesizing Systems in Probabilistic Environments -- Achieving Distributed Control through Model Checking -- Robustness in the Presence of Liveness -- RATSY – A New Requirements Analysis Tool with Synthesis -- Comfusy: A Tool for Complete Functional Synthesis -- Session 9. Concurrent Program Verification I -- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs -- Automatically Proving Linearizability -- Model Checking of Linearizability of Concurrent List Implementations -- Local Verification of Global Invariants in Concurrent Programs -- Abstract Analysis of Symbolic Executions -- Session 10. Compositional Reasoning -- Automated Assume-Guarantee Reasoning through Implicit Learning -- Learning Component Interfaces with May and Must Abstractions -- A Dash of Fairness for Compositional Reasoning -- SPLIT: A Compositional LTL Verifier -- Session 11. Tools -- A Model Checker for AADL -- PESSOA: A Tool for Embedded Controller Synthesis -- Session 12. Decision Procedures -- On Array Theory of Bounded Elements -- Quantifier Elimination by Lazy Model Enumeration -- Session 13. Concurrent Program Verification II -- Bounded Underapproximations -- Global Reachability in Bounded Phase Multi-stack Pushdown Systems -- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces -- Dynamic Cutoff Detection in Parameterized Concurrent Programs -- Session 14. Tools -- PARAM: A Model Checker for Parametric Markov Models -- Gist: A Solver for Probabilistic Games -- A NuSMV Extension for Graded-CTL Model Checking. |
| Altri titoli varianti | CAV 2010 |
| Record Nr. | UNINA-9910482958903321 |
| New York, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings / / edited by Kousha Etessami, Sriram K. Rajamani
| Computer Aided Verification [[electronic resource] ] : 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings / / edited by Kousha Etessami, Sriram K. Rajamani |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XVI, 568 p.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Artificial intelligence Logic design Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence Logic Design |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Randomized Algorithms for Program Analysis and Verification -- Validating a Modern Microprocessor -- Algorithmic Algebraic Model Checking I: Challenges from Systems Biology -- Tools Competition -- SMT-COMP: Satisfiability Modulo Theories Competition -- Abstraction and Refinement -- Predicate Abstraction via Symbolic Decision Procedures -- Interpolant-Based Transition Relation Approximation -- Concrete Model Checking with Abstract Matching and Refinement -- Abstraction for Falsification -- Bounded Model Checking -- Bounded Model Checking of Concurrent Programs -- Incremental and Complete Bounded Model Checking for Full PLTL -- Abstraction Refinement for Bounded Model Checking -- Symmetry Reduction in SAT-Based Model Checking -- Tool Papers I -- Saturn: A SAT-Based Tool for Bug Detection -- JVer: A Java Verifier -- Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework -- Wolf – Bug Hunter for Concurrent Software Using Formal Methods -- Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ -- The ComFoRT Reasoning Framework -- Verification of Hardware, Microcode, and Synchronous Systems -- Formal Verification of Pentium ® 4 Components with Symbolic Simulation and Inductive Invariants -- Formal Verification of Backward Compatibility of Microcode -- Compositional Analysis of Floating-Point Linear Numerical Filters -- Syntax-Driven Reachable State Space Construction of Synchronous Reactive Programs -- Games and Probabilistic Verification -- Program Repair as a Game -- Improved Probabilistic Models for 802.11 Protocol Verification -- Probabilistic Verification for “Black-Box” Systems -- On Statistical Model Checking of Stochastic Systems -- Tool Papers II -- The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications -- The Orchids Intrusion Detection Tool -- TVOC: A Translation Validator for Optimizing Compilers -- Cogent: Accurate Theorem Proving for Program Verification -- F-Soft: Software Verification Platform -- Decision Procedures and Applications -- Yet Another Decision Procedure for Equality Logic -- DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic -- Efficient Satisfiability Modulo Theories via Delayed Theory Combination -- Automata and Transition Systems -- Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking -- Efficient Monitoring of ?-Languages -- Verification of Tree Updates for Optimization -- Expand, Enlarge and Check... Made Efficient -- Tool Papers III -- IIV: An Invisible Invariant Verifier -- Action Language Verifier, Extended -- Romeo: A Tool for Analyzing Time Petri Nets -- TRANSYT:A Tool for the Verification of Asynchronous Concurrent Systems -- Ymer: A Statistical Model Checker -- Program Analysis and Verification I -- Extended Weighted Pushdown Systems -- Incremental Algorithms for Inter-procedural Analysis of Safety Properties -- A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs -- Program Analysis and Verification II -- Data Structure Specifications via Local Equality Axioms -- Linear Ranking with Reachability -- Reasoning About Threads Communicating via Locks -- Applications of Learning -- Abstraction Refinement via Inductive Learning -- Automated Assume-Guarantee Reasoning for Simulation Conformance -- Symbolic Compositional Verification by Learning Assumptions. |
| Record Nr. | UNISA-996465831703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
