Skip to content
Library Home
Start Over
Research Databases
E-Journals
Course Reserves
Library Home
Login to library account
English
Deutsch
Español
Français
Italiano
日本語
Nederlands
Português
Português (Brasil)
中文(简体)
中文(繁體)
Türkçe
עברית
Gaeilge
Cymraeg
Ελληνικά
Català
Euskara
Русский
Čeština
Suomi
Svenska
polski
Dansk
slovenščina
اللغة العربية
বাংলা
Galego
Tiếng Việt
Hrvatski
हिंदी
Հայերէն
Українська
Language
Library Catalog
All Fields
Title
Author
Subject
Call Number
ISBN/ISSN
Find
Advanced Search
|
Browse
|
Search Tips
Computer Aided Verification
Cite this
Text this
Email this
Print
Export Record
Export to RefWorks
Export to EndNoteWeb
Export to EndNote
Save to List
Permanent link
Computer Aided Verification 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings / edited by Tayssir Touili, Byron Cook, Paul Jackson.
Saved in:
Bibliographic Details
Corporate Author:
SpringerLink (Online service)
Other Authors:
Touili, Tayssir
(Editor)
,
Cook, Byron
(Editor)
,
Jackson, Paul
(Editor)
Format:
eBook
Language:
English
Published:
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2010.
Edition:
1st ed. 2010.
Series:
Theoretical Computer Science and General Issues ;
6174
Springer eBook Collection.
Subjects:
Computer logic.
Software engineering.
Programming languages (Electronic computers).
Mathematical logic.
Artificial intelligence.
Computer communication systems.
Electronic resources (E-books)
Online Access:
Click to view e-book
Holy Cross Note:
Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Holdings
Description
Table of Contents
Similar Items
Staff View
Table of Contents:
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.
Similar Items
Computer Aided Verification 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings
Published: (2011)
Computer Aided Verification 20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008, Proceedings
Published: (2008)
Computer Aided Verification 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings
Published: (2005)
Computer Aided Verification 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings
Published: (2007)
Computer Aided Verification 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings
Published: (2004)