top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
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
Opac: Controlla la disponibilità qui
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
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. UNINA-9910484603403321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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 0-253-04412-X
0-253-04410-3
0-253-04411-1
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-9910866398203321
Bloomington : , : Indiana University Press, 2019
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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. UNINA-9910427673603321
Cham, Switzerland : , : Springer, , [2020]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui
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
Opac: Controlla la disponibilità qui