Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Computer Aided Verification [[electronic resource] ] : 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings / / edited by Gerard Berry, Hubert Comon, Alain Finkel
| Computer Aided Verification [[electronic resource] ] : 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings / / edited by Gerard Berry, Hubert Comon, Alain Finkel |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIII, 522 p.) |
| Disciplina | 005.74 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Database management
Computers Software engineering Computer logic Mathematical logic Artificial intelligence Database Management Theory of Computation Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-540-44585-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNISA-996465780103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings / / edited by Gerard Berry, Hubert Comon, Alain Finkel
| Computer Aided Verification : 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings / / edited by Gerard Berry, Hubert Comon, Alain Finkel |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIII, 522 p.) |
| Disciplina | 005.74 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Database management
Computers Software engineering Computer logic Mathematical logic Artificial intelligence Database Management Theory of Computation Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-540-44585-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNINA-9910143594503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Constraints in Computational Logics: Theory and Applications [[electronic resource] ] : International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8, 1999 Revised Lectures / / edited by Hubert Comon, Claude Marche, Ralf Treinen
| Constraints in Computational Logics: Theory and Applications [[electronic resource] ] : International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8, 1999 Revised Lectures / / edited by Hubert Comon, Claude Marche, Ralf Treinen |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 316 p.) |
| Disciplina | 005.11 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Software engineering Mathematical logic Artificial intelligence Computer logic Computer programming Computer System Implementation Software Engineering/Programming and Operating Systems Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-540-45406-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Constraints and Constraint Solving: An Introduction -- Constraint Solving on Terms -- Combining Constraint Solving -- Constraints and Theorem Proving -- Functional and Constraint Logic Programming -- Building Industrial Applications with Constraint Programming. |
| Record Nr. | UNISA-996465715603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Constraints in Computational Logics: Theory and Applications : International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8, 1999 Revised Lectures / / edited by Hubert Comon, Claude Marche, Ralf Treinen
| Constraints in Computational Logics: Theory and Applications : International Summer School, CCL'99 Gif-sur-Yvette, France, September 5-8, 1999 Revised Lectures / / edited by Hubert Comon, Claude Marche, Ralf Treinen |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 316 p.) |
| Disciplina | 005.11 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Software engineering Mathematical logic Artificial intelligence Computer logic Computer programming Computer System Implementation Software Engineering/Programming and Operating Systems Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-540-45406-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Constraints and Constraint Solving: An Introduction -- Constraint Solving on Terms -- Combining Constraint Solving -- Constraints and Theorem Proving -- Functional and Constraint Logic Programming -- Building Industrial Applications with Constraint Programming. |
| Record Nr. | UNINA-9910767541503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Rewriting Techniques and Applications [[electronic resource] ] : 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997. Proceedings / / edited by Hubert Comon
| Rewriting Techniques and Applications [[electronic resource] ] : 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997. Proceedings / / edited by Hubert Comon |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XII, 348 p.) |
| Disciplina | 005.13/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Computer science—Mathematics Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Symbolic and Algebraic Manipulation Artificial Intelligence |
| ISBN | 3-540-69051-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Well-behaved search and the Robbins problem -- Goal-Directed Completion using SOUR Graphs -- Shostak's congruence closure as completion -- Conditional equational specifications of data types with partial operations for inductive theorem proving -- Cross-sections for finitely presented monoids with decidable word problems -- New undecidability results for finitely presented monoids -- On the property of preserving regularity for string-rewriting systems -- Rewrite systems for natural, integral, and rational arithmetic -- D-bases for polynomial ideals over commutative noetherian rings -- On the word problem for free lattices -- A total, ground path ordering for proving termination of AC-rewrite systems -- Proving innermost normalisation automatically -- Termination of context-sensitive rewriting -- A new parallel closed condition for Church-Rosser of left-linear term rewriting systems -- Innocuous constructor-sharing combinations -- Scott's conjecture is true, position sensitive weights -- Two-dimensional rewriting -- A complete axiomatisation for the inclusion of series-parallel partial orders -- Undecidability of the first order theory of one-step right ground rewriting -- The first-order theory of one step rewriting in linear noetherian systems is undecidable -- Solving linear Diophantine equations using the geometric structure of the solution space -- A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms -- Effective reduction and conversion strategies for combinators -- Finite family developments -- Prototyping combination of unification algorithms with the ELAN rule-based programming language -- The invariant package of MAS -- Opal: A system for computing noncommutative gröbner bases -- TRAM: An abstract machine for order-sorted conditional term rewriting systems. |
| Record Nr. | UNINA-9910144922303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Rewriting Techniques and Applications [[electronic resource] ] : 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997. Proceedings / / edited by Hubert Comon
| Rewriting Techniques and Applications [[electronic resource] ] : 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997. Proceedings / / edited by Hubert Comon |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XII, 348 p.) |
| Disciplina | 005.13/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Computer science—Mathematics Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Symbolic and Algebraic Manipulation Artificial Intelligence |
| ISBN | 3-540-69051-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Well-behaved search and the Robbins problem -- Goal-Directed Completion using SOUR Graphs -- Shostak's congruence closure as completion -- Conditional equational specifications of data types with partial operations for inductive theorem proving -- Cross-sections for finitely presented monoids with decidable word problems -- New undecidability results for finitely presented monoids -- On the property of preserving regularity for string-rewriting systems -- Rewrite systems for natural, integral, and rational arithmetic -- D-bases for polynomial ideals over commutative noetherian rings -- On the word problem for free lattices -- A total, ground path ordering for proving termination of AC-rewrite systems -- Proving innermost normalisation automatically -- Termination of context-sensitive rewriting -- A new parallel closed condition for Church-Rosser of left-linear term rewriting systems -- Innocuous constructor-sharing combinations -- Scott's conjecture is true, position sensitive weights -- Two-dimensional rewriting -- A complete axiomatisation for the inclusion of series-parallel partial orders -- Undecidability of the first order theory of one-step right ground rewriting -- The first-order theory of one step rewriting in linear noetherian systems is undecidable -- Solving linear Diophantine equations using the geometric structure of the solution space -- A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms -- Effective reduction and conversion strategies for combinators -- Finite family developments -- Prototyping combination of unification algorithms with the ELAN rule-based programming language -- The invariant package of MAS -- Opal: A system for computing noncommutative gröbner bases -- TRAM: An abstract machine for order-sorted conditional term rewriting systems. |
| Record Nr. | UNISA-996465554403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Term Rewriting [[electronic resource] ] : French Spring School of Theoretical Computer Science, Font Romeux, France, 17 - 21, 1993. Advanced Course / / edited by Hubert Comon, Jean-Pierre Jouannaud
| Term Rewriting [[electronic resource] ] : French Spring School of Theoretical Computer Science, Font Romeux, France, 17 - 21, 1993. Advanced Course / / edited by Hubert Comon, Jean-Pierre Jouannaud |
| Edizione | [1st ed. 1995.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 |
| Descrizione fisica | 1 online resource (VIII, 228 p.) |
| Disciplina | 005.13/1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Mathematical logic
Mathematical Logic and Formal Languages |
| ISBN | 3-540-49237-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | to rewriting -- 33 Examples of termination -- The word problem for Thue rewriting systems -- Word problem for Thue systems with a few relations -- Some extensions of rewriting -- Graph rewriting: A bibliographical guide -- Formal languages & word-rewriting -- Rewriting and tree automata -- On efficient reduction algorithms for some trace rewriting systems -- Automatic groups and string rewriting -- A survey of symmetrized and complete group presentations -- Normalized rewriting — Application to ground completion and standard bases -- Equational reasoning with 2-dimensional diagrams -- Affine geometry of collinearity and conditional term rewriting -- Burnside monoids word problem and the conjecture of Brzozowski. |
| Record Nr. | UNISA-996466119603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||