Borrow it
Coverart for item
The Resource Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)

Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)

Creator
Contributor
Summary
This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6-10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis methods for software and hardware systems. The conference covered the spectrum from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 123 submissions for regular papers and 32 submissions for tool papers. Ofthesesubmissions, theProgramCommitteeselected32regularpapers and 16 tool papers, which formed the technical program of the conference. The conference had three invited talks, by Bob Bentley (Intel), Bud Mishra (NYU), and George C. Necula (UC Berkeley). The conference was preceded by a tutorial day, with two tutorials: - Automated Abstraction Re?nement, by Thomas Ball (Microsoft) and Ken McMillan (Cadence); and - Theory and Practice of Decision Procedures for Combinations of (First- Order) Theories, by Clark Barrett (NYU) and Cesare Tinelli (U Iowa). CAV 2005 had six a?liated workshops: - BMC 2005: 3rd Int. Workshop on Bounded Model Checking; - FATES 2005: 5th Workshop on Formal Approaches to Testing Software; - GDV 2005: 2nd Workshop on Games in Design and Veri?cation; - PDPAR 2005: 3rd Workshop on Pragmatics of Decision Procedures in - tomated Reasoning; - RV 2005: 5th Workshop on Runtime Veri?cation; and - SoftMC 2005: 3rd Workshop on Software Model Checking
Language
eng
Work
Publication
Extent
1 online resource (xv, 564 pages)
Contents
  • 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
Isbn
9783540316862
Instance
Label
Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings
Title
Computer aided verification
Title remainder
17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings
Statement of responsibility
Kousha Etessami, Sriram K. Rajamani (eds.)
Title variation
CAV 2005
Creator
Contributor
Subject
Genre
Language
eng
Summary
This volume contains the proceedings of the International Conference on Computer Aided Veri?cation (CAV), held in Edinburgh, Scotland, July 6-10, 2005. CAV 2005 was the seventeenth in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal an- ysis methods for software and hardware systems. The conference covered the spectrum from theoretical results to concrete applications, with an emphasis on practical veri?cation tools and the algorithms and techniques that are needed for their implementation. We received 123 submissions for regular papers and 32 submissions for tool papers. Ofthesesubmissions, theProgramCommitteeselected32regularpapers and 16 tool papers, which formed the technical program of the conference. The conference had three invited talks, by Bob Bentley (Intel), Bud Mishra (NYU), and George C. Necula (UC Berkeley). The conference was preceded by a tutorial day, with two tutorials: - Automated Abstraction Re?nement, by Thomas Ball (Microsoft) and Ken McMillan (Cadence); and - Theory and Practice of Decision Procedures for Combinations of (First- Order) Theories, by Clark Barrett (NYU) and Cesare Tinelli (U Iowa). CAV 2005 had six a?liated workshops: - BMC 2005: 3rd Int. Workshop on Bounded Model Checking; - FATES 2005: 5th Workshop on Formal Approaches to Testing Software; - GDV 2005: 2nd Workshop on Games in Design and Veri?cation; - PDPAR 2005: 3rd Workshop on Pragmatics of Decision Procedures in - tomated Reasoning; - RV 2005: 5th Workshop on Runtime Veri?cation; and - SoftMC 2005: 3rd Workshop on Software Model Checking
Member of
Cataloging source
GW5XE
Dewey number
004.24
Illustrations
illustrations
Index
index present
LC call number
QA76.76.V47
LC item number
C38 2005
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2005
http://bibfra.me/vocab/lite/meetingName
CAV (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1970-
http://library.link/vocab/relatedWorkOrContributorName
  • Etessami, Kousha
  • Rajamani, Sriram K.
Series statement
Lecture notes in computer science,
Series volume
3576
http://library.link/vocab/subjectName
  • Computer software
  • Integrated circuits
  • Electronic digital computers
  • Informatique
  • Computer software
  • Electronic digital computers
  • Integrated circuits
  • Vérification de logiciels
  • Circuit intégré
  • Vérification formelle
  • Ordinateur
Label
Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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
Control code
262680942
Dimensions
unknown
Extent
1 online resource (xv, 564 pages)
Form of item
online
Isbn
9783540316862
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-27231-1
Specific material designation
remote
System control number
(OCoLC)262680942
Label
Computer aided verification : 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005 : proceedings, Kousha Etessami, Sriram K. Rajamani (eds.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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
Control code
262680942
Dimensions
unknown
Extent
1 online resource (xv, 564 pages)
Form of item
online
Isbn
9783540316862
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-540-27231-1
Specific material designation
remote
System control number
(OCoLC)262680942

Subject

Genre

Member of

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125

Library Links

Structured data from the Bibframe namespace is licensed under the Creative Commons Attribution 4.0 International License by University of Missouri Libraries. Additional terms may apply to data associated with third party namespaces.
Processing Feedback ...