06879nam 22007935 450 99646578120331620230221150157.01-280-38785-897866135657783-642-14295-810.1007/978-3-642-14295-6(CKB)2550000000015596(SSID)ssj0000446364(PQKBManifestationID)11297669(PQKBTitleCode)TC0000446364(PQKBWorkID)10492148(PQKB)10580752(DE-He213)978-3-642-14295-6(MiAaPQ)EBC3065505(PPN)149072821(EXLCZ)99255000000001559620100709d2010 u| 0engurnn|008mamaatxtccrComputer Aided Verification[electronic resource] 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010, Proceedings /edited by Tayssir Touili, Byron Cook, Paul Jackson1st ed. 2010.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2010.1 online resource (XVI, 676 p. 169 illus.) Theoretical Computer Science and General Issues,2512-2029 ;6174Bibliographic Level Mode of Issuance: Monograph3-642-14294-X Includes bibliographical references and index.Invited Talks -- Policy Monitoring in First-Order Temporal Logic -- Retrofitting Legacy Code for Security -- Quantitative Information Flow: From Theory to Practice? -- Memory Management in Concurrent Algorithms -- Invited Tutorials -- ABC: An Academic Industrial-Strength Verification Tool -- There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code -- Constraint Solving for Program Verification: Theory and Practice by Example -- Session 1. Software Model Checking -- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data -- Termination Analysis with Compositional Transition Invariants -- Lazy Annotation for Program Testing and Verification -- The Static Driver Verifier Research Platform -- Dsolve: Safety Verification via Liquid Types -- Contessa: Concurrency Testing Augmented with Symbolic Analysis -- Session 2. Model Checking and Automata -- Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing -- Efficient Emptiness Check for Timed Büchi Automata -- Session 3. Tools -- Merit: An Interpolating Model-Checker -- Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems -- Jtlv: A Framework for Developing Verification Algorithms -- Petruchio: From Dynamic Networks to Nets -- Session 4. Counter and Hybrid Systems Verification -- Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems -- Safety Verification for Probabilistic Hybrid Systems -- A Logical Product Approach to Zonotope Intersection -- Fast Acceleration of Ultimately Periodic Relations -- An Abstraction-Refinement Approach to Verification of Artificial Neural Networks -- Session 5. Memory Consistency -- Fences in Weak Memory Models -- Generating Litmus Tests for Contrasting Memory Consistency Models -- Session 6. Verification of Hardware and Low Level Code -- Directed Proof Generation for Machine Code -- Verifying Low-Level Implementations of High-Level Datatypes -- Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics -- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification -- Session 7. Tools -- LTSmin: Distributed and Symbolic Reachability -- libalf: The Automata Learning Framework -- Session 8. Synthesis -- Symbolic Bounded Synthesis -- Measuring and Synthesizing Systems in Probabilistic Environments -- Achieving Distributed Control through Model Checking -- Robustness in the Presence of Liveness -- RATSY – A New Requirements Analysis Tool with Synthesis -- Comfusy: A Tool for Complete Functional Synthesis -- Session 9. Concurrent Program Verification I -- Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs -- Automatically Proving Linearizability -- Model Checking of Linearizability of Concurrent List Implementations -- Local Verification of Global Invariants in Concurrent Programs -- Abstract Analysis of Symbolic Executions -- Session 10. Compositional Reasoning -- Automated Assume-Guarantee Reasoning through Implicit Learning -- Learning Component Interfaces with May and Must Abstractions -- A Dash of Fairness for Compositional Reasoning -- SPLIT: A Compositional LTL Verifier -- Session 11. Tools -- A Model Checker for AADL -- PESSOA: A Tool for Embedded Controller Synthesis -- Session 12. Decision Procedures -- On Array Theory of Bounded Elements -- Quantifier Elimination by Lazy Model Enumeration -- Session 13. Concurrent Program Verification II -- Bounded Underapproximations -- Global Reachability in Bounded Phase Multi-stack Pushdown Systems -- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces -- Dynamic Cutoff Detection in Parameterized Concurrent Programs -- Session 14. Tools -- PARAM: A Model Checker for Parametric Markov Models -- Gist: A Solver for Probabilistic Games -- A NuSMV Extension for Graded-CTL Model Checking.Theoretical Computer Science and General Issues,2512-2029 ;6174Computer scienceSoftware engineeringCompilers (Computer programs)Machine theoryArtificial intelligenceComputer networksComputer Science Logic and Foundations of ProgrammingSoftware EngineeringCompilers and InterpretersFormal Languages and Automata TheoryArtificial IntelligenceComputer Communication NetworksComputer science.Software engineering.Compilers (Computer programs).Machine theory.Artificial intelligence.Computer networks.Computer Science Logic and Foundations of Programming.Software Engineering.Compilers and Interpreters.Formal Languages and Automata Theory.Artificial Intelligence.Computer Communication Networks.005.1015113Touili Tayssiredthttp://id.loc.gov/vocabulary/relators/edtCook Byronedthttp://id.loc.gov/vocabulary/relators/edtJackson Pauledthttp://id.loc.gov/vocabulary/relators/edtBOOK996465781203316Computer Aided Verification772228UNISA04500nam 22004813 450 991082256110332120231110225902.0(CKB)4100000011930235(MiAaPQ)EBC28617767(Au-PeEL)EBL28617767(OCoLC)1252420229(OCoLC)1252413486(EXLCZ)99410000001193023520210901d2021 uy 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierPerspectives for Digital Social Innovation to Reshape the European Welfare Systems1st ed. :IOS Press, Incorporated,2021.©2021.1 online resource (358 pages)Emerging Communication: Studies in New Technologies and Practices in Communication ;v.131-64368-157-5 Intro -- Title Page -- Preface -- Notes on Contributors -- Acknowledgements -- Contents -- Perspectives for Digital Social Innovation to Reshape the European Welfare Systems: An Introduction -- Section 1. Holistic Approaches to Innovation of Welfare Eco-Systems -- Shaping the Welfare Society: Unleashing Transformation Through ICT-Enabled Social Innovation -- Positive Innovation Networks -- Networks, Communities and Value Chains in Digital Social Innovation for Social Services -- The Role of ICT-Enabled Social Enterprise for Promoting Social Investment -- Section 2. Emerging Digital Technologies -- Civic Engagement Innovation: How ICTs Shape the Relationship Between State and Citizens -- Innovation Policies and Big Data: Opportunities and Challenges -- Using Data Analytics Results in Practice: Challenges and Solution Directions -- A Model for Evidence-Based Social Policy Making, Driven by Big Data, Dynamic Simulation and Stakeholders Participation -- Section 3. Field Studies -- ICT-Enabled Social Innovation in Children's Services -- Improving Education Environment for Socially Disadvantaged Families Through ICT-Enabled Social Innovation: The Case of Papinotas -- Multi-Stakeholder Digital Collaboration and Social Innovation in Social Services: The Cross Project and the Smart Cities -- Digitalising Public Employment Services: Benefit to Social Justice in the Labour Market? -- Maximizing the Role of Digital Social Innovation in Building the Future of Social Protection Systems -- Subject Index -- Author Index.Social welfare is riddled with ingrained problems that have already defeated all standard approaches, and reform calls for counterintuitive action. Digital Social Innovation (DSI) is primarily about promoting grassroots initiatives to address localized societal problems, and is not normally talked about in relation to welfare reform, but perhaps social innovation initiatives, with their localized and case-based approach, could help to solve the enormous structural problems faced by our welfare democracies today.this book addresses the potential and implications of DSI for the reform of the European welfare state. The 14 papers collected here focus on key issues, such as the nature of social innovation and its effects; scaling up to address structural problems and make systemic change; new social risks and challenges; the role of digital thinking and emerging technologies; public governance approaches; tolerance of institutions; integrating innovation in the welfare system; and the empowerment of marginalized citizens. These topics are examined from an integrated and multi-disciplinary perspective, taking into consideration not only current EU debate on policy trends for social protection, but also the nature of digital transformation and its effects on social change. The book also highlights barriers to adoption, as well as the potential limitations and failures of this emerging approach.Emerging Communication: Studies in New Technologies and Practices in Communication Public welfareTechnological innovationsEuropeEuropefastPublic welfareTechnological innovations361.6/5094Davide F1068401Gaggioli A899271Misuraca G1664459MiAaPQMiAaPQMiAaPQBOOK9910822561103321Perspectives for Digital Social Innovation to Reshape the European Welfare Systems4022504UNINA