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

Preview

Export

ChatGPT Discussion

AI Recommended Related Books