Computer aided verification : 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings
Salvato in:
| Ente Autore: | |
|---|---|
| Altri autori: | , , |
| Natura: | Livre numérique |
| Lingua: | Anglais |
| Pubblicazione: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serie: | Lecture notes in computer science
2102 |
| Soggetti: | |
| Accesso online: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Computer aided verification, 13th International conference, CAV 2001, Paris, France, July 18-22, 2001, proceedings, Gérard Berry, Hubert Comon, Alain Finkel (eds.), 2001, Berlin, Springer, 1 vol. (XIII-520 p.), Lecture notes in computer science, 3-540-42345-1 • Computer Aided Verification, Texte imprimé, 9783662178379 |
| LEADER | 06240nam a22004697a 4500 | ||
|---|---|---|---|
| 001 | 948937 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN15519982X | ||
| 020 | |a 9783540445852 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004.24 | ||
| 082 | |a 004 | ||
| 111 | 2 | |a International conference on computer-aided verification |n (13 |d :2001 |c :Paris). | |
| 245 | 1 | 0 | |a Computer aided verification : |b 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 : proceedings |c [edited by] Gérard Berry, Hubert Comon, Alain Finkel. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 2102 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Invited Talk -- Software Documentation and the Verification Process -- Model Checking and Theorem Proving -- Certifying Model Checkers -- Formalizing a JVML Verifier for Initialization in a Theorem Prover -- Automated Inductive Verification of Parameterized Protocols? -- Automata Techniques -- Efficient Model Checking Via Büchi Tableau Automata? -- Fast LTL to Büchi Automata Translation -- A Practical Approach to Coverage in Model Checking -- Verification Core Technology -- A Fast Bisimulation Algorithm -- Symmetry and Reduced Symmetry in Model Checking? -- Transformation-Based Verification Using Generalized Retiming -- BDD and Decision Procedures -- Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions -- CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination -- Finite Instantiations in Equivalence Logic with Uninterpreted Functions -- Abstraction and Refinement -- Model Checking with Formula-Dependent Abstract Models -- Verifying Network Protocol Implementations by Symbolic Refinement Checking -- Automatic Abstraction for Verification of Timed Circuits and Systems? -- Combinations -- Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM? -- Analysis of Recursive State Machines -- Parameterized Verification with Automatically Computed Inductive Assertions? -- Tool Presentations: Rewriting and Theorem-Proving Techniques -- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations -- AGVI Automatic Generation, Verification, and Implementation of Security Protocols -- ICS: Integrated Canonizer and Solver? -- CRL: A Toolset for Analysing Algebraic Specifications -- Truth/SLC A Parallel Verification Platform for Concurrent Systems -- The SLAM Toolkit -- Invited Talk -- Java Bytecode Verification: An Overview -- Infinite State Systems -- Iterating Transducers -- Attacking Symbolic State Explosion -- A Unifying Model Checking Approach for Safety Properties of Parameterized Systems -- A BDD-Based Model Checker for Recursive Programs -- Temporal Logics and Verification -- Model Checking the World Wide Web? -- Distributed Symbolic Model Checking for ?-Calculus -- Tool Presentations: Model-Checking and Automata Techniques -- The Temporal Logic Sugar -- TReX: A Tool for Reachability Analysis of Complex Systems -- BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction -- SDLcheck: A Model Checking Tool -- EASN: Integrating ASN.1 and Model Checking -- Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams -- TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems? -- Microprocessor Verification, Cache Coherence -- Microarchitecture Verification by Compositional Model Checking -- Rewriting for Symbolic Execution of State Machine Models -- Using Timestamping and History Variables to Verify Sequential Consistency -- SAT, BDDs, and Applications -- Benefits of Bounded Model Checking at an Industrial Setting -- Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers -- Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m) -- Timed Automata -- Job-Shop Scheduling Using Timed Automata? -- As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata -- Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 650 | |a Informatique | ||
| 650 | |a Logiciels |x Vérification | ||
| 650 | |a Circuits intégrés | ||
| 650 | |a Intelligence artificielle | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Essais | ||
| 650 | |a Logiciels |x Essais | ||
| 650 | |a Structure logique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Finkel, Alain, |d 1958- |4 pbd | |
| 700 | 1 | |a Berry, Gérard, |d 1948-...., |c informaticien. |4 pbd | |
| 700 | 1 | |a Comon-Lundh, Hubert, |d 1957-...., |c auteur en informatique. |4 pbd | |
| 776 | 0 | |0 058096728 |t Computer aided verification |o 13th International conference, CAV 2001, Paris, France, July 18-22, 2001 |o proceedings |f Gérard Berry, Hubert Comon, Alain Finkel (eds.) |d 2001 |c Berlin |n Springer |p 1 vol. (XIII-520 p.) |s Lecture notes in computer science |z 3-540-42345-1 | |
| 776 | 0 | |t Computer Aided Verification |b Texte imprimé |z 9783662178379 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-44585-4 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-VQDPZN7H-2 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:748061479 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-44585-4 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:751513059 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-44585-4 |z Accès INSA CVL | |
| 997 | |0 948937 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||