| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466073903316 |
|
|
Titolo |
Brainlesion: Glioma, Multiple Sclerosis, Stroke and Traumatic Brain Injuries [[electronic resource] ] : 4th International Workshop, BrainLes 2018, Held in Conjunction with MICCAI 2018, Granada, Spain, September 16, 2018, Revised Selected Papers, Part II / / edited by Alessandro Crimi, Spyridon Bakas, Hugo Kuijf, Farahani Keyvan, Mauricio Reyes, Theo van Walsum |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2019.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XXI, 521 p. 231 illus., 187 illus. in color.) |
|
|
|
|
|
|
Collana |
|
Image Processing, Computer Vision, Pattern Recognition, and Graphics ; ; 11384 |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Optical data processing |
Health informatics |
Machine learning |
Computer communication systems |
Pattern recognition |
Bioinformatics |
Image Processing and Computer Vision |
Health Informatics |
Machine Learning |
Computer Communication Networks |
Pattern Recognition |
Computational Biology/Bioinformatics |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Nota di contenuto |
|
Brain lesion image analysis.-Brain tumor image segmentation -- Ischemic stroke lesion image segmentation -- Grand challenge on MR brain segmentation -- Computational precision medicine -- Stroke workshop on imaging and treatment challenges. . |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
This two-volume set LNCS 11383 and 11384 constitutes revised |
|
|
|
|
|
|
|
|
|
|
|
|
selected papers from the 4th International MICCAI Brainlesion Workshop, BrainLes 2018, as well as the International Multimodal Brain Tumor Segmentation, BraTS, Ischemic Stroke Lesion Segmentation, ISLES, MR Brain Image Segmentation, MRBrainS18, Computational Precision Medicine, CPM, and Stroke Workshop on Imaging and Treatment Challenges, SWITCH, which were held jointly at the Medical Image Computing for Computer Assisted Intervention Conference, MICCAI, in Granada, Spain, in September 2018. The 92 papers presented in this volume were carefully reviewed and selected from 95 submissions. They were organized in topical sections named: brain lesion image analysis; brain tumor image segmentation; ischemic stroke lesion image segmentation; grand challenge on MR brain segmentation; computational precision medicine; stroke workshop on imaging and treatment challenges. |
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996465602503316 |
|
|
Titolo |
Computer Aided Verification [[electronic resource] ] : 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings / / edited by Thomas Ball, Robert B. Jones |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2006.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XV, 564 p.) |
|
|
|
|
|
|
Collana |
|
Theoretical Computer Science and General Issues, , 2512-2029 ; ; 4144 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computer science |
Software engineering |
Machine theory |
Artificial intelligence |
Logic design |
Theory of Computation |
Computer Science Logic and Foundations of Programming |
Software Engineering |
Formal Languages and Automata Theory |
Artificial Intelligence |
Logic Design |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Invited Talks -- Formal Specifications on Industrial-Strength Code—From Myth to Reality -- I Think I Voted: E-Voting vs. Democracy -- Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based Programs -- The Ideal of Verified Software -- Session 1. Automata -- Antichains: A New Algorithm for Checking Universality of Finite Automata -- Safraless Compositional Synthesis -- Minimizing Generalized Büchi Automata -- Session 2. Tools Papers -- Ticc: A Tool for Interface Compatibility and Composition -- FAST Extended Release -- Session 3. Arithmetic -- Don’t Care Words with an Application to the Automata-Based Approach for Real Addition -- A Fast Linear-Arithmetic Solver for DPLL(T) -- Session 4. SAT and Bounded Model Checking -- Bounded Model Checking for Weak Alternating Büchi Automata -- Deriving Small Unsatisfiable Cores with Dominators -- Session 5. Abstraction/Refinement -- Lazy Abstraction with Interpolants -- Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop -- Counterexamples with Loops for Predicate Abstraction -- Session 6. Tools Papers -- cascade: C Assertion Checker and Deductive Engine -- Yasm: A Software Model-Checker for Verification and Refutation -- Session 7. Symbolic Trajectory Evaluation -- SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation -- Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation -- Session 8. Property Specification and Verification -- Some Complexity Results for SystemVerilog Assertions -- Check It Out: On the Efficient Formal Verification of Live Sequence Charts -- Session 9. Time -- Symmetry Reduction for Probabilistic Model Checking -- Communicating Timed Automata: The More Synchronous, the More Difficult to Verify -- Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis -- Session 10. Tools Papers -- DiVinE – A Tool for Distributed Verification -- EverLost: A Flexible Platform for Industrial-Strength Abstraction-Guided Simulation -- Session 11. Concurrency -- Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions -- Model Checking Multithreaded Programs with Asynchronous Atomic Methods -- Causal Atomicity -- Session 12. Trees, Pushdown Systems and Boolean Programs -- Languages of Nested Trees -- Improving Pushdown System Model Checking -- Repair of Boolean Programs with an Application to C -- Session 13. Termination -- Termination of Integer Linear Programs -- Automatic Termination Proofs for Programs with Shape-Shifting Heaps -- Termination Analysis with Calling Context Graphs -- Session 14. Tools Papers -- Terminator: Beyond Safety -- CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking Tools -- Session 15. Abstract Interpretation -- SMT Techniques for Fast Predicate Abstraction -- The Power of Hybrid Acceleration -- Lookahead Widening -- Session 16. Tools Papers -- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover -- LEVER: A Tool for Learning Based Verification -- Session 17. Memory Consistency -- Formal Verification of a Lazy Concurrent List-Based Set Algorithm -- Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study -- Fast and Generalized Polynomial Time Memory Consistency Verification -- Session 18. Shape Analysis -- Programs with Lists Are Counter Automata -- Lazy Shape Analysis -- Abstraction for Shape Analysis with Fast and Precise |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
3. |
Record Nr. |
UNIORUON00013090 |
|
|
Autore |
LEVY, André |
|
|
Titolo |
Inventaire analityque et critique du conte chinois en langue vulgaire / André Lévy |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Paris, : Collège de France Institut des Hautes Etudes Chinois, [1978-1981] |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Descrizione fisica |
|
|
|
|
|
|
Classificazione |
|
|
|
|
|
|
Soggetti |
|
LETTERATURA CINESE - NARRATIVA - ANTOLOGIE - SEC. XVII |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
I v. 2-4 in collaborazione con altri autori. Le date di pubb. si riferiscono a quelle di stampa] |
|
|
|
|
|
|
|
| |