Computer aided verification : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 July 2, 1998 : proceedings
This book consitutes the refereed proceedings of the 10th International Conference on Computer Aided Verification, CAV'98, held in Vancouver, BC, Canada, in June/July 1998. The 33 revised full papers and 10 tool papers presented were carefully selected from a total of 117 submissions. Also incl...
Guardat en:
| Autor corporatiu: | |
|---|---|
| Altres autors: | , |
| Format: | Livre numérique |
| Idioma: | Anglais |
| Publicat: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Col·lecció: | Lecture notes in computer science
1427 |
| Matèries: | |
| Accés en línia: | 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, 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998, proceedings, Alan J. Hu, Moshe Y. Vardi (eds.), 1998, Berlin, Springer, 1 vol. (IX-552 p.), Lecture notes in computer science, 3-540-64608-6 • Computer Aided Verification, Texte imprimé, 9783662193075 |
| LEADER | 06661nam a22004937a 4500 | ||
|---|---|---|---|
| 001 | 945152 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155216201 | ||
| 020 | |a 9783540693390 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 111 | 2 | |a International conference on computer-aided verification |n (10 |d :1998 |c :Vancouver, Canada). | |
| 245 | 1 | 0 | |a Computer aided verification : |b 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 July 2, 1998 : proceedings |c [edited by] Alan J. Hu, Moshe Y. Vardi. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 1427 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Synchronous programming of reactive systems -- Ten years of partial order reduction -- An ACL2 proof of write invalidate cache coherence -- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle -- A role for theorem proving in multi-processor design -- A formal method experience at secure computing corporation -- Formal methods in an industrial environment -- On checking model checkers -- Finite-state analysis of security protocols -- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols -- Verifying systems with infinite but regular state spaces -- Formal verification of out-of-order execution using incremental flushing -- Verification of an implementation of Tomasulo's algorithm by compositional model checking -- Decomposing the proof of correctness of pipelined microprocessors -- Processor verification with precise exceptions and speculative execution -- Symmetry reductions in model checking -- Structural symmetry and model checking -- Using magnetic disk instead of main memory in the Mur ? verifier -- On-the-fly model checking of RCTL formulas -- From pre-historic to post-modern symbolic model checking -- Model checking LTL using net unforldings -- Model checking for a first-order temporal logic using multiway decision graphs -- On the limitations of ordered representations of functions -- BDD based procedures for a theory of equality with uninterpreted functions -- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory -- Multiple counters automata, safety analysis and presburger arithmetic -- A comparison of Presburger engines for EFSM reachability -- Generating finite-state abstractions of reactive systems using decision procedures -- On-the-fly analysis of systems with unbounded, lossy FIFO channels -- Computing abstractions of infinite state systems compositionally and automatically -- Normed simulations -- An experiment in parallelizing an application using formal methods -- Efficient symbolic detection of global properties in distributed systems -- A machine-checked proof of the optimality of a real-time scheduling policy -- A general approach to partial order reductions in symbolic verification -- Correctness of the concurrent approach to symbolic verification of interleaved models -- Verification of timed systems using POSETs -- Mechanising BAN Kerberos by the inductive method -- Protocol verification in Nuprl -- You assume, we guarantee: Methodology and case studies -- Verification of a parameterized bus arbitration protocol -- The test model-checking approach to the verification of formal memory models of multiprocessors -- Design constraints in symbolic model checking -- Verification of floating-point adders -- Xeve, an Esterel verification environment -- InVeSt : A tool for the verification of invariants -- Verifying mobile processes in the HAL environment -- MONA 1.x: New techniques for WS1S and WS2S -- MOCHA: Modularity in modelchecking -- SCR: A toolset for specifying and analyzing software requirements -- A toolset for message sequence charts -- Real-time verification of Statemate designs -- Optikron: A tool suite for enhancing model-checking of real-time systems -- Kronos: A model-checking tool for real-time systems. | |
| 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 | ||
| 520 | |a This book consitutes the refereed proceedings of the 10th International Conference on Computer Aided Verification, CAV'98, held in Vancouver, BC, Canada, in June/July 1998. The 33 revised full papers and 10 tool papers presented were carefully selected from a total of 117 submissions. Also included are 11 invited contributions. Among the topics covered are modeling and specification formalisms; verification techniques like state-space exploration, model checking, synthesis, and automated deduction; various verification techniques; applications and case studies, and verification in practice. | ||
| 650 | |a Génie logiciel | ||
| 650 | |a Conception assistée par ordinateur | ||
| 650 | |a Informatique | ||
| 650 | |a Circuits intégrés | ||
| 650 | |a Intelligence artificielle | ||
| 650 | |a Évaluation | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Ordinateurs | ||
| 650 | |a Ingénierie assistée par ordinateur | ||
| 650 | |a Évaluation des logiciels | ||
| 650 | |a Structure logique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Hu, Alan J. |4 pbd | |
| 700 | 1 | |a Vardi, Moshe Ya'akov, |d 1954- |4 pbd | |
| 776 | 0 | |0 035973234 |t Computer aided verification |o 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28 - July 2, 1998 |o proceedings |f Alan J. Hu, Moshe Y. Vardi (eds.) |d 1998 |c Berlin |n Springer |p 1 vol. (IX-552 p.) |s Lecture notes in computer science |z 3-540-64608-6 | |
| 776 | 0 | |t Computer Aided Verification |b Texte imprimé |z 9783662193075 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/BFb0028725 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-CWF2LXQP-N |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:747913234 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/BFb0028725 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:75092599X |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/BFb0028725 |z Accès INSA CVL | |
| 997 | |0 945152 |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/ | ||