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.
Automated Technology for Verification and Analysis [[electronic resource] ] : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang
| Automated Technology for Verification and Analysis [[electronic resource] ] : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XIII, 520 p. 96 illus.) |
| Disciplina | 005.13 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Computer programming Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence Programming Techniques |
| ISBN | 3-319-24953-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Probabilistic Programming: A True Verification Challenge -- References -- Machines Reasoning About Machines: 2015 -- 1 Introduction -- 2 A Quick History and Acknowledgments -- 3 1970s -- Simple List Processing -- 4 1980s -- Academic Math and Computer Science -- 5 1990s -- Commercial Breakthrough -- 6 2000s -- Gradual Acceptance -- 7 2010 -- Integrated with the Design Process -- 8 Lessons -- 9 Conclusion -- References -- Using SMT for Solving Fragments of Parameterised Boolean Equation Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Motivating Example -- 4 Disjunctive and Conjunctive PBESs -- 5 Solving Disjunctive and Conjunctive PBESs Using SMT -- 5.1 Finding Lasso-Shaped Proof Graphs -- 5.2 Proving the Absence of Proof Graphs -- 5.3 A Pseudo-Decision Procedure -- 6 Experiments -- 7 Closing Remarks -- References -- Unfolding-Based Process Discovery -- 1 Introduction -- 2 Preliminaries -- 3 Independence-Preserving Discovery -- 4 Introducing Generalization -- 4.1 Language-Preserving Generalization -- 4.2 Controlling Generalization via Negative Information -- 5 Computing Folding Equivalences -- 5.1 SMT Encoding -- 5.2 Finding an Optimal Folding Equivalence -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Improving Interpolants for Linear Arithmetic -- 1 Introduction -- 2 Preliminaries -- 2.1 Notations -- 2.2 Computing Interpolants by Resolution Proofs -- 2.3 Computing Interpolants by DC-Removability Checks -- 2.4 Description of a State Set -- 3 The General Algorithm -- 3.1 Test Whether One Additional Linear Constraint Is Sufficient -- 3.2 Finding Pairs of Indistinguishable Points with SMT -- 3.3 Enlarge Pairs of Indistinguishable Points to Convex Regions -- 3.4 Finding a Linear Constraint Separating Pairs of Convex Regions with LP -- 4 Optimizations -- 5 Experimental Results.
6 Conclusion and Further Research -- References -- A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences -- 1 Introduction -- 2 Overview -- 3 Source Language and Its Guarded Form -- 3.1 Input Language -- 3.2 Guarded Language -- 3.3 Translation to Guarded Form -- 4 Structured Differences Between Programs -- 5 Generation Algorithm Directed by Structured Differences -- 6 Implementation and Experiments -- 7 Related Work -- 8 Conclusion -- References -- On Automated Lemma Generation for Separation Logic with Inductive Definitions -- 1 Introduction -- 2 Motivating Example -- 3 Separation Logic with Inductive Definitions -- 4 Composition Lemmas -- 5 Derived Lemmas -- 5.1 The ``Completion'' Lemmas -- 5.2 The ``Stronger'' Lemmas -- 6 A Proof Strategy Based on Lemmas -- 7 Experimental Results -- 8 Related Work -- 9 Conclusion -- References -- Severity Levels of Inconsistent Code -- 1 Introduction -- 2 Overview -- 3 Inconsistent Code -- 4 Severity Levels of Inconsistency -- 5 Algorithm for Categorizing Inconsistent Code -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning the Language of Error -- 1 Introduction -- 2 Preliminaries -- the L* Algorithm -- 3 The Language We Learn -- 4 L* and the Queries -- 4.1 Membership Queries -- 4.2 Conjecture Queries -- 5 Usage Scenarios for the Learning Framework -- 6 System Description and Empirical Evaluation -- 6.1 Optimisations -- 6.2 Implementation and Evaluation -- 7 Conclusions and Future Work -- References -- Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage -- 1 Introduction -- 2 Preliminaries -- 3 Disk-Based State Space Exploration with Partitioning -- 3.1 Representation of MDP in Memory and on Disk -- 3.2 Disk-Based Exploration Using Partitioning -- 4 Disk-Based Partitioned Value Iteration -- 5 Evaluation. 6 Conclusion -- References -- Model Checking Failure-Prone Open Systems Using Probabilistic Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Hierarchical Probabilistic Automata -- 3 Decision Algorithms and Robustness -- 3.1 Forward Algorithm -- 3.2 Backward Algorithm -- 3.3 Forward vs. Backward -- 3.4 Robustness -- 4 Undecidability for 2-HPA -- 5 Modeling Failure-Prone Open Systems -- 6 Implementation and Experiment -- 6.1 Implementation of the Verification Algorithms -- 6.2 Abstracting Models of Web Applications -- 6.3 Experiment -- 7 Conclusions -- References -- Optimal Continuous Time Markov Decisions -- 1 Introduction -- 2 Preliminaries -- 3 Unif+: Optimal Time-Bounded Reachability Revisited -- 3.1 Uniformisation to C -- 3.2 Lower and Upper Bounds on the Value of C -- 3.3 Convergence of the Bounds for Increasing -- 3.4 Extracting the Scheduler -- 4 Existing Algorithms -- 5 Empirical Evaluation and Comparison -- 6 Conclusion -- References -- Spanning the Spectrum from Safety to Liveness -- 1 Introduction -- 2 Preliminaries -- 3 Classes of Safety -- 3.1 Co-safety -- 3.2 Finding the Safety Level -- 4 Finding the Safety Class -- 4.1 Observations on Automata -- 4.2 Expressive Power -- 4.3 Decision Procedures -- 5 Discussion and Directions for Future Research -- References -- Marimba: A Tool for Verifying Properties of Hidden Markov Models -- 1 Introduction -- 2 Tool Architecture and Implementation -- 2.1 Marimba's Input and Modules -- 3 Verification of a Human-Robot Interaction -- 4 Conclusions -- References -- ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols -- 1 Introduction -- 2 Consistency Lemma -- 3 Overview of Our Approach -- 4 Validation and Conclusion -- References -- ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks -- 1 Introduction -- 2 Architecture and Usage. 3 Comparison, Evaluation and Future Developments -- References -- EviCheck: Digital Evidence for Android -- 1 Introduction and Related Work -- 2 EviCheck's Main Ingredients -- 2.1 Policy Language -- 2.2 The Verifier -- 2.3 The Checker -- 2.4 Policy Generator -- 2.5 Technical Discussion -- 3 Implementation and Experiments -- References -- Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant Schedules -- 1 Introduction -- 2 Optimized Scheduler Encoding -- 3 Implementation Details -- 4 Experimental Evaluation and Conclusion -- References -- A Contextual Equivalence Checker for IMJ* -- 1 Introduction -- 2 Tool Architecture -- 3 Evaluation -- References -- Trace Diagnostics Using Temporal Implicants -- 1 Introduction -- 2 Propositional Foundations -- 2.1 Problem Statement -- 2.2 Syntactic and Semantic Formulations -- 2.3 Practical Solution -- 3 Temporal Issues -- 3.1 Syntactic Rewritings -- 3.2 Semantic Restrictions -- 3.3 Sub-models of a Formula -- 3.4 Temporal Implicants -- 4 MTL Diagnostics -- 4.1 Non-Standard MTL Semantics -- 4.2 Explanation Operators -- 4.3 Computation of Selection Functions -- 4.4 Discussion -- 5 LTL Ultimately-Periodic Diagnostics -- 5.1 Recurrent LTL Semantics -- 5.2 Explanation Operators -- 6 Conclusion and Perspectives -- References -- Test Case Generation of Actor Systems -- 1 Introduction -- 2 The Language -- 3 Symbolic Execution -- 4 Less Redundant Exploration in Symbolic Execution -- 5 Generation of Test Cases -- 5.1 Coverage and Termination Criteria for Actor Systems -- 5.2 Test Cases for Actor Systems -- 6 Implementation and Experimental Evaluation -- 7 Related Work and Conclusions -- References -- Lattice-Based Semantics for Combinatorial Model Evolution -- 1 Introduction -- 2 Running Example and Overview -- 3 Preliminaries. 4 Lattice-Based Semantics for Combinatorial Model Evolution -- 5 Atomic Operations on Combinatorial Models -- 5.1 Adding or Removing a Parameter and Its Values -- 5.2 Adding or Removing a Value from an Existing Parameter -- 5.3 Adding, Removing, or Changing a Constraint -- 6 Split and Merge Operations on Combinatorial Models -- 7 Related Work -- 8 Summary and Future Work -- References -- Effective Verification of Replicated Data Types Using Later Appearance Records (LAR) -- 1 Introduction -- 2 CRDTs, Traces and Specifications -- 3 CRDT Implementation -- 3.1 Reference Implementation -- 3.2 Details of the Reference Implementation -- 3.3 Correctness of the Reference Implementation -- 3.4 Bounding the Reference Implementation -- 4 Effective Verification Using Bounded Reference Implementation via CEGAR -- 5 Conclusion -- References -- TSO-to-TSO Linearizability Is Undecidable -- 1 Introduction -- 2 TSO Concurrent Systems -- 2.1 Notations -- 2.2 Libraries and the Most General Clients -- 2.3 TSO Operational Semantics -- 3 TSO-to-TSO Linearizability and Equivalent Characterization -- 3.1 TSO-to-TSO Linearizability -- 3.2 Equivalence Characterization -- 4 Undecidability of TSO-to-TSO Linearizability -- 4.1 Classic-Lossy Single-Channel Systems -- 4.2 Simulation on the TSO Memory Model -- 4.3 Undecidability of History Inclusion -- 4.4 Undecidability of TSO-to-TSO Linearizability -- 5 Conclusion and Future Work -- References -- Formal Verification of Infinite-State BIP Models -- 1 Introduction -- 2 The BIP Model -- 3 ESST for BIP (ESST BIP ) -- 3.1 The ESST Framework -- 3.2 Instantiation of ESST for BIP -- 3.3 Optimizations -- 4 Encoding BIP into Transition System -- 5 Related Work -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- PBMC: Symbolic Slicing for the Verification of Concurrent Programs -- 1 Introduction. 2 Motivating Example. |
| Record Nr. | UNISA-996466290303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Technology for Verification and Analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang
| Automated Technology for Verification and Analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XIII, 520 p. 96 illus.) |
| Disciplina | 005.13 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Logic, Symbolic and mathematical Artificial intelligence Computer programming Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence Programming Techniques |
| ISBN | 3-319-24953-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Probabilistic Programming: A True Verification Challenge -- References -- Machines Reasoning About Machines: 2015 -- 1 Introduction -- 2 A Quick History and Acknowledgments -- 3 1970s -- Simple List Processing -- 4 1980s -- Academic Math and Computer Science -- 5 1990s -- Commercial Breakthrough -- 6 2000s -- Gradual Acceptance -- 7 2010 -- Integrated with the Design Process -- 8 Lessons -- 9 Conclusion -- References -- Using SMT for Solving Fragments of Parameterised Boolean Equation Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Motivating Example -- 4 Disjunctive and Conjunctive PBESs -- 5 Solving Disjunctive and Conjunctive PBESs Using SMT -- 5.1 Finding Lasso-Shaped Proof Graphs -- 5.2 Proving the Absence of Proof Graphs -- 5.3 A Pseudo-Decision Procedure -- 6 Experiments -- 7 Closing Remarks -- References -- Unfolding-Based Process Discovery -- 1 Introduction -- 2 Preliminaries -- 3 Independence-Preserving Discovery -- 4 Introducing Generalization -- 4.1 Language-Preserving Generalization -- 4.2 Controlling Generalization via Negative Information -- 5 Computing Folding Equivalences -- 5.1 SMT Encoding -- 5.2 Finding an Optimal Folding Equivalence -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Improving Interpolants for Linear Arithmetic -- 1 Introduction -- 2 Preliminaries -- 2.1 Notations -- 2.2 Computing Interpolants by Resolution Proofs -- 2.3 Computing Interpolants by DC-Removability Checks -- 2.4 Description of a State Set -- 3 The General Algorithm -- 3.1 Test Whether One Additional Linear Constraint Is Sufficient -- 3.2 Finding Pairs of Indistinguishable Points with SMT -- 3.3 Enlarge Pairs of Indistinguishable Points to Convex Regions -- 3.4 Finding a Linear Constraint Separating Pairs of Convex Regions with LP -- 4 Optimizations -- 5 Experimental Results.
6 Conclusion and Further Research -- References -- A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences -- 1 Introduction -- 2 Overview -- 3 Source Language and Its Guarded Form -- 3.1 Input Language -- 3.2 Guarded Language -- 3.3 Translation to Guarded Form -- 4 Structured Differences Between Programs -- 5 Generation Algorithm Directed by Structured Differences -- 6 Implementation and Experiments -- 7 Related Work -- 8 Conclusion -- References -- On Automated Lemma Generation for Separation Logic with Inductive Definitions -- 1 Introduction -- 2 Motivating Example -- 3 Separation Logic with Inductive Definitions -- 4 Composition Lemmas -- 5 Derived Lemmas -- 5.1 The ``Completion'' Lemmas -- 5.2 The ``Stronger'' Lemmas -- 6 A Proof Strategy Based on Lemmas -- 7 Experimental Results -- 8 Related Work -- 9 Conclusion -- References -- Severity Levels of Inconsistent Code -- 1 Introduction -- 2 Overview -- 3 Inconsistent Code -- 4 Severity Levels of Inconsistency -- 5 Algorithm for Categorizing Inconsistent Code -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning the Language of Error -- 1 Introduction -- 2 Preliminaries -- the L* Algorithm -- 3 The Language We Learn -- 4 L* and the Queries -- 4.1 Membership Queries -- 4.2 Conjecture Queries -- 5 Usage Scenarios for the Learning Framework -- 6 System Description and Empirical Evaluation -- 6.1 Optimisations -- 6.2 Implementation and Evaluation -- 7 Conclusions and Future Work -- References -- Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage -- 1 Introduction -- 2 Preliminaries -- 3 Disk-Based State Space Exploration with Partitioning -- 3.1 Representation of MDP in Memory and on Disk -- 3.2 Disk-Based Exploration Using Partitioning -- 4 Disk-Based Partitioned Value Iteration -- 5 Evaluation. 6 Conclusion -- References -- Model Checking Failure-Prone Open Systems Using Probabilistic Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Hierarchical Probabilistic Automata -- 3 Decision Algorithms and Robustness -- 3.1 Forward Algorithm -- 3.2 Backward Algorithm -- 3.3 Forward vs. Backward -- 3.4 Robustness -- 4 Undecidability for 2-HPA -- 5 Modeling Failure-Prone Open Systems -- 6 Implementation and Experiment -- 6.1 Implementation of the Verification Algorithms -- 6.2 Abstracting Models of Web Applications -- 6.3 Experiment -- 7 Conclusions -- References -- Optimal Continuous Time Markov Decisions -- 1 Introduction -- 2 Preliminaries -- 3 Unif+: Optimal Time-Bounded Reachability Revisited -- 3.1 Uniformisation to C -- 3.2 Lower and Upper Bounds on the Value of C -- 3.3 Convergence of the Bounds for Increasing -- 3.4 Extracting the Scheduler -- 4 Existing Algorithms -- 5 Empirical Evaluation and Comparison -- 6 Conclusion -- References -- Spanning the Spectrum from Safety to Liveness -- 1 Introduction -- 2 Preliminaries -- 3 Classes of Safety -- 3.1 Co-safety -- 3.2 Finding the Safety Level -- 4 Finding the Safety Class -- 4.1 Observations on Automata -- 4.2 Expressive Power -- 4.3 Decision Procedures -- 5 Discussion and Directions for Future Research -- References -- Marimba: A Tool for Verifying Properties of Hidden Markov Models -- 1 Introduction -- 2 Tool Architecture and Implementation -- 2.1 Marimba's Input and Modules -- 3 Verification of a Human-Robot Interaction -- 4 Conclusions -- References -- ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols -- 1 Introduction -- 2 Consistency Lemma -- 3 Overview of Our Approach -- 4 Validation and Conclusion -- References -- ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks -- 1 Introduction -- 2 Architecture and Usage. 3 Comparison, Evaluation and Future Developments -- References -- EviCheck: Digital Evidence for Android -- 1 Introduction and Related Work -- 2 EviCheck's Main Ingredients -- 2.1 Policy Language -- 2.2 The Verifier -- 2.3 The Checker -- 2.4 Policy Generator -- 2.5 Technical Discussion -- 3 Implementation and Experiments -- References -- Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant Schedules -- 1 Introduction -- 2 Optimized Scheduler Encoding -- 3 Implementation Details -- 4 Experimental Evaluation and Conclusion -- References -- A Contextual Equivalence Checker for IMJ* -- 1 Introduction -- 2 Tool Architecture -- 3 Evaluation -- References -- Trace Diagnostics Using Temporal Implicants -- 1 Introduction -- 2 Propositional Foundations -- 2.1 Problem Statement -- 2.2 Syntactic and Semantic Formulations -- 2.3 Practical Solution -- 3 Temporal Issues -- 3.1 Syntactic Rewritings -- 3.2 Semantic Restrictions -- 3.3 Sub-models of a Formula -- 3.4 Temporal Implicants -- 4 MTL Diagnostics -- 4.1 Non-Standard MTL Semantics -- 4.2 Explanation Operators -- 4.3 Computation of Selection Functions -- 4.4 Discussion -- 5 LTL Ultimately-Periodic Diagnostics -- 5.1 Recurrent LTL Semantics -- 5.2 Explanation Operators -- 6 Conclusion and Perspectives -- References -- Test Case Generation of Actor Systems -- 1 Introduction -- 2 The Language -- 3 Symbolic Execution -- 4 Less Redundant Exploration in Symbolic Execution -- 5 Generation of Test Cases -- 5.1 Coverage and Termination Criteria for Actor Systems -- 5.2 Test Cases for Actor Systems -- 6 Implementation and Experimental Evaluation -- 7 Related Work and Conclusions -- References -- Lattice-Based Semantics for Combinatorial Model Evolution -- 1 Introduction -- 2 Running Example and Overview -- 3 Preliminaries. 4 Lattice-Based Semantics for Combinatorial Model Evolution -- 5 Atomic Operations on Combinatorial Models -- 5.1 Adding or Removing a Parameter and Its Values -- 5.2 Adding or Removing a Value from an Existing Parameter -- 5.3 Adding, Removing, or Changing a Constraint -- 6 Split and Merge Operations on Combinatorial Models -- 7 Related Work -- 8 Summary and Future Work -- References -- Effective Verification of Replicated Data Types Using Later Appearance Records (LAR) -- 1 Introduction -- 2 CRDTs, Traces and Specifications -- 3 CRDT Implementation -- 3.1 Reference Implementation -- 3.2 Details of the Reference Implementation -- 3.3 Correctness of the Reference Implementation -- 3.4 Bounding the Reference Implementation -- 4 Effective Verification Using Bounded Reference Implementation via CEGAR -- 5 Conclusion -- References -- TSO-to-TSO Linearizability Is Undecidable -- 1 Introduction -- 2 TSO Concurrent Systems -- 2.1 Notations -- 2.2 Libraries and the Most General Clients -- 2.3 TSO Operational Semantics -- 3 TSO-to-TSO Linearizability and Equivalent Characterization -- 3.1 TSO-to-TSO Linearizability -- 3.2 Equivalence Characterization -- 4 Undecidability of TSO-to-TSO Linearizability -- 4.1 Classic-Lossy Single-Channel Systems -- 4.2 Simulation on the TSO Memory Model -- 4.3 Undecidability of History Inclusion -- 4.4 Undecidability of TSO-to-TSO Linearizability -- 5 Conclusion and Future Work -- References -- Formal Verification of Infinite-State BIP Models -- 1 Introduction -- 2 The BIP Model -- 3 ESST for BIP (ESST BIP ) -- 3.1 The ESST Framework -- 3.2 Instantiation of ESST for BIP -- 3.3 Optimizations -- 4 Encoding BIP into Transition System -- 5 Related Work -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- PBMC: Symbolic Slicing for the Verification of Concurrent Programs -- 1 Introduction. 2 Motivating Example. |
| Record Nr. | UNINA-9910484603403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You
| Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You |
| Pubbl/distr/stampa | Bloomington : , : Indiana University Press, 2019 |
| Descrizione fisica | 1 online resource (196 pages) |
| Disciplina | 320.5409471 |
| Altri autori (Persone) |
YouZiying
ZhangLijun |
| Soggetto genere / forma | Electronic books. |
| ISBN |
0-253-04410-3
0-253-04411-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910480474003321 |
| Bloomington : , : Indiana University Press, 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You
| Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You |
| Pubbl/distr/stampa | Bloomington : , : Indiana University Press, 2019 |
| Descrizione fisica | 1 online resource (196 pages) |
| Disciplina | 320.5409471 |
| Altri autori (Persone) |
YouZiying
ZhangLijun |
| Soggetto topico |
Folklore - China
Folklore - Study and teaching - China |
| Soggetto genere / forma | Electronic books. |
| ISBN |
0-253-04412-X
0-253-04410-3 0-253-04411-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910793879203321 |
| Bloomington : , : Indiana University Press, 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You
| Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You |
| Pubbl/distr/stampa | Bloomington : , : Indiana University Press, 2019 |
| Descrizione fisica | 1 online resource (196 pages) |
| Disciplina | 320.5409471 |
| Altri autori (Persone) |
YouZiying
ZhangLijun |
| Soggetto topico |
Folklore - China
Folklore - Study and teaching - China |
| Soggetto genere / forma | Electronic books. |
| ISBN |
0-253-04412-X
0-253-04410-3 0-253-04411-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910824558003321 |
| Bloomington : , : Indiana University Press, 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You
| Chinese Folklore Studies Today : Discourse and Practice / / Lijun Zhang; Ziying You |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Bloomington : , : Indiana University Press, 2019 |
| Descrizione fisica | 1 online resource (196 pages) |
| Disciplina | 320.5409471 |
| Altri autori (Persone) |
YouZiying
ZhangLijun |
| Soggetto topico |
Folklore - China
Folklore - Study and teaching - China |
| Soggetto genere / forma | Electronic books. |
| ISBN |
9780253044129
025304412X 9780253044105 0253044103 9780253044112 0253044111 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cover -- Title Page -- Copyright -- Dedication -- Contents -- Foreword / Chao Gejin -- Acknowledgments -- Introduction: History and Trends of Chinese Folklore Studies / Lijun Zhang and Ziying You -- 1. Disciplinary Tradition, Everyday Life, and Childbirth Negotiation: The Past and Present of Chinese Urban Folklore Studies / Yongyi Yue, Translated by Wenyuan Shao and Yuanhao Zhao -- 2. From "Women" to "Female Folklore Practitioners": The History and Current Trend of Women's Folklore Studies in China / Junxia Wang -- 3. A Semiotics of Song: Fusing Lyrical and Social Narrativesin Contemporary China / Levi S. Gibbs -- 4. Contested Myth, History, and Beliefs: Remaking Yao and Shun's Stories in Hongtong, Shanxi / Ziying You -- 5. Institutional Practice of Heritage-Making: The Transformation of Tulou from Residencesto UNESCO World Heritage Site / Lijun Zhang -- Index. |
| Record Nr. | UNINA-9910975260503321 |
| Bloomington : , : Indiana University Press, 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Dependable software engineering. theories, tools, and applications : 6th international symposium, setta 2020, guangzhou, china, november 24-27, 2020, proceedings / / edited by Jun Pang, Lijun Zhang
| Dependable software engineering. theories, tools, and applications : 6th international symposium, setta 2020, guangzhou, china, november 24-27, 2020, proceedings / / edited by Jun Pang, Lijun Zhang |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2020] |
| Descrizione fisica | 1 online resource (XIII, 203 p. 228 illus., 31 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Formal methods (Computer science)
Computers Software engineering |
| ISBN | 3-030-62822-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Road Ahead for Supervisor Synthesis -- Reentrancy? Yes. Reentrancy bug? No -- Graph Transformation Systems: a Semantics Based on (Stochastic) Symmetric Nets -- Modelling and Implementation of Unmanned Aircraft Collision Avoidance -- Randomized Re nement Checking of Timed I/O Automata -- Computing Linear Arithmetic Representation for Reachability Relation of One-counter Automata -- Compiling FL^{res} on Finite Words -- Symbolic Model Checking with Sentential Decision Diagrams -- Probably Approximately Correct Interpolants Generation -- Symbolic Verification of MPI Programs with Non-deterministic Synchronizations -- Learning Safe Neural Network Controllers with Barrier Certificates -- Software Defect-proneness Prediction Based on Package Cohesion and Coupling Metrics. |
| Record Nr. | UNISA-996418222403316 |
| Cham, Switzerland : , : Springer, , [2020] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Dependable Software Engineering. Theories, Tools, and Applications : 6th International Symposium, SETTA 2020, Guangzhou, China, November 24–27, 2020, Proceedings / / edited by Jun Pang, Lijun Zhang
| Dependable Software Engineering. Theories, Tools, and Applications : 6th International Symposium, SETTA 2020, Guangzhou, China, November 24–27, 2020, Proceedings / / edited by Jun Pang, Lijun Zhang |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XIII, 203 p. 228 illus., 31 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer science Computer engineering Computer networks Logic programming Computer simulation Software Engineering Theory of Computation Computer Engineering and Networks Logic in AI Computer Modelling |
| ISBN | 3-030-62822-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Road Ahead for Supervisor Synthesis -- Reentrancy? Yes. Reentrancy bug? No -- Graph Transformation Systems: a Semantics Based on (Stochastic) Symmetric Nets -- Modelling and Implementation of Unmanned Aircraft Collision Avoidance -- Randomized Re nement Checking of Timed I/O Automata -- Computing Linear Arithmetic Representation for Reachability Relation of One-counter Automata -- Compiling FL^{res} on Finite Words -- Symbolic Model Checking with Sentential Decision Diagrams -- Probably Approximately Correct Interpolants Generation -- Symbolic Verification of MPI Programs with Non-deterministic Synchronizations -- Learning Safe Neural Network Controllers with Barrier Certificates -- Software Defect-proneness Prediction Based on Package Cohesion and Coupling Metrics. |
| Record Nr. | UNINA-9910427673603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
In Pursuit of Presence or Prominence? [[electronic resource] ] : The Prospect of Chinese Banks' Global Expansion and Their Benchmarks / / by Shenglin Ben, Jiefang Yu, Yue Gu, Jiamin Lv, Lijun Zhang, Huichao Gong, Hanting Gu, Qi Shuai
| In Pursuit of Presence or Prominence? [[electronic resource] ] : The Prospect of Chinese Banks' Global Expansion and Their Benchmarks / / by Shenglin Ben, Jiefang Yu, Yue Gu, Jiamin Lv, Lijun Zhang, Huichao Gong, Hanting Gu, Qi Shuai |
| Autore | Ben Shenglin |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Singapore : , : Springer Singapore : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XXVI, 167 p. 41 illus. in color.) |
| Disciplina | 332.1 |
| Collana | Current Chinese Economic Report Series |
| Soggetto topico |
Banks and banking
International finance Banking International Finance |
| ISBN | 981-10-7730-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Chapter 1 Changes in the Domestic and International Economy -- Chapter 2 Status of Chinese Banks’ Internationalization -- Chapter 3. Current Situation of Foreign Banks’ Internationalization -- Chapter 4 Comparison of the overseas expansion between Chinese and Foreign Banks -- Chapter 5 Risk implications with Bank Internationalization -- Chapter 6 The Future Prospects of Chinese Banks Internationalization. |
| Record Nr. | UNINA-9910299652003321 |
Ben Shenglin
|
||
| Singapore : , : Springer Singapore : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part II / / edited by Tomáš Vojnar, Lijun Zhang
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part II / / edited by Tomáš Vojnar, Lijun Zhang |
| Autore | Vojnar Tomáš |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXIII, 413 p. 552 illus., 55 illus. in color.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Algorithms Logic design Logic programming Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Logic Design Logic in AI |
| ISBN | 3-030-17465-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Concurrent and Distributed Systems -- Checking Deadlock-Freedom of Parametric Component-Based Systems -- The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability -- Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude -- Multi-Core On-The-Fly Saturation -- Monitoring and Runtime Verification -- Specification and Efficient Monitoring Beyond STL -- VyPR2: A Framework for Runtime Verification of Python Web Services -- Constraint-based Monitoring of Hyperproperties -- Hybrid and Stochastic Systems -- Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments -- Computing the Expected Execution Time of Probabilistic Workflow Nets -- Shepherding Hordes of Markov Chains -- Optimal Time-Bounded Reachability Analysis for Concurrent Systems -- Synthesis -- Minimal-Time Synthesis for Parametric Timed Automata -- Environmentally-friendly GR(1) Synthesis -- StocHy: automated verification and synthesis of stochastic processes -- Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach -- Symbolic Verification -- iRank: a variable order metric for DEDS subject to linear invariants -- Binary Decision Diagrams with Edge-Specified Reductions -- Effective Entailment Checking for Separation Logic with Inductive Definitions -- Safety and Fault-Tolerant Systems -- Digital Bifurcation Analysis of TCP Dynamics -- Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking -- Measuring Masking Fault-Tolerance -- PhASAR: An Inter-Procedural Static Analysis Framework for C/C++. |
| Record Nr. | UNISA-996466301303316 |
|
Vojnar Tomáš
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
