CONCUR 2002 - Concurrency Theory [[electronic resource] ] : 13th International Conference, Brno, Czech Republic, August 20-23, 2002. Proceedings / / edited by Lubos Brim, Petr Jancar, Mojmir Kretinsky, Antonin Kucera |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XII, 609 p.) |
Disciplina | 004.35 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Architecture, Computer Computer logic Programming languages (Electronic computers) Computer programming Theory of Computation Computer System Implementation Logics and Meanings of Programs Computation by Abstract Devices Programming Languages, Compilers, Interpreters Programming Techniques |
ISBN | 3-540-45694-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Refinement and Verification Applied to an In-Flight Data Acquisition Unit* -- A Deductive Proof System for CTL* -- Event-State Duality: The Enriched Case -- Expressive Power of Temporal Logics -- Types, or: Where’s the Difference Between CCS and ?? -- Invited Tutorials -- to Modal and Temporal Mu-Calculi -- Types for Cryptographic Protocols -- Verification, Model Checking -- Network Invariants in Action* -- Regular Model Checking Made Simple and Effcient* -- A Hierarchy of Polynomial-Time Computable Simulations for Automata -- A Decidable Class of Asynchronous Distributed Controllers -- Alphabet-Based Synchronisation is Exponentially Cheaper -- Safe Realizability of High-Level Message Sequence Charts* -- Widening the Boundary between Decidable and Undecidable Hybrid Systems* -- Logic -- A Spatial Logic for Concurrency (Part II) -- Reducing Model Checking from Multi-valued CTL* to CTL* -- Local Model Checking Games for Fixed Point Logic with Chop -- A Decidable Fixpoint Logic for Time-Outs* -- Mobility -- A Calculus of Mobile Resources* -- Using Ambients to Control Resources* -- Typing and Subtyping Mobility in Boxed Ambients* -- Orchestrating Transactions in Join Calculus* -- Probabilistic Systems -- Simulation for Continuous-Time Markov Chains -- Weak Bisimulation is Sound and Complete for PCTL* -- Decision Algorithms for Probabilistic Bisimulation* -- Models of Computation, Process Algebra -- Axiomatizing an Algebra of Step Reactions for Synchronous Languages -- Regular Sets of Pomsets with Autoconcurrency -- The Fusion Machine -- HOPLA—A Higher-Order Process Language -- A First Order Coalgebraic Model of ?-Calculus Early Observational Equivalence* -- Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes -- Security -- A Framework for the Analysis of Security Protocols* -- On Name Generation and Set-Based Analysis in the Dolev-Yao Model -- On the Decidability of Cryptographic Protocols with Open-Ended Data Structures -- Petri Nets -- Causality Semantics of Petri Nets with Weighted Inhibitor Arcs -- Refinement-Robust Fairness -- Bisimulation -- Decidability of Strong Bisimilarity for Timed BPP -- Undecidability of Weak Bisimilarity for Pushdown Processes -- Why Is Simulation Harder than Bisimulation?. |
Record Nr. | UNISA-996466340503316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
CONCUR 2002 - Concurrency Theory : 13th International Conference, Brno, Czech Republic, August 20-23, 2002. Proceedings / / edited by Lubos Brim, Petr Jancar, Mojmir Kretinsky, Antonin Kucera |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (XII, 609 p.) |
Disciplina | 004.35 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Architecture, Computer Computer logic Programming languages (Electronic computers) Computer programming Theory of Computation Computer System Implementation Logics and Meanings of Programs Computation by Abstract Devices Programming Languages, Compilers, Interpreters Programming Techniques |
ISBN | 3-540-45694-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Refinement and Verification Applied to an In-Flight Data Acquisition Unit* -- A Deductive Proof System for CTL* -- Event-State Duality: The Enriched Case -- Expressive Power of Temporal Logics -- Types, or: Where’s the Difference Between CCS and ?? -- Invited Tutorials -- to Modal and Temporal Mu-Calculi -- Types for Cryptographic Protocols -- Verification, Model Checking -- Network Invariants in Action* -- Regular Model Checking Made Simple and Effcient* -- A Hierarchy of Polynomial-Time Computable Simulations for Automata -- A Decidable Class of Asynchronous Distributed Controllers -- Alphabet-Based Synchronisation is Exponentially Cheaper -- Safe Realizability of High-Level Message Sequence Charts* -- Widening the Boundary between Decidable and Undecidable Hybrid Systems* -- Logic -- A Spatial Logic for Concurrency (Part II) -- Reducing Model Checking from Multi-valued CTL* to CTL* -- Local Model Checking Games for Fixed Point Logic with Chop -- A Decidable Fixpoint Logic for Time-Outs* -- Mobility -- A Calculus of Mobile Resources* -- Using Ambients to Control Resources* -- Typing and Subtyping Mobility in Boxed Ambients* -- Orchestrating Transactions in Join Calculus* -- Probabilistic Systems -- Simulation for Continuous-Time Markov Chains -- Weak Bisimulation is Sound and Complete for PCTL* -- Decision Algorithms for Probabilistic Bisimulation* -- Models of Computation, Process Algebra -- Axiomatizing an Algebra of Step Reactions for Synchronous Languages -- Regular Sets of Pomsets with Autoconcurrency -- The Fusion Machine -- HOPLA—A Higher-Order Process Language -- A First Order Coalgebraic Model of ?-Calculus Early Observational Equivalence* -- Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes -- Security -- A Framework for the Analysis of Security Protocols* -- On Name Generation and Set-Based Analysis in the Dolev-Yao Model -- On the Decidability of Cryptographic Protocols with Open-Ended Data Structures -- Petri Nets -- Causality Semantics of Petri Nets with Weighted Inhibitor Arcs -- Refinement-Robust Fairness -- Bisimulation -- Decidability of Strong Bisimilarity for Timed BPP -- Undecidability of Weak Bisimilarity for Pushdown Processes -- Why Is Simulation Harder than Bisimulation?. |
Record Nr. | UNINA-9910768179203321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal Methods: Applications and Technology [[electronic resource] ] : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (371 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Special purpose computers Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
Record Nr. | UNISA-996466247603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods: Applications and Technology : 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected / / edited by Lubos Brim, Boudewijn Haverkort, Martin Leucker, Jaco van de Pol |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (371 p.) |
Disciplina | 004.0151 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computers
Software engineering Computer logic Programming languages (Electronic computers) Special purpose computers Theory of Computation Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
ISBN |
1-280-93577-4
9786610935772 3-540-70952-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Challenges for Formal Verification in Industrial Setting -- Distributed Verification: Exploring the Power of Raw Computing Power -- FMICS -- An Easy-to-Use, Efficient Tool-Chain to Analyze the Availability of Telecommunication Equipment -- ”To Store or Not To Store” Reloaded: Reclaiming Memory on Demand -- Discovering Symmetries -- On Combining Partial Order Reduction with Fairness Assumptions -- Test Coverage for Loose Timing Annotations -- Model-Based Testing of a WAP Gateway: An Industrial Case-Study -- Heuristics for ioco-Based Test-Based Modelling -- Verifying VHDL Designs with Multiple Clocks in SMV -- Verified Design of an Automated Parking Garage -- Evaluating Quality of Service for Service Level Agreements -- Simulation-Based Performance Analysis of a Medical Image-Processing Architecture -- Blasting Linux Code -- A Finite State Modeling of AFDX Frame Management Using Spin -- UML 2.0 State Machines: Complete Formal Semantics Via core state machine -- Automated Incremental Synthesis of Timed Automata -- SAT-Based Verification of LTL Formulas -- jmle: A Tool for Executing JML Specifications Via Constraint Programming -- Goanna—A Static Model Checker -- PDMC -- Parallel SAT Solving in Bounded Model Checking -- Parallel Algorithms for Finding SCCs in Implicitly Given Graphs -- Can Saturation Be Parallelised? -- Distributed Colored Petri Net Model-Checking with Cyclades. |
Record Nr. | UNINA-9910483608403321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Mathematical Foundations of Computer Science 1998 [[electronic resource] ] : 23rd International Symposium, MFCS'98, Brno, Czech Republic, August 24-28, 1998 / / edited by Lubos Brim, Josef Gruska, Jiri Zlatuska |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (XVIII, 854 p.) |
Disciplina | 004.0151 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer communication systems Computer science—Mathematics Theory of Computation Computer Communication Networks Discrete Mathematics in Computer Science |
ISBN | 3-540-68532-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Hypergraph traversal revisited: Cost measures and dynamic algorithms -- Defining the Java Virtual Machine as platform for provably correct Java compilation -- Towards a theory of recursive structures -- Modularization and abstraction: The keys to practical formal verification -- On the role of time and space in neural computation -- From algorithms to working programs: On the use of program checking in LEDA -- Computationally-sound checkers -- Reasoning about the past -- Satisfiability — Algorithms and logic -- The joys of bisimulation -- Towards algorithmic explanation of mind evolution and functioning -- Combinatorial hardness proofs for polynomial evaluation -- Minimum propositional proof length is NP-hard to linearly approximate -- Reconstructing polyatomic structures from discrete X-rays: NP-completeness proof for three atoms -- Locally explicit construction of r?dl's asymptotically good packings -- Proof theory of fuzzy logics: Urquhart's C and related logics -- Nonstochastic languages as projections of 2-tape quasideterministic languages -- Flow logic for Imperative Objects -- Expressive completeness of Temporal Logic of action -- Reducing AC-termination to termination -- On one-pass term rewriting -- On the word, subsumption, and complement problem for recurrent term schematizations -- Encoding the hydra battle as a rewrite system -- Computing ?-free NFA from regular expressions in O(n log2(N)) time -- Iterated length-preserving rational transductions -- The head hierarchy for oblivious finite automata with polynomial advice collapses -- The equivalence problem for deterministic pushdown transducers into abelian groups -- The semi-full closure of Pure Type Systems -- Predicative polymorphic subtyping -- A computational interpretation of the ??-calculus -- Polymorphic subtyping without distributivity -- A (non-elementary) modular decision procedure for LTrL -- Complete abstract interpretations made constructive -- Timed bisimulation and open maps -- Deadlocking states in context-free process algebra -- A superpolynomial lower bound for a circuit computing the clique function with at most (1/6) log log n negation gates -- On counting ac 0 circuits with negative constants -- A second step towards circuit complexity-theoretic analogs of Rice's theorem -- Model checking Real-Time properties of symmetric systems -- Locality of order-invariant first-order formulas -- Probabilistic concurrent constraint programming: Towards a fully abstract model -- Lazy functional algorithms for exact real functionals -- Randomness vs. completeness: On the diagonalization strength of resource-bounded random sets -- Positive turing and truth-table completeness for NEXP are incomparable -- Tally NP sets and easy census functions -- Average-case intractability vs. worst-case intractability -- Shuffle on trajectories: The schützenberger product and related operations -- Gaußian elimination and a characterization of algebraic power series -- D0L-systems and surface automorphisms -- About synchronization languages -- When can an equational simple graph be generated by hyperedge replacement? -- Spatial and temporal refinement of typed graph transformation systems -- Approximating maximum independent sets in uniform hypergraphs -- Representing hyper-graphs by regular languages -- Improved time and space hierarchies of one-tape off-line TMs -- Tarskian set constraints are in NEXPTIME -- ??*-Equational theory of context unification is ? 1 0 -hard -- Speeding-up nondeterministic single-tape off-line computations by one alternation -- Facial circuits of planar graphs and context-free languages -- Optimizing OBDDs is still intractable for monotone functions -- Blockwise variable orderings for shared BDDs -- On the composition problem for OBDDs with multiple variable orders -- Equations in transfinite strings -- Minimal forbidden words and factor automata -- On defect effect of bi-infinite words -- On repetition-free binary words of minimal density -- Embedding of hypercubes into grids -- Tree decompositions of small diameter -- Degree-preserving forests -- A parallelization of Dijkstra's shortest path algorithm -- Comparison between the complexity of a function and the complexity of its graph -- IFS and control languages -- One quantifier will do in existential monadic second-order logic over pictures -- On some recognizable picture-languages -- On the complexity of wavelength converters -- On Boolean vs. Modular arithmetic for circuits and communication protocols -- Communication complexity and lower bounds on multilective computations -- A finite hierarchy of the recursively enumerable real numbers -- One guess one-way cellular arrays -- Topological definitions of chaos applied to cellular automata dynamics -- Characterization of sensitive linear cellular automata with respect to the counting distance -- Additive cellular automata over ?p and the bottom of (CA,?). |
Record Nr. | UNISA-996466106303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Mathematical Foundations of Computer Science 1998 [[electronic resource] ] : 23rd International Symposium, MFCS'98, Brno, Czech Republic, August 24-28, 1998 / / edited by Lubos Brim, Josef Gruska, Jiri Zlatuska |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
Descrizione fisica | 1 online resource (XVIII, 854 p.) |
Disciplina | 004.0151 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Computer communication systems Computer science—Mathematics Theory of Computation Computer Communication Networks Discrete Mathematics in Computer Science |
ISBN | 3-540-68532-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Hypergraph traversal revisited: Cost measures and dynamic algorithms -- Defining the Java Virtual Machine as platform for provably correct Java compilation -- Towards a theory of recursive structures -- Modularization and abstraction: The keys to practical formal verification -- On the role of time and space in neural computation -- From algorithms to working programs: On the use of program checking in LEDA -- Computationally-sound checkers -- Reasoning about the past -- Satisfiability — Algorithms and logic -- The joys of bisimulation -- Towards algorithmic explanation of mind evolution and functioning -- Combinatorial hardness proofs for polynomial evaluation -- Minimum propositional proof length is NP-hard to linearly approximate -- Reconstructing polyatomic structures from discrete X-rays: NP-completeness proof for three atoms -- Locally explicit construction of r?dl's asymptotically good packings -- Proof theory of fuzzy logics: Urquhart's C and related logics -- Nonstochastic languages as projections of 2-tape quasideterministic languages -- Flow logic for Imperative Objects -- Expressive completeness of Temporal Logic of action -- Reducing AC-termination to termination -- On one-pass term rewriting -- On the word, subsumption, and complement problem for recurrent term schematizations -- Encoding the hydra battle as a rewrite system -- Computing ?-free NFA from regular expressions in O(n log2(N)) time -- Iterated length-preserving rational transductions -- The head hierarchy for oblivious finite automata with polynomial advice collapses -- The equivalence problem for deterministic pushdown transducers into abelian groups -- The semi-full closure of Pure Type Systems -- Predicative polymorphic subtyping -- A computational interpretation of the ??-calculus -- Polymorphic subtyping without distributivity -- A (non-elementary) modular decision procedure for LTrL -- Complete abstract interpretations made constructive -- Timed bisimulation and open maps -- Deadlocking states in context-free process algebra -- A superpolynomial lower bound for a circuit computing the clique function with at most (1/6) log log n negation gates -- On counting ac 0 circuits with negative constants -- A second step towards circuit complexity-theoretic analogs of Rice's theorem -- Model checking Real-Time properties of symmetric systems -- Locality of order-invariant first-order formulas -- Probabilistic concurrent constraint programming: Towards a fully abstract model -- Lazy functional algorithms for exact real functionals -- Randomness vs. completeness: On the diagonalization strength of resource-bounded random sets -- Positive turing and truth-table completeness for NEXP are incomparable -- Tally NP sets and easy census functions -- Average-case intractability vs. worst-case intractability -- Shuffle on trajectories: The schützenberger product and related operations -- Gaußian elimination and a characterization of algebraic power series -- D0L-systems and surface automorphisms -- About synchronization languages -- When can an equational simple graph be generated by hyperedge replacement? -- Spatial and temporal refinement of typed graph transformation systems -- Approximating maximum independent sets in uniform hypergraphs -- Representing hyper-graphs by regular languages -- Improved time and space hierarchies of one-tape off-line TMs -- Tarskian set constraints are in NEXPTIME -- ??*-Equational theory of context unification is ? 1 0 -hard -- Speeding-up nondeterministic single-tape off-line computations by one alternation -- Facial circuits of planar graphs and context-free languages -- Optimizing OBDDs is still intractable for monotone functions -- Blockwise variable orderings for shared BDDs -- On the composition problem for OBDDs with multiple variable orders -- Equations in transfinite strings -- Minimal forbidden words and factor automata -- On defect effect of bi-infinite words -- On repetition-free binary words of minimal density -- Embedding of hypercubes into grids -- Tree decompositions of small diameter -- Degree-preserving forests -- A parallelization of Dijkstra's shortest path algorithm -- Comparison between the complexity of a function and the complexity of its graph -- IFS and control languages -- One quantifier will do in existential monadic second-order logic over pictures -- On some recognizable picture-languages -- On the complexity of wavelength converters -- On Boolean vs. Modular arithmetic for circuits and communication protocols -- Communication complexity and lower bounds on multilective computations -- A finite hierarchy of the recursively enumerable real numbers -- One guess one-way cellular arrays -- Topological definitions of chaos applied to cellular automata dynamics -- Characterization of sensitive linear cellular automata with respect to the counting distance -- Additive cellular automata over ?p and the bottom of (CA,?). |
Record Nr. | UNINA-9910767582103321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|