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.
CONCUR '95 Concurrency Theory [[electronic resource] ] : 6th International Conference, Philadelphia, PA, USA, August 21 - 24, 1995. Proceedings / / edited by Scott Smolka
| CONCUR '95 Concurrency Theory [[electronic resource] ] : 6th International Conference, Philadelphia, PA, USA, August 21 - 24, 1995. Proceedings / / edited by Scott Smolka |
| Edizione | [1st ed. 1995.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 |
| Descrizione fisica | 1 online resource (XI, 553 p.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Programming languages (Electronic computers) Theory of Computation Logics and Meanings of Programs Computation by Abstract Devices Programming Languages, Compilers, Interpreters |
| ISBN | 3-540-44738-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Local model checking games (extended abstract) -- Compositional proof systems for model checking infinite state processes -- Compositional model checking of real time systems -- Checking bisimilarity for finitary ?-calculus -- The weak late ?-calculus semantics as observation equivalence -- The fixpoint-analysis machine -- Unique fixpoint induction for mobile processes -- A polymorphic type system for the polyadic ?-calculus -- Fibrational control structures -- Fully abstract models for nondeterministic regular expressions -- A Petri net semantics for ?-calculus -- A complete theory of deterministic event structures -- Characterizing behavioural congruences for Petri nets -- Verification of a distributed summation algorithm -- Confluence for process verification -- Axiomatisations of weak equivalences for De Simone languages -- A compositional trace-based semantics for probabilistic automata -- Acceptance trees for probabilistic processes -- Will I be pretty, will I be rich? Some thoughts on theory vs. practice in systems engineering -- Towards a denotational semantics for ET-LOTOS -- Reachability analysis at procedure level through timing coincidence -- Faster asynchronous systems -- Fair testing -- Formal methods technology transfer: Impediments and innovation (abstract) -- Decidability of simulation and bisimulation between lossy channel systems and finite state systems -- Checking regular properties of Petri nets -- Metric predicate transformers: Towards a notion of refinement for concurrency -- A refinement theory that supports both ’decrease of nondeterminism’ and ’increase of parallelism’ -- Model checking and efficient automation of temporal reasoning -- Verifying parameterized networks using abstraction and regular languages -- On the complexity of branching modular model checking -- Axiomatising linear time mu-calculus -- A trace consistent subset of PTL -- Tutorial: Proving properties of concurrent systems with SPIN -- On sharing and determinacy in concurrent systems -- Process semantics of graph reduction -- Bisimulations for a calculus of broadcasting systems -- Delayed choice for process algebra with abstraction -- CTR: A calculus of timed refinement -- Temporal logic + timed automata: Expressiveness and decidability. |
| Record Nr. | UNISA-996466131203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by Nir Piterman, Scott Smolka
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by Nir Piterman, Scott Smolka |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XXIV, 646 p. 137 illus.) |
| Disciplina | 004.21 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Algorithms Compilers (Computer programs) Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters |
| ISBN | 3-642-36742-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | On-the-Fly Exact Computation of Bisimilarity Distances -- The Quest for Minimal Quotients for Probabilistic Automata -- LTL Model Checking of Interval Markov Chains -- Ramsey vs. Lexicographic Termination Proving -- Structural Counter Abstraction -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors -- The MathSAT5 SMT Solver -- Formula Preprocessing in MUS Extraction -- Proof Tree Preserving Interpolation -- Asynchronous Multi-core Incremental SAT Solving -- Model-Checking Iterated Games -- PRISM-games: A Model Checker for Stochastic Multi-Player Games -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus -- An Overview of the mCRL2 Toolset and Its Recent Advances -- Analysis of Boolean Programs -- Weighted Pushdown Systems with Indexed Weight Domains -- Underapproximation of Procedure Summaries for Integer Programs -- Runtime Verification Based on Register Automata -- Unbounded Model-Checking with Interpolation for Regular Language Constraints -- eVolCheck: Incremental Upgrade Checker for C -- Intertwined Forward-Backward Reachability Analysis Using Interpolants -- An Integrated Specification and Verification Technique or Highly Concurrent Data Structures -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory -- Synthesis of Circular Compositional Program Proofs via Abduction -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty -- Integer Parameter Synthesis for Timed Automata -- LTL Model-Checking for Malware Detection -- Policy Analysis for Self-administrated Role-Based Access Control -- Model Checking Agent Knowledge in Dynamic Access Control Policies -- Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems -- Equivalence Checking of Quantum Protocols -- Encoding Monomorphic and Polymorphic Types -- Deriving Probability Density Functions from Probabilistic Functional Programs -- Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO -- BULL: A Library for Learning Algorithms of Boolean Functions -- AppGuard – Enforcing User Requirements on Android Apps -- Model Checking Database Applications -- Efficient Property Preservation Checking of Model Refinements -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking -- Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013) -- CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution) -- CSeq: A Sequentialization Tool for C (Competition Contribution) -- Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) -- Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution) -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution) -- Threader: A Verifier for Multi-threaded Programs (Competition Contribution) -- UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) -- Ultimate Automizer with SMTInterpol (Competition Contribution). |
| Record Nr. | UNISA-996465970203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by Nir Piterman, Scott Smolka
| Tools and Algorithms for the Construction and Analysis of Systems : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings / / edited by Nir Piterman, Scott Smolka |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XXIV, 646 p. 137 illus.) |
| Disciplina | 004.21 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Algorithms Compilers (Computer programs) Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters |
| ISBN | 3-642-36742-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | On-the-Fly Exact Computation of Bisimilarity Distances -- The Quest for Minimal Quotients for Probabilistic Automata -- LTL Model Checking of Interval Markov Chains -- Ramsey vs. Lexicographic Termination Proving -- Structural Counter Abstraction -- Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors -- The MathSAT5 SMT Solver -- Formula Preprocessing in MUS Extraction -- Proof Tree Preserving Interpolation -- Asynchronous Multi-core Incremental SAT Solving -- Model-Checking Iterated Games -- PRISM-games: A Model Checker for Stochastic Multi-Player Games -- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus -- An Overview of the mCRL2 Toolset and Its Recent Advances -- Analysis of Boolean Programs -- Weighted Pushdown Systems with Indexed Weight Domains -- Underapproximation of Procedure Summaries for Integer Programs -- Runtime Verification Based on Register Automata -- Unbounded Model-Checking with Interpolation for Regular Language Constraints -- eVolCheck: Incremental Upgrade Checker for C -- Intertwined Forward-Backward Reachability Analysis Using Interpolants -- An Integrated Specification and Verification Technique or Highly Concurrent Data Structures -- A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems -- Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory -- Synthesis of Circular Compositional Program Proofs via Abduction -- As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty -- Integer Parameter Synthesis for Timed Automata -- LTL Model-Checking for Malware Detection -- Policy Analysis for Self-administrated Role-Based Access Control -- Model Checking Agent Knowledge in Dynamic Access Control Policies -- Frontiers (Graphics and Quantum) Automatic Testing of Real-Time Graphics Systems -- Equivalence Checking of Quantum Protocols -- Encoding Monomorphic and Polymorphic Types -- Deriving Probability Density Functions from Probabilistic Functional Programs -- Tool Demonstrations Polyglot: Systematic Analysis for Multiple Statechart Formalisms -- Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO -- BULL: A Library for Learning Algorithms of Boolean Functions -- AppGuard – Enforcing User Requirements on Android Apps -- Model Checking Database Applications -- Efficient Property Preservation Checking of Model Refinements -- Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking -- Competition on Software Verification Second Competition on Software Verification (Summary of SV-COMP 2013) -- CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution) -- CSeq: A Sequentialization Tool for C (Competition Contribution) -- Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution) -- LLBMC: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution) -- Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution) -- Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution) -- Threader: A Verifier for Multi-threaded Programs (Competition Contribution) -- UFO: Verification with Interpolants and Abstract Interpretation (Competition Contribution) -- Ultimate Automizer with SMTInterpol (Competition Contribution). |
| Record Nr. | UNINA-9910739423503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||