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 | ||
| ||
Reachability Problems [[electronic resource] ] : 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings / / edited by Alain Finkel, Jerome Leroux, Igor Potapov
| Reachability Problems [[electronic resource] ] : 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings / / edited by Alain Finkel, Jerome Leroux, Igor Potapov |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XII, 149 p. 31 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Compilers (Computer programs) Algorithms Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Compilers and Interpreters Theory of Computation |
| ISBN | 3-642-33512-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Reachability problems in algebraic structures, computational models, hybrid systems, logic and verification -- Finite- and infinite-state concurrent systems -- Computational models -- Decision procedures. |
| Record Nr. | UNISA-996465865703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
STACS 92 [[electronic resource] ] : 9th Annual Symposium on Theoretical Aspects of Computer Science, Cachan, France, February 13-15, 1992. Proceedings / / edited by Alain Finkel, Matthias Jantzen
| STACS 92 [[electronic resource] ] : 9th Annual Symposium on Theoretical Aspects of Computer Science, Cachan, France, February 13-15, 1992. Proceedings / / edited by Alain Finkel, Matthias Jantzen |
| Edizione | [1st ed. 1992.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1992 |
| Descrizione fisica | 1 online resource (XVI, 628 p.) |
| Disciplina | 004 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Algorithms Computer logic Mathematical logic Numerical analysis Theory of Computation Computation by Abstract Devices Algorithm Analysis and Problem Complexity Logics and Meanings of Programs Mathematical Logic and Formal Languages Numerical Analysis |
| ISBN | 3-540-46775-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Structuring and modularizing algebraic specifications: the PLUSS specification language, evolutions and perspectives -- The parallel complexity of tree embedding problems (extended abstract) -- A theory of strict P-completeness -- Fast and optimal simulations between CRCW PRAMs -- Suitability of the propositional temporal logic to express properties of real-time systems -- Axiomatizations of backtracking -- Joining k- and l-recognizable sets of natural numbers -- On the performance of networks with multiple busses -- Efficient algorithms for solving systems of linear equations and path problems -- Efficient sublinear time parallel algorithms for dynamic programming and context-free recognition -- A simplified technique for hidden-line elimination in terrains -- A competitive analysis of nearest neighbor based algorithms for searching unknown scenes -- Equality and disequality constraints on direct subterms in tree automata -- Deterministic regular languages -- The extended low hierarchy is an infinite hierarchy -- Locally definable acceptance types for polynomial time machines -- The theory of the polynomial many-one degrees of recursive sets is undecidable -- A plane-sweep algorithm for finding a closest pair among convex planar objects -- Linear approximation of simple objects -- Language learning without overgeneralization -- The log-star revolution -- Separating counting communication complexity classes -- A nonlinear lower bound on the practical combinational complexity -- Characterizations of some complexity classes between ? 2 p and ? 2 p -- On complexity classes and algorithmically random languages -- New time hierarchy results for deterministic TMS -- Unconditional Byzantine agreement for any number of faulty processors -- Broadcasting in butterfly and debruijn networks -- Interval approximations of message causality in distributed executions -- On the approximability of the maximum common subgraph problem -- The complexity of colouring circle graphs -- Graph isomorphism is low for PP -- A simple linear time algorithm for triangulating three-colored graphs -- On locally optimal alignments in genetic sequences -- Secure commitment against a powerful adversary -- Communication efficient Zero-knowledge Proofs of knowledge -- Four results on randomized incremental constructions -- Enclosing many boxes by an optimal pair of boxes -- Performance driven k-layer wiring -- Synthesis for testability: Binary Decision Diagrams -- Compression and entropy -- Iterative devices generating infinite words -- On the factorization conjecture -- Conditional semi-Thue systems for presenting monoids -- A combinatorial bound for linear programming and related problems -- In-place linear probing sort -- Speeding up two string-matching algorithms -- The ANIGRAF system -- A programming language for symbolic computation of regular languages, automata and semigroups -- ?SPEED: a system for the specification and verification of microprocessors -- A discrete event simulator of communication algorithms in interconnection networks -- ALPHA DU CENTAUR: An environment for the design of systolic arrays -- Verification of communicating processes by means of automata reduction and abstraction -- Distributed system simulator (DSS) -- An interactive proof tool for process algebras -- SPECI90 A term rewriting and narrowing system. |
| Record Nr. | UNISA-996465639303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1992 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
STACS 93 [[electronic resource] ] : 10th Annual Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 25-27, 1993. Proceedings / / edited by Patrice Enjalbert, Alain Finkel, Klaus W. Wagner
| STACS 93 [[electronic resource] ] : 10th Annual Symposium on Theoretical Aspects of Computer Science, Würzburg, Germany, February 25-27, 1993. Proceedings / / edited by Patrice Enjalbert, Alain Finkel, Klaus W. Wagner |
| Edizione | [1st ed. 1993.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 |
| Descrizione fisica | 1 online resource (XIV, 730 p.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Algorithms Computer logic Mathematical logic Arithmetic and logic units, Computer Theory of Computation Computation by Abstract Devices Algorithm Analysis and Problem Complexity Logics and Meanings of Programs Mathematical Logic and Formal Languages Arithmetic and Logic Structures |
| ISBN | 3-540-47574-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Causal and distributed semantics for concurrent processes -- Editorial note -- Alternation for two-way machines with sublogarithmic space -- Separating the lower levels of the sublogarithmic space hierarchy -- Locating P/poly optimally in the extended low hierarchy -- Measure, stochasticity, and the density of hard languages -- Halting problem of one binary Horn clause is undecidable -- Decidability and undecidability results for duration calculus -- Defining ?-typed ?-calculi by axiomatizing the typing relation -- The complexity of logic-based abduction -- Treewidth of chordal bipartite graphs -- On paths in networks with valves -- Scheduling interval ordered tasks in parallel -- An O(?n)-worst-case-time solution to the granularity problem -- The synthesis problem of Petri nets -- General refinement and recursion operators for the Petri Box calculus -- On fairness in distributed automated deduction -- Divide-and-conquer algorithms on the hypercube -- A first-order isomorphism theorem -- Splittings, robustness and structure of complete sets -- Defying upward and downward separation -- Counting, selecting, and sorting by query-bounded machines -- Cancellation in context-free languages: Enrichment by reduction -- Counting overlap-free binary words -- The limit set of recognizable substitution systems -- Partially commutative Lyndon words -- Parallel architectures: Design and efficient use -- Weighted closest pairs -- Rectilinear path queries in a simple rectilinear polygon -- Parallel algorithm for the matrix chain product and the optimal triangulation problems (extended abstract) -- Multi-list ranking: complexity and applications -- Exact algorithms for a geometric packing problem (extended abstract) -- A decomposition theorem for probabilistic transition systems -- Local automata and completion -- Efficient compression of wavelet coefficients for smooth and fractal-like data -- On the equivalence of two-way pushdown automata and counter machines over bounded languages -- Computability properties of low-dimensional dynamical systems -- Fixed-parameter intractability II (extended abstract) -- Limits on the power of parallel random access machines with weak forms of write conflict resolution -- On using oracles that compute values -- Multicounter automata with sublogarithmic reversal bounds -- Structured operational semantics for concurrency and hierarchy -- The complexity of verifying functional programs -- Towards the formal design of self-stabilizing distributed algorithms -- Axiomatizations of temporal logics on trace systems -- Capabilities and complexity of computations with integer division -- Extended locally definable acceptance types -- Gap-definability as a closure property -- On the logical definability of some rational trace languages -- Solving systems of set constraints using tree automata -- Complement problems and tree automata in AC-like theories (extended abstract) -- Transparent (holographic) proofs -- Computing symmetric functions with AND/OR circuits and a single MAJORITY gate -- Threshold circuits for iterated multiplication: Using AC0 for free -- Circuits with monoidal gates -- A non-probabilistic switching lemma for the Sipser function -- Frontiers of feasible and probabilistic feasible Boolean manipulation with branching programs -- On syntactic congruences for ?—languages -- A polynomial time algorithm for the equivalence of two morphisms on ?-regular languages -- Locally threshold testable languages of infinite words -- Deterministic asynchronous automata for infinite traces -- Recursive automata on infinite words -- A complexity theoretic approach to incremental computation -- Precise average case complexity -- The bit probe complexity measure revisited -- Language learning with some negative information -- Language learning with a bounded number of mind changes -- Efficient sharing of many secrets -- The KIV system a tool for formal program development -- 1st Grade — A system for implementation, testing and animation of graph algorithms -- The program verifier Tatzelwurm -- LEDA a library of efficient data types and algorithms -- Defining ?-typed ?-calculi by axiomatizing the typing relation. |
| Record Nr. | UNISA-996466078103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||