서브메뉴
검색
Computer Aided Verification(LNCS2102)
Computer Aided Verification(LNCS2102)
Detailed Information
- 자료유형
- 단행본
- ISBN
- 3-540-42345-1
- UDC
- 681.3.09
- DDC
- 600-23
- 청구기호
- 600 G356c
- 서명/저자
- Computer Aided Verification(LNCS2102) / Gerard Berry, Hubert Comon, Alain Finkel 저.
- 발행사항
- 미국 : Springer-Verlag, 2001
- 형태사항
- 520p. ; 24cm
- 내용주기
- 완전내용Invited Talk완전내용Software Documenttion and The Verification Process부분내용1완전내용Model Checking and Theorem Proving완전내용Certifying Model Checkers부분내용2완전내용Formalizing a JVML Verifier for Intitalization in a Theorem Prover부분내용14완전내용Automated Inductive Verification of Parmeterized Protocols부분내용25완전내용Automata Techniques완전내용Efficient Model Checking via Buchi Tableau Automata부분내용38완전내용Fast LTL to Buchi Automata Tanslation부분내용53완전내용A Practial Approach to Coverage in Model Checking부분내용6600완전내용Verification Core Technology11완전내용A Fast Binsimulation Algorithm부분내용7922완전내용Symmetry and Reduced Symmetry in Model Checking부분내용9133완전내용Transformation-Based Verification Using Generalized Retiming부분내용10444완전내용BDD and Decision Procedures55완전내용Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions부분내용11866완전내용CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negrtive Elimination부분내용13177완전내용Finite Instantiations in Equibalence Logic with Uninterpreted Functions부분내용14488완전내용Abstraction and Refinement99완전내용Model-Checking With Formula-Dependent Abstract Models부분내용15500완전내용Verifying Network Protocol Implementations by Symbolic Refinement Checking부분내용16911완전내용Automatic Abstraction for Verification of Timed Circuits and Systems부분내용18222완전내용Combinations33완전내용Automated Verification of a Randomized Distributed Concensus Protocol Using Cadence SMV and PRISM부분내용19444완전내용Analysis of Recursive State Machines부분내용20755완전내용Prameterized Verfication with Automatically Computed Inductive Assertions부분내용22166완전내용Tool Presemtations: Rewriting and Theorem-Proving Techniques77완전내용EVC: A Validity Checker for the Logic of Equality With Uniterpreted Functionsand Memories, Exploiting Positive Equality, and Conservative Transformations부분내용23588완전내용AGVI--Automatic Generation, Verifcation, and Implementation of Security Protocols부분내용24199완전내용ICS: Integrated Canonizer and Solver부분내용24600완전내용μCLR: A Toolset for Analysing Algebraic Specfications부분내용25011완전내용Truth/SLC--A Parallel Verification Platform For Concurrent Systems부분내용25522완전내용The SLAM Toolkit부분내용26033완전내용Invited Talk44완전내용Java Bytecode Verification: An Overview부분내용26555완전내용Infinite Syate Systems66완전내용ITerating Transducers부분내용28677완전내용Attacking Symbolic State Explosion부분내용29888완전내용A Unifying Model Checking Approach for Safety Properies of Parameterized Sysetms부분내용31199완전내용A BDD-Based Model Checker for Recursive Programs부분내용32400완전내용Temproal Logics and Verification11완전내용Model Checking the World Wide Web부분내용33722완전내용Distributed Symbolic Model Checking For μ-Calculus부분내용35033완전내용Tool Presentations: Model-Checking and Automata Techniques44완전내용The Temporal Logic Sugar부분내용36355완전내용TREX: A Tool for Reachability Analysis of Complex Systems부분내용36866완전내용BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstaction부분내용37377완전내용SDLcheck: a Model Checking Tool부분내용37888완전내용EASN: Interating ASN. 1 and Model Checking부분내용38299완전내용RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams부분내용38700완전내용TAXYS: a Tool for the Development and Verification of Real-Time Embedded Systems부분내용39111완전내용Microprocessor Verification, Cache Coherence22완전내용Microarchitecture Verification By Compositional Model Checking부분내용39633완전내용Rewriring for Symbolic Execution of State Machine Models부분내용41144완전내용Using Timestamping and History Variables to Verify Sequential Consistency부분내용41155완전내용SAT, BDDs, and Applications66완전내용Benefits of Bounded Model Checking at an Industrial Setting부분내용43677완전내용Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers부분내용45488완전내용Towards Effcint Verification of Arithmetic Algorithms over Galois Fields GF(2m)부분내용46599완전내용Timed Automata00완전내용Job-Shop Scheduling Using Timed Automata부분내용47811완전내용As Cheap ad Possible: Efficient Cost-Optimal Reachability foir Priced Timed Automata부분내용49322완전내용Binary reachability Analysis of Pushdown Timed Automata with Dense Colcks부분내용50633완전내용Author Index부분내용51944
- 가격
- ￦65390
- Control Number
- gtec:8237
MARC
008021018s2001 us 000 eng■020 ▼a3-540-42345-1
■0801 ▼a681.3.09
■082 ▼a600▼223
■090 ▼a600▼bG356c
■1000 ▼aFinkel, Gerard Berry, Hubert Comon, Alain
■24510▼aComputer Aided Verification(LNCS2102)▼dGerard Berry, Hubert Comon, Alain Finkel 저.
■260 ▼a미국▼bSpringer-Verlag▼c2001
■300 ▼a520p.▼c24cm
■505 ▼aInvited Talk▼aSoftware Documenttion and The Verification Process▼c1▼aModel Checking and Theorem Proving▼aCertifying Model Checkers▼c2▼aFormalizing a JVML Verifier for Intitalization in a Theorem Prover▼c14▼aAutomated Inductive Verification of Parmeterized Protocols▼c25▼aAutomata Techniques▼aEfficient Model Checking via Buchi Tableau Automata▼c38▼aFast LTL to Buchi Automata Tanslation▼c53▼aA Practial Approach to Coverage in Model Checking▼c6600▼aVerification Core Technology11▼aA Fast Binsimulation Algorithm▼c7922▼aSymmetry and Reduced Symmetry in Model Checking▼c9133▼aTransformation-Based Verification Using Generalized Retiming▼c10444▼aBDD and Decision Procedures55▼aMeta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions▼c11866▼aCLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negrtive Elimination▼c13177▼aFinite Instantiations in Equibalence Logic with Uninterpreted Functions▼c14488▼aAbstraction and Refinement99▼aModel-Checking With Formula-Dependent Abstract Models▼c15500▼aVerifying Network Protocol Implementations by Symbolic Refinement Checking▼c16911▼aAutomatic Abstraction for Verification of Timed Circuits and Systems▼c18222▼aCombinations33▼aAutomated Verification of a Randomized Distributed Concensus Protocol Using Cadence SMV and PRISM▼c19444▼aAnalysis of Recursive State Machines▼c20755▼aPrameterized Verfication with Automatically Computed Inductive Assertions▼c22166▼aTool Presemtations: Rewriting and Theorem-Proving Techniques77▼aEVC: A Validity Checker for the Logic of Equality With Uniterpreted Functionsand Memories, Exploiting Positive Equality, and Conservative Transformations▼c23588▼aAGVI--Automatic Generation, Verifcation, and Implementation of Security Protocols▼c24199▼aICS: Integrated Canonizer and Solver▼c24600▼aμCLR: A Toolset for Analysing Algebraic Specfications▼c25011▼aTruth/SLC--A Parallel Verification Platform For Concurrent Systems▼c25522▼aThe SLAM Toolkit▼c26033▼aInvited Talk44▼aJava Bytecode Verification: An Overview▼c26555▼aInfinite Syate Systems66▼aITerating Transducers▼c28677▼aAttacking Symbolic State Explosion▼c29888▼aA Unifying Model Checking Approach for Safety Properies of Parameterized Sysetms▼c31199▼aA BDD-Based Model Checker for Recursive Programs▼c32400▼aTemproal Logics and Verification11▼aModel Checking the World Wide Web▼c33722▼aDistributed Symbolic Model Checking For μ-Calculus▼c35033▼aTool Presentations: Model-Checking and Automata Techniques44▼aThe Temporal Logic Sugar▼c36355▼aTREX: A Tool for Reachability Analysis of Complex Systems▼c36866▼aBOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstaction▼c37377▼aSDLcheck: a Model Checking Tool▼c37888▼aEASN: Interating ASN. 1 and Model Checking▼c38299▼aRTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams▼c38700▼aTAXYS: a Tool for the Development and Verification of Real-Time Embedded Systems▼c39111▼aMicroprocessor Verification, Cache Coherence22▼aMicroarchitecture Verification By Compositional Model Checking▼c39633▼aRewriring for Symbolic Execution of State Machine Models▼c41144▼aUsing Timestamping and History Variables to Verify Sequential Consistency▼c41155▼aSAT, BDDs, and Applications66▼aBenefits of Bounded Model Checking at an Industrial Setting▼c43677▼aFinding Bugs in an Alpha Microprocessor Using Satisfiability Solvers▼c45488▼aTowards Effcint Verification of Arithmetic Algorithms over Galois Fields GF(2m)▼c46599▼aTimed Automata00▼aJob-Shop Scheduling Using Timed Automata▼c47811▼aAs Cheap ad Possible: Efficient Cost-Optimal Reachability foir Priced Timed Automata▼c49322▼aBinary reachability Analysis of Pushdown Timed Automata with Dense Colcks▼c50633▼aAuthor Index▼c51944
■9500 ▼b￦65390
