MARC record from Internet Archive

LEADER: 08626cam 2200841Ia 4500
001 ocn272314660
003 OCoLC
005 20201105023717.0
008 081117s2008 gw a ob 101 0 eng d
006 m o d
007 cr cn|||||||||
040 $aGW5XE$beng$epn$cGW5XE$dCUS$dMNU$dWAU$dIXA$dNUI$dOCLCQ$dCOO$dOCLCQ$dUKMGB$dOCLCO$dOCLCA$dOCLCF$dBEDGE$dOCLCQ$dOCLCO$dYDXCP$dIDEBK$dOCLCQ$dOCL$dOCLCO$dEBLCP$dOCLCQ$dESU$dOCLCQ$dBUF$dUAB$dOCLCQ$dU3W$dAU@$dWYU$dOCLCQ$dLEAUB$dOCLCQ
016 7 $a014665797$2Uk
019 $a246898804$a297448385$a488390733$a495284809$a827361485$a1058177916$a1060688797
020 $a9783540705451
020 $a3540705457
020 $a9783540705437
020 $a3540705430
024 7 $a10.1007/978-3-540-70545-1$2doi
035 $a(OCoLC)272314660$z(OCoLC)246898804$z(OCoLC)297448385$z(OCoLC)488390733$z(OCoLC)495284809$z(OCoLC)827361485$z(OCoLC)1058177916$z(OCoLC)1060688797
037 $a978-3-540-70545-1$bSpringer$nhttp://www.springerlink.com
050 4 $aQA76.76.V47$b.C38 2008eb
072 7 $aQA$2lcco
072 7 $aUM$2bicssc
072 7 $aCOM051000$2bisacsh
082 04 $a005.14$222
111 2 $aCAV (Conference)$n(20th :$d2008 :$cPrinceton, N.J.)
245 10 $aComputer aided verification :$b20th international conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008 : proceedings /$cAarti Gupta, Sharad Malik (eds.).
246 30 $aCAV 2008
260 $aBerlin ;$aNew York :$bSpringer,$c©2008.
300 $a1 online resource (xvii, 558 pages)
336 $atext$btxt$2rdacontent
337 $acomputer$bc$2rdamedia
338 $aonline resource$bcr$2rdacarrier
347 $atext file$bPDF$2rda
490 1 $aLecture notes in computer science,$x0302-9743 ;$v5123
490 1 $aLNCS sublibrary. SL 1, Theoretical computer science and general issues
504 $aIncludes bibliographical references and index.
520 8 $aAnnotation$bThis book constitutes the refereed proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008, held in Princeton, NJ, USA, in July 2008. The 33 revised full papers presented together with 14 tool papers and 2 invited papers and 4 invited tutorials were carefully reviewed and selected from 104 regular paper and 27 tool paper submissions. The papers are organized in topical sections on concurrency, memory consistency, abstraction/refinement, hybrid systems, dynamic verification, modeling and specification formalisms, decision procedures, program verification, program and shape analysis, security and program analysis, hardware verification, model checking, space efficient algorithms, and model checking.
505 0 $aInvited Talks -- Singularity: Designing Better Software (Invited Talk) -- Coping with Outside-the-Box Attacks -- Invited Tutorials -- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial) -- Theorem Proving for Verification (Invited Tutorial) -- Tutorial on Separation Logic (Invited Tutorial) -- Abstract Interpretation with Applications to Timing Validation -- Session 1: Concurrency -- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis -- Monitoring Atomicity in Concurrent Programs -- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings -- A Hybrid Type System for Lock-Freedom of Mobile Processes -- Session 2: Memory Consistency -- Implied Set Closure and Its Application to Memory Consistency Verification -- Effective Program Verification for Relaxed Memory Models -- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses -- Session 3: Abstraction/Refinement -- Automated Assume-Guarantee Reasoning by Abstraction Refinement -- Local Proofs for Linear-Time Properties of Concurrent Programs -- Probabilistic CEGAR -- Session 4: Hybrid Systems -- Computing Differential Invariants of Hybrid Systems as Fixedpoints -- Constraint-Based Approach for Analysis of Hybrid Systems -- Session 5: Tools -- Dynamic Verification -- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems -- FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement -- Session 6: Modeling and Specification Formalisms -- Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems -- Conflict-Tolerant Features -- Ranking Automata and Games for Prioritized Requirements -- Session 7: Decision Procedures -- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations -- Linear Arithmetic with Stars -- Inferring Congruence Equations Using SAT -- Session 8: Tools -- Decision Procedures -- The Barcelogic SMT Solver -- The MathSAT 4 SMT Solver -- CSIsat: Interpolation for LA+EUF -- Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B -- Session 9: Program Verification -- Heap Assumptions on Demand -- Proving Conditional Termination -- Monotonic Abstraction for Programs with Dynamic Memory Heaps -- Enhancing Program Verification with Lemmas -- Session 10: Program and Shape Analysis -- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis -- Scalable Shape Analysis for Systems Code -- Thread Quantification for Concurrent Shape Analysis -- Session 11: Tools -- Security and Program Analysis -- The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols -- The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis -- Jakstab: A Static Analysis Platform for Binaries -- THOR: A Tool for Reasoning about Shape and Arithmetic -- Session 12: Hardware Verification I -- Functional Verification of Power Gated Designs by Compositional Reasoning -- A Practical Approach to Word Level Model Checking of Industrial Netlists -- Session 13: Hardware Verification II -- Validating High-Level Synthesis -- An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths -- Application of Formal Word-Level Analysis to Constrained Random Simulation -- Session 14: Model Checking -- Producing Short Counterexamples Using "Crucial Events" -- Discriminative Model Checking -- Session 15: Space Efficient Algorithms -- Correcting a Space-Efficient Simulation Algorithm -- Semi-external LTL Model Checking -- Session 16: Tools -- Model Checking -- QMC: A Model Checker for Quantum Systems -- T(O)RMC: A Tool for -Regular Model Checking -- Faster Than Uppaal?
546 $aEnglish.
650 0 $aComputer software$xVerification$vCongresses.
650 0 $aElectronic digital computers$xEvaluation$vCongresses.
650 7 $aInformatique.$2eclas
650 7 $aComputer software$xVerification.$2fast$0(OCoLC)fst00872604
650 7 $aElectronic digital computers$xEvaluation.$2fast$0(OCoLC)fst00907149
655 4 $aElectronic books.
655 7 $aConference papers and proceedings.$2fast$0(OCoLC)fst01423772
700 1 $aGupta, Aarti,$cDr.
700 1 $aMalik, Sharad.
776 08 $iPrint version:$aCAV 2008 (2008 : Princeton, N.J.).$tComputer aided verification.$dBerlin ; New York : Springer, ©2008$z9783540705437$w(OCoLC)232569765
830 0 $aLecture notes in computer science ;$v5123.
830 0 $aLNCS sublibrary.$nSL 1,$pTheoretical computer science and general issues.
856 40 $3ProQuest Ebook Central$uhttp://public.ebookcentral.proquest.com/choice/publicfullrecord.aspx?p=3068465
856 40 $3MyiLibrary$uhttp://www.myilibrary.com?id=184984
856 40 $3SpringerLink$uhttps://doi.org/10.1007/978-3-540-70545-1
856 40 $3SpringerLink$uhttp://www.springerlink.com/openurl.asp?genre=book&isbn=978-3-540-70543-7
856 40 $3SpringerLink$uhttp://link.springer.com/10.1007/978-3-540-70545-1
856 40 $3SpringerLink$uhttps://link.springer.com/book/10.1007/978-3-540-70545-1
856 40 $uhttps://0-link-springer-com.pugwash.lib.warwick.ac.uk/10.1007/978-3-540-70545-1$zConnect to Springer e-book
856 40 $uhttp://VH7QX3XE2P.search.serialssolutions.com/?V=1.0&L=VH7QX3XE2P&S=JCs&C=TC0000316848&T=marc&tab=BOOKS$zVIEW FULL TEXT
938 $aProQuest Ebook Central$bEBLB$nEBL3068465
938 $aProQuest MyiLibrary Digital eBook Collection$bIDEB$ncis23927355
938 $aYBP Library Services$bYANK$n3024501
029 1 $aAU@$b000043802018
029 1 $aAU@$b000057998421
029 1 $aAU@$b000058158666
029 1 $aAU@$b000060388417
029 1 $aDKDLA$b820120-katalog:000462153
029 1 $aNLGGC$b384371434
029 1 $aNZ1$b12550567
994 $aZ0$bP4A
948 $hNO HOLDINGS IN P4A - 379 OTHER HOLDINGS