Computer Aided Verification 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings / edited by Rajeev Alur, Doron A. Peled.

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Alur, Rajeev (Editor), Peled, Doron A. (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.
Edition:1st ed. 2004.
Series:Lecture Notes in Computer Science, 3114
Springer eBook Collection.
Subjects:
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.

MARC

LEADER 00000nam a22000005i 4500
001 b3192949
003 MWH
005 20191026121739.0
007 cr nn 008mamaa
008 121227s2004 gw | s |||| 0|eng d
020 |a 9783540278139 
024 7 |a 10.1007/b98490  |2 doi 
035 |a (DE-He213)978-3-540-27813-9 
050 4 |a E-Book 
072 7 |a UY  |2 bicssc 
072 7 |a COM014000  |2 bisacsh 
072 7 |a UY  |2 thema 
072 7 |a UYA  |2 thema 
245 1 0 |a Computer Aided Verification  |h [electronic resource] :  |b 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings /  |c edited by Rajeev Alur, Doron A. Peled. 
250 |a 1st ed. 2004. 
264 1 |a Berlin, Heidelberg :  |b Springer Berlin Heidelberg :  |b Imprint: Springer,  |c 2004. 
300 |a XII, 536 p.  |b online resource. 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
347 |a text file  |b PDF  |2 rda 
490 1 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 3114 
490 1 |a Springer eBook Collection 
505 0 |a Rob Tristan Gerth: 1956–2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying ?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification. 
590 |a Loaded electronically. 
590 |a Electronic access restricted to members of the Holy Cross Community. 
650 0 |a Computers. 
650 0 |a Software engineering. 
650 0 |a Logic design. 
650 0 |a Computer logic. 
650 0 |a Mathematical logic. 
650 0 |a Artificial intelligence. 
690 |a Electronic resources (E-books) 
700 1 |a Alur, Rajeev.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
700 1 |a Peled, Doron A.  |e editor.  |4 edt  |4 http://id.loc.gov/vocabulary/relators/edt 
710 2 |a SpringerLink (Online service) 
773 0 |t Springer eBooks 
830 0 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 3114 
830 0 |a Springer eBook Collection. 
856 4 0 |u https://holycross.idm.oclc.org/login?auth=cas&url=https://doi.org/10.1007/b98490  |3 Click to view e-book  |t 0 
907 |a .b31929497  |b 04-18-22  |c 02-26-20 
998 |a he  |b 02-26-20  |c m  |d @   |e -  |f eng  |g gw   |h 0  |i 1 
912 |a ZDB-2-SCS 
912 |a ZDB-2-LNC 
912 |a ZDB-2-BAE 
950 |a Computer Science (Springer-11645) 
902 |a springer purchased ebooks 
903 |a SEB-COLL 
945 |f  - -   |g 1  |h 0  |j  - -   |k  - -   |l he   |o -  |p $0.00  |q -  |r -  |s b   |t 38  |u 0  |v 0  |w 0  |x 0  |y .i21061129  |z 02-26-20 
999 f f |i 9ab9668f-fb1a-52fc-a135-5d480e1f439c  |s 8d9df9f4-6eee-50a3-80b8-0e5683270d95  |t 0 
952 f f |p Online  |a College of the Holy Cross  |b Main Campus  |c E-Resources  |d Online  |t 0  |e E-Book  |h Library of Congress classification  |i Elec File