Info
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 | ||
| ||
Formal Methods for Industrial Critical Systems [[electronic resource] ] : 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009, Proceedings / / edited by María Alpuente, Byron Cook, Christophe Joubert
| Formal Methods for Industrial Critical Systems [[electronic resource] ] : 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009, Proceedings / / edited by María Alpuente, Byron Cook, Christophe Joubert |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (X, 213 p.) |
| Disciplina | 005.131 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Special purpose computers Software Engineering/Programming and Operating Systems Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
| ISBN | 3-642-04570-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Attacking Large Industrial Code with Bi-abductive Inference -- On a Uniform Framework for the Definition of Stochastic Process Languages -- Applying a Formal Method in Industry: A 15-Year Trajectory -- What’s in Common between Test, Model Checking, and Decision Procedures? -- Contributed Papers -- Verifying Cryptographic Software Correctness with Respect to Reference Implementations -- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software -- Dynamic State Space Partitioning for External Memory Model Checking -- Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle -- Modeling Concurrent Systems with Shared Resources -- Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs -- Formal Analysis of Non-determinism in Verilog Cell Library Simulation Models -- Preemption Abstraction -- A Rigorous Methodology for Composing Services -- A Certified Implementation on Top of the Java Virtual Machine -- Selected Posters -- Formal Development for Railway Signaling Using Commercial Tools -- Integrated Formal Approach for Qualified Critical Embedded Code Generator -- Visualising Event-B Models with B-Motion Studio -- Behavioural Analysis of an I2C Linux Driver -- Model-Based Testing of Electronic Passports -- Developing a Decision Support Tool for Dam Management with SPIN. |
| Record Nr. | UNISA-996466305203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods for industrial critical systems / / volume editors, Maria Alpuente, Byron Cooker, Christophe Joubert
| Formal methods for industrial critical systems / / volume editors, Maria Alpuente, Byron Cooker, Christophe Joubert |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; London, : Springer, c2009 |
| Descrizione fisica | 1 online resource (X, 213 p.) |
| Disciplina | 005.131 |
| Altri autori (Persone) |
AlpuenteMaria
CookByron JoubertChristophe |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer programs - Verification
Formal methods (Computer science) Software engineering |
| ISBN | 3-642-04570-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Attacking Large Industrial Code with Bi-abductive Inference -- On a Uniform Framework for the Definition of Stochastic Process Languages -- Applying a Formal Method in Industry: A 15-Year Trajectory -- What’s in Common between Test, Model Checking, and Decision Procedures? -- Contributed Papers -- Verifying Cryptographic Software Correctness with Respect to Reference Implementations -- Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software -- Dynamic State Space Partitioning for External Memory Model Checking -- Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle -- Modeling Concurrent Systems with Shared Resources -- Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs -- Formal Analysis of Non-determinism in Verilog Cell Library Simulation Models -- Preemption Abstraction -- A Rigorous Methodology for Composing Services -- A Certified Implementation on Top of the Java Virtual Machine -- Selected Posters -- Formal Development for Railway Signaling Using Commercial Tools -- Integrated Formal Approach for Qualified Critical Embedded Code Generator -- Visualising Event-B Models with B-Motion Studio -- Behavioural Analysis of an I2C Linux Driver -- Model-Based Testing of Electronic Passports -- Developing a Decision Support Tool for Dam Management with SPIN. |
| Record Nr. | UNINA-9910484030903321 |
| Berlin ; ; London, : Springer, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / / edited by Byron Cook, Andreas Podelski
| Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / / edited by Byron Cook, Andreas Podelski |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 395 p.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Compilers (Computer programs) Software Engineering Computer Science Logic and Foundations of Programming Compilers and Interpreters |
| ISBN | 3-540-69738-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk -- DIVINE: DIscovering Variables IN Executables -- Session 1 -- Verifying Compensating Transactions -- Model Checking Nonblocking MPI Programs -- Model Checking Via ?CFA -- Using First-Order Theorem Provers in the Jahob Data Structure Verification System -- Invited Tutorial -- Interpolants and Symbolic Model Checking -- Session 2 -- Shape Analysis of Single-Parent Heaps -- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures -- On Flat Programs with Lists -- Invited Talk -- Automata-Theoretic Model Checking Revisited -- Session 3 -- Language-Based Abstraction Refinement for Hybrid System Verification -- More Precise Partition Abstractions -- The Spotlight Principle -- Lattice Automata -- Invited Tutorial -- Learning Algorithms and Formal Verification (Invited Tutorial) -- Session 4 -- Constructing Specialized Shape Analyses for Uniform Change -- Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning -- Automated Verification of Shape and Size Properties Via Separation Logic -- Invited Talk -- Towards Shape Analysis for Device Drivers -- Session 5 -- An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints -- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes -- Symmetry and Completeness in the Analysis of Parameterized Systems -- Better Under-Approximation of Programs by Hiding Variables -- Invited Tutorial -- The Constraint Database Approach to Software Verification -- Session 6 -- Constraint Solving for Interpolation -- Assertion Checking Unified -- Invariant Synthesis for Combined Theories. |
| Record Nr. | UNISA-996465274003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Verification, Model Checking, and Abstract Interpretation : 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / / edited by Byron Cook, Andreas Podelski
| Verification, Model Checking, and Abstract Interpretation : 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings / / edited by Byron Cook, Andreas Podelski |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 395 p.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Compilers (Computer programs) Software Engineering Computer Science Logic and Foundations of Programming Compilers and Interpreters |
| ISBN | 3-540-69738-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk -- DIVINE: DIscovering Variables IN Executables -- Session 1 -- Verifying Compensating Transactions -- Model Checking Nonblocking MPI Programs -- Model Checking Via ?CFA -- Using First-Order Theorem Provers in the Jahob Data Structure Verification System -- Invited Tutorial -- Interpolants and Symbolic Model Checking -- Session 2 -- Shape Analysis of Single-Parent Heaps -- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures -- On Flat Programs with Lists -- Invited Talk -- Automata-Theoretic Model Checking Revisited -- Session 3 -- Language-Based Abstraction Refinement for Hybrid System Verification -- More Precise Partition Abstractions -- The Spotlight Principle -- Lattice Automata -- Invited Tutorial -- Learning Algorithms and Formal Verification (Invited Tutorial) -- Session 4 -- Constructing Specialized Shape Analyses for Uniform Change -- Maintaining Doubly-Linked List Invariants in Shape Analysis with Local Reasoning -- Automated Verification of Shape and Size Properties Via Separation Logic -- Invited Talk -- Towards Shape Analysis for Device Drivers -- Session 5 -- An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints -- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes -- Symmetry and Completeness in the Analysis of Parameterized Systems -- Better Under-Approximation of Programs by Hiding Variables -- Invited Tutorial -- The Constraint Database Approach to Software Verification -- Session 6 -- Constraint Solving for Interpolation -- Assertion Checking Unified -- Invariant Synthesis for Combined Theories. |
| Record Nr. | UNINA-9910768451103321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||