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.
Bridging the Gap Between AI and Reality : First International Conference, AISoLA 2023, Crete, Greece, October 23–28, 2023, Selected Papers / / edited by Bernhard Steffen
| Bridging the Gap Between AI and Reality : First International Conference, AISoLA 2023, Crete, Greece, October 23–28, 2023, Selected Papers / / edited by Bernhard Steffen |
| Edizione | [1st ed. 2025.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2025 |
| Descrizione fisica | 1 online resource (XI, 472 p. 89 illus., 69 illus. in color.) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Software engineering Computers, Special purpose Computer systems Artificial intelligence Computer Science Logic and Foundations of Programming Software Engineering Special Purpose and Application-Based Systems Computer System Implementation Artificial Intelligence |
| ISBN |
9783031737411
3031737415 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Digital Humanities and Cultural Heritage in AI and IT-enabled Environments -- Common Language for Accessibility, Interoperability, and Reusability in Historical Demography -- Coding historical causes of death data with Large Language Models -- Teaching the specialized language of Mathematics with a data-driven approach: what data do we use? -- Interoperating Civil Registration of Death and Census Data: Old Age and Marriage as Categories of Analysis -- From Data Science to Modular Workflows - Changing Perspectives from Data to Platform: DBDIrl 1864-1922 Case Study -- Mapping Madness: HGIS and the granular analysis of Irish patient records -- Digitised historical sources and non-digital humanists: an interdisciplinary challenge? -- Using Passive Sensing to Identify Depression -- The GraphBRAIN Framework for Knowledge Graph Management and its Applications to Cultural Heritage -- Challenges for AI in Healthcare Systems -- Towards a Multi-dimensional Health Data Analysis Framework -- Future Opportunities for Systematic AI Support in Healthcare -- CRISP-PCCP – A Development Methodology Supporting FDA Approval for Machine Learning Enabled Medical Devices -- Model Driven Development for AI-based Healthcare Systems: A Review -- Balancing Transparency and Risk: An Overview of the Security and Privacy Risks of Open-Source Machine Learning Models -- AI-related risk and uncertainty -- Leveraging Actionable Explanations to Improve People’s Reactions to AI-based Decisions -- From Explanation Correctness to Explanation Goodness: Only Provably Correct Explanations can Save the World -- Thinking Outside the Box? Regulatory Sandboxes as a Tool for AI Regulation -- AI and Democratic Equality: How Surveillance Capitalism and Computational Propaganda Threaten Democracy -- Safeguarding AI-Based Software Development and Verification using Witnesses (Position Paper) -- End-to-End AI Generated Runtime Verification from Natural Language Specification -- AI-Assisted Programming with Test-based Refinement -- Safer Than Perception: Increasing Resilience of Automated Vehicles Against Misperception -- Towards ML-Integration and Training Patterns for AI-Enabled Systems -- The Reachability Problem for Neural-Network Control Systems. |
| Record Nr. | UNINA-9910898593403321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2025 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computing and Software Science [[electronic resource] ] : State of the Art and Perspectives / / edited by Bernhard Steffen, Gerhard Woeginger
| Computing and Software Science [[electronic resource] ] : State of the Art and Perspectives / / edited by Bernhard Steffen, Gerhard Woeginger |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIX, 590 p. 774 illus., 54 illus. in color.) |
| Disciplina | 004 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Compilers (Computer programs) Electronic digital computers—Evaluation Algorithms Artificial intelligence Computer Science Software Engineering Compilers and Interpreters System Performance and Evaluation Artificial Intelligence |
| ISBN | 3-319-91908-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466446103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computing and Software Science : State of the Art and Perspectives / / edited by Bernhard Steffen, Gerhard Woeginger
| Computing and Software Science : State of the Art and Perspectives / / edited by Bernhard Steffen, Gerhard Woeginger |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIX, 590 p. 774 illus., 54 illus. in color.) |
| Disciplina | 004 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Compilers (Computer programs) Electronic digital computers—Evaluation Algorithms Artificial intelligence Computer Science Software Engineering Compilers and Interpreters System Performance and Evaluation Artificial Intelligence |
| ISBN | 3-319-91908-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349297603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Correct system design : recent insights and advances / / Ernst-RuÌdiger Olderog, Bernhard Steffen (editors)
| Correct system design : recent insights and advances / / Ernst-RuÌdiger Olderog, Bernhard Steffen (editors) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 422 p.) |
| Disciplina | 004.0684 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer systems - Reliability
System design |
| ISBN | 3-540-48092-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Methodology -- Theories of programming: Top-Down and Bottomup and Meeting in the Middle -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- Real-Time Constraints Through the ProCoS Layers -- Real-Time Constraints Through the ProCoS Layers -- Monotonicity in Calculational Proofs -- Monotonicity in Calculational Proofs -- Programming -- The Alma Project, or How First-Order Logic Can Help us in Imperative Programming -- Type and Effect Systems -- Automation -- Proving Theorems About Java-Like Byte Code -- Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking -- On the Existence of Network Invariants for Verifying Parameterized Systems -- Compilation -- Verification of Compilers -- Translation Validation: From SIGNAL to C -- Compilation and Synthesis for Real-Time Embedded Controllers -- Optimization Under the Perspective of Soundness, Completeness, and Reusability -- Application -- Verification of Automotive Control Units -- Correct Real-Time Software for Programmable Logic Controllers -- Formal Methods for the International Space Station ISS -- METAFrame in Practice: Design of Intelligent Network Services. |
| Record Nr. | UNISA-996465307703316 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Correct system design : recent insights and advances / / Ernst-RuÌdiger Olderog, Bernhard Steffen (editors)
| Correct system design : recent insights and advances / / Ernst-RuÌdiger Olderog, Bernhard Steffen (editors) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 422 p.) |
| Disciplina | 004.0684 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer systems - Reliability
System design |
| ISBN | 3-540-48092-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Methodology -- Theories of programming: Top-Down and Bottomup and Meeting in the Middle -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- A Triptych Software Development Paradigm: Domain, Requirements and Software Towards a Nodel Development of a Decision Support System for Sustainable Development -- Real-Time Constraints Through the ProCoS Layers -- Real-Time Constraints Through the ProCoS Layers -- Monotonicity in Calculational Proofs -- Monotonicity in Calculational Proofs -- Programming -- The Alma Project, or How First-Order Logic Can Help us in Imperative Programming -- Type and Effect Systems -- Automation -- Proving Theorems About Java-Like Byte Code -- Multiple State and Single State Tableaux for Combining Local and Global Nodel Checking -- On the Existence of Network Invariants for Verifying Parameterized Systems -- Compilation -- Verification of Compilers -- Translation Validation: From SIGNAL to C -- Compilation and Synthesis for Real-Time Embedded Controllers -- Optimization Under the Perspective of Soundness, Completeness, and Reusability -- Application -- Verification of Automotive Control Units -- Correct Real-Time Software for Programmable Logic Controllers -- Formal Methods for the International Space Station ISS -- METAFrame in Practice: Design of Intelligent Network Services. |
| Record Nr. | UNINA-9910767573403321 |
| Berlin : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Leveraging Applications of Formal Methods [[electronic resource] ] : First International Symposium, ISoLA 2004, Paphos, Cyprus, October 30 - November 2, 2004, Revised Selected Papers / / edited by Tiziana Maragria, Bernhard Steffen
| Leveraging Applications of Formal Methods [[electronic resource] ] : First International Symposium, ISoLA 2004, Paphos, Cyprus, October 30 - November 2, 2004, Revised Selected Papers / / edited by Tiziana Maragria, Bernhard Steffen |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (VI, 197 p.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer science Compilers (Computer programs) Computers, Special purpose Software Engineering Computer Science Logic and Foundations of Programming Compilers and Interpreters Special Purpose and Application-Based Systems |
| ISBN | 3-540-48929-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interaction and Coordination of Tools for Structured Data -- Modelling Coordination in Biological Systems -- A Rule Markup Language and Its Application to UML -- Using XML Transformations for Enterprise Architectures -- Classification and Utilization of Abstractions for Optimization -- On the Correctness of Transformations in Compiler Back-Ends -- Accurate Theorem Proving for Program Verification -- Designing Safe, Reliable Systems Using Scade -- Decreasing Maintenance Costs by Introducing Formal Analysis of Real-Time Behavior in Industrial Settings -- Static Timing Analysis of Real-Time Operating System Code -- A Case Study in Domain-Customized Model Checking for Real-Time Component Software -- Models for Contract Conformance. |
| Record Nr. | UNISA-996466130303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging applications of formal methods : first international symposium, ISoLA 2004, Paphos, Cyprus, October 30-November 2, 2004 : revised selected papers / / Tiziana Margaria, Bernhard Steffen (eds.)
| Leveraging applications of formal methods : first international symposium, ISoLA 2004, Paphos, Cyprus, October 30-November 2, 2004 : revised selected papers / / Tiziana Margaria, Bernhard Steffen (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2006 |
| Descrizione fisica | 1 online resource (VI, 197 p.) |
| Disciplina | 005.1 |
| Altri autori (Persone) |
Margaria-SteffenTiziana <1964->
SteffenBernhard |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-540-48929-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interaction and Coordination of Tools for Structured Data -- Modelling Coordination in Biological Systems -- A Rule Markup Language and Its Application to UML -- Using XML Transformations for Enterprise Architectures -- Classification and Utilization of Abstractions for Optimization -- On the Correctness of Transformations in Compiler Back-Ends -- Accurate Theorem Proving for Program Verification -- Designing Safe, Reliable Systems Using Scade -- Decreasing Maintenance Costs by Introducing Formal Analysis of Real-Time Behavior in Industrial Settings -- Static Timing Analysis of Real-Time Operating System Code -- A Case Study in Domain-Customized Model Checking for Real-Time Component Software -- Models for Contract Conformance. |
| Altri titoli varianti | ISoLA 2004 |
| Record Nr. | UNINA-9910484570103321 |
| Berlin ; ; New York, : Springer, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
| Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (608 pages) |
| Disciplina | 006.3 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Artificial intelligence
Data mining Electronic data processing |
| ISBN | 3-031-19849-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory -- 5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT -- 4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge -- 5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References.
Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References -- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References -- Selective Presumed Benevolence in Multi-party System Verification -- 1 Introduction -- 2 Smart Contracts, Solidity and Reentrancy -- 3 Semantics of Solidity and Handling of Callbacks -- 4 Presumption of Benevolence -- 4.1 Presuming Benevolence of Oneself -- 4.2 Presuming Benevolence of a Static Group -- 4.3 Presuming Benevolence of a Dynamic Group -- 5 Collaborative Malicious Behaviour -- 6 Conclusions -- References -- On the Pragmatics of Moving from System Models to Program Contracts -- 1 Introduction -- 2 The PGP Server Hagrid -- 3 The Alloy Model -- 4 From Alloy to VCC Contracts -- 4.1 Precondition and Framing Analysis -- 4.2 Translation to Annotated C -- 4.3 Contract Augmentation -- 5 Discussion -- References -- X-by-Construction Meets Runtime Verification. X-by-Construction Meets Runtime Verification -- 1 Motivation -- 2 Aim -- 3 Contributions -- 3.1 CbC: Robustness, Co-piloting, and Digital Twinning -- 3.2 CbC and RV: Configurable and Cyber-Physical Systems -- 3.3 XbC: Security, Resilience, and Consumption Properties -- 3.4 CbC and RV: Reinforcement Learning and Synthesis -- References -- Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime -- 1 Introduction -- 2 Preliminaries -- 3 Adaptive Strategies -- 3.1 Definitions -- 3.2 Computing Adaptive Strategies -- 4 Strongly Adaptive Strategies -- 4.1 Bad Moves -- 4.2 Motivating Example -- 4.3 Definitions -- 4.4 Existence of Strongly Adaptive Strategies -- 4.5 Computing Strongly Adaptive Strategies -- 5 Conclusion -- References -- TriCo-Triple Co-piloting of Implementation, Specification and Tests -- 1 Introduction -- 1.1 Triple Co-piloting at a Glance -- 2 Emerging Trends in Software Technology -- 2.1 Code Synthesis Through Large Language Models -- 2.2 Automated Test Case Generation -- 2.3 Specification Synthesis -- 2.4 Formal Software Verification -- 3 The TriCo Methodology -- 3.1 Envisaged Workflow -- 3.2 Use Cases -- 3.3 Envisaged Technology -- 4 Research Efforts Required for TriCo -- 5 Turning Vision into Reality -- References -- Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins -- 1 Introduction -- 2 Twinned-by-Construction Systems -- 3 Twinning-by-Construction and Temporal Properties -- 4 The Digital Thread as a Temporal Property -- 5 Related Work -- 6 Conclusion -- References -- On Formal Choreographic Modelling: A Case Study in EU Business Processes -- 1 Introduction -- 2 Background -- 3 Legal Provisions -- 4 Formal Models -- 5 From BPMN to Global Choreographies -- 6 Conclusions and Future Work -- References -- Configurable-by-Construction Runtime Monitoring -- 1 Introduction. 2 The Quest of Configurable Runtime Monitoring -- 2.1 Feature-Oriented Example -- 2.2 Challenges -- 2.3 This Paper -- 3 Configurable Automata-Based Monitoring -- 3.1 Preliminaries -- 3.2 Featured Monitors -- 3.3 Synthesizing Featured Monitors -- 3.4 Concise Featured Monitors -- 4 Configurable Stream-Based Monitoring -- 4.1 Preliminaries -- 4.2 Configurable Lola -- 4.3 Family-Based Specification Analysis -- 5 Concluding Remarks -- References -- Runtime Verification of Correct-by-Construction Driving Maneuvers -- 1 Introduction -- 2 Workflow by Example -- 3 Modeling and Verifying Maneuvers with Hybrid Mode Automata -- 3.1 Formalization of Hybrid Mode Automata -- 3.2 Verification Based on Differential Dynamic Logic -- 4 Runtime Verification of HMA Models -- 4.1 Generating Monitor Conditions for Runtime Verification -- 4.2 Simulation -- 5 Evaluation -- 5.1 Case Studies and Setup -- 5.2 Results and Insights -- 6 Related Work -- 7 Conclusion -- References -- Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems -- 1 Introduction -- 2 Preliminary Concepts -- 2.1 Signal Model -- 2.2 Signal Temporal Logic (STL) ch16mn04 -- 3 Exploiting Knowledge of System Dynamics -- 3.1 Motivating Example -- 3.2 System Model -- 3.3 Knowledge of Signal Dynamics -- 3.4 Using Partial Knowledge -- 4 Monitoring Distributed CPS -- 4.1 Distributed CPS Architecture -- 4.2 Additional Challenges in the Distributed Setup -- 5 Using Verified Dynamics -- 6 Conclusion -- References -- Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept -- 1 Introduction -- 2 Background and Related Work -- 2.1 Essentials of Statistical Model Checking -- 2.2 Trace Execution Properties -- 2.3 Probabilistic Verification -- 2.4 SMC Tools -- 3 Illustrative Example -- 3.1 SMC-Based Validation -- 3.2 Using Traces for Automated Program Repair. 4 Designing a Repair Agent -- 4.1 A SMC-Based Program Repair Algorithm -- 5 Implementation and Experimental Results -- 5.1 Experimental Results -- 6 Conclusions and Future Work -- References -- Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty -- 1 Introduction -- 2 Background -- 2.1 Reinforcement Learning (RL) -- 2.2 Simulink and the RL Toolbox -- 2.3 Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 2.5 Stochastic Hybrid Model -- 2.6 Signal Temporal Logic -- 2.7 Learning Optimal Decisions for Stochastic Hybrid Systems -- 3 Related Work -- 4 Combining Deductive and Quantitative Analyses -- 4.1 An Intelligent Water Distribution System -- 4.2 Formal Verification of Safety and Resilience -- 4.3 Resilient Scheduling Under Uncertainty -- 5 Evaluation -- 5.1 Deductive Verification -- 5.2 Quantitative Analysis -- 6 Conclusion -- References -- Non-functional Testing of Runtime Enforcers in Android -- 1 Introduction -- 2 Background -- 2.1 Runtime Policy -- 2.2 Policy Enforcement Models -- 3 Test4Enforcers -- 3.1 Test Case Generation -- 3.2 Test Execution -- 4 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Automata Learning Meets Shielding -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Markov Decision Processes and Reinforcement Learning -- 3.2 Learning of MDPs -- 3.3 Shielding in MDPs -- 4 Learned Shields for Safe RL -- 4.1 Setting and Problem Statement -- 4.2 Overview of Iterative Safe RL via Learned Shields -- 4.3 Details for Training Using Learned Shields -- 5 Experiments -- 5.1 Case Study Subjects -- 5.2 Experimental Results -- 5.3 Zigzag Gridworlds -- 5.4 Slippery Shortcuts Gridworlds -- 5.5 Wall Gridworlds -- 5.6 Discussion -- 6 Conclusion -- References -- Safe Policy Improvement in Constrained Markov Decision Processes -- 1 Introduction. 2 Motivating Example. |
| Record Nr. | UNINA-9910619268603321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors)
| Leveraging applications of formal methods, verification and validation . Part I : verification principles : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings / / Tiziana Margaria and Bernhard Steffen (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (608 pages) |
| Disciplina | 006.3 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Artificial intelligence
Data mining Electronic data processing |
| ISBN | 3-031-19849-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Introduction -- Organization -- Contents - Part I -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- SpecifyThis - Bridging Gaps Between Program Specification Paradigms -- 1 Introduction -- 2 Summary of Contributions -- References -- Deductive Verification Based Abstraction for Software Model Checking -- 1 Introduction -- 2 Overview of the Verification Approach -- 3 Deductive Verification and Frama-C -- 4 Model Checking and TLA -- 4.1 The TLA Framework -- 4.2 Translating Code and Contracts into TLA -- 5 Contracts as a Unifying Theory -- 5.1 An Abstract Contract Theory -- 5.2 Deductive Verification in the Abstract Contract Theory -- 5.3 Procedure-Modular Verification with TLA -- 5.4 Contract Based System Design -- 6 Preliminary Evaluation -- 6.1 Simple File Open-Close Example -- 6.2 Simplified Industrial Example -- 7 Conclusion -- References -- Abstraction in Deductive Verification: Model Fields and Model Methods -- 1 Introduction -- 2 Logical Encoding of Local Computations -- 3 Encoding Heap Access and Update-Previous and Related Work -- 3.1 Notation -- 3.2 Heaps as Maps -- 3.3 Arrays -- 3.4 Embedding in SMT -- 4 Model Fields and Model Methods -- 5 Simple Example -- 6 Using Model Methods -- 7 Encoding Model Methods -- 8 Contrast and Conclusion -- References -- A Hoare Logic with Regular Behavioral Specifications -- 1 Introduction -- 2 Motivation -- 3 Approach -- 3.1 Preliminaries and Notation -- 3.2 Regular Behavioral Specifications -- 3.3 Programs and Behavioral Correctness -- 3.4 Hoare Logic Proof Rules -- 4 Tool Support in SecC -- 4.1 Specification Syntax -- 4.2 Verification Engine -- 5 Case Studies -- 5.1 Case Study: Regular Expression Matching -- 5.2 Case-Study: VerifyThis Casino Challenge -- 5.3 Discussion -- 6 Related and Alternative Approaches -- 7 Conclusion -- References.
Specification-Based Monitoring in C++ -- 1 Introduction -- 2 Related Work -- 3 Overview -- 4 The Specification Language -- 4.1 Events -- 4.2 A Simple State Machine -- 4.3 Some Alternative Monitors -- 4.4 Monitoring Events that Carry Data -- 4.5 Referring to the Past -- 4.6 A Complex Property -- 4.7 The Complete Grammar -- 5 Usage -- 6 Implementation -- 7 Experiment -- 7.1 Setting Up the Experiment -- 7.2 Result and Interpretation -- 8 Conclusion -- A Visualization of Monitors -- References -- Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS -- 1 Introduction -- 2 Specifying Termination Detection -- 3 Verification by Model Checking and Theorem Proving -- 3.1 Finite-State Model Checking Using tlc -- 3.2 Bounded Model Checking with Apalache -- 3.3 Theorem Proving Using tlaps -- 4 Safra's Algorithm for Termination Detection -- 5 Analyzing Safra's Algorithm -- 5.1 Model Checking Correctness Properties -- 5.2 Safra's Algorithm Implements Termination Detection -- 5.3 Proving Correctness Using tlaps -- 6 Conclusion -- References -- Selective Presumed Benevolence in Multi-party System Verification -- 1 Introduction -- 2 Smart Contracts, Solidity and Reentrancy -- 3 Semantics of Solidity and Handling of Callbacks -- 4 Presumption of Benevolence -- 4.1 Presuming Benevolence of Oneself -- 4.2 Presuming Benevolence of a Static Group -- 4.3 Presuming Benevolence of a Dynamic Group -- 5 Collaborative Malicious Behaviour -- 6 Conclusions -- References -- On the Pragmatics of Moving from System Models to Program Contracts -- 1 Introduction -- 2 The PGP Server Hagrid -- 3 The Alloy Model -- 4 From Alloy to VCC Contracts -- 4.1 Precondition and Framing Analysis -- 4.2 Translation to Annotated C -- 4.3 Contract Augmentation -- 5 Discussion -- References -- X-by-Construction Meets Runtime Verification. X-by-Construction Meets Runtime Verification -- 1 Motivation -- 2 Aim -- 3 Contributions -- 3.1 CbC: Robustness, Co-piloting, and Digital Twinning -- 3.2 CbC and RV: Configurable and Cyber-Physical Systems -- 3.3 XbC: Security, Resilience, and Consumption Properties -- 3.4 CbC and RV: Reinforcement Learning and Synthesis -- References -- Robustness-by-Construction Synthesis: Adapting to the Environment at Runtime -- 1 Introduction -- 2 Preliminaries -- 3 Adaptive Strategies -- 3.1 Definitions -- 3.2 Computing Adaptive Strategies -- 4 Strongly Adaptive Strategies -- 4.1 Bad Moves -- 4.2 Motivating Example -- 4.3 Definitions -- 4.4 Existence of Strongly Adaptive Strategies -- 4.5 Computing Strongly Adaptive Strategies -- 5 Conclusion -- References -- TriCo-Triple Co-piloting of Implementation, Specification and Tests -- 1 Introduction -- 1.1 Triple Co-piloting at a Glance -- 2 Emerging Trends in Software Technology -- 2.1 Code Synthesis Through Large Language Models -- 2.2 Automated Test Case Generation -- 2.3 Specification Synthesis -- 2.4 Formal Software Verification -- 3 The TriCo Methodology -- 3.1 Envisaged Workflow -- 3.2 Use Cases -- 3.3 Envisaged Technology -- 4 Research Efforts Required for TriCo -- 5 Turning Vision into Reality -- References -- Twinning-by-Construction: Ensuring Correctness for Self-adaptive Digital Twins -- 1 Introduction -- 2 Twinned-by-Construction Systems -- 3 Twinning-by-Construction and Temporal Properties -- 4 The Digital Thread as a Temporal Property -- 5 Related Work -- 6 Conclusion -- References -- On Formal Choreographic Modelling: A Case Study in EU Business Processes -- 1 Introduction -- 2 Background -- 3 Legal Provisions -- 4 Formal Models -- 5 From BPMN to Global Choreographies -- 6 Conclusions and Future Work -- References -- Configurable-by-Construction Runtime Monitoring -- 1 Introduction. 2 The Quest of Configurable Runtime Monitoring -- 2.1 Feature-Oriented Example -- 2.2 Challenges -- 2.3 This Paper -- 3 Configurable Automata-Based Monitoring -- 3.1 Preliminaries -- 3.2 Featured Monitors -- 3.3 Synthesizing Featured Monitors -- 3.4 Concise Featured Monitors -- 4 Configurable Stream-Based Monitoring -- 4.1 Preliminaries -- 4.2 Configurable Lola -- 4.3 Family-Based Specification Analysis -- 5 Concluding Remarks -- References -- Runtime Verification of Correct-by-Construction Driving Maneuvers -- 1 Introduction -- 2 Workflow by Example -- 3 Modeling and Verifying Maneuvers with Hybrid Mode Automata -- 3.1 Formalization of Hybrid Mode Automata -- 3.2 Verification Based on Differential Dynamic Logic -- 4 Runtime Verification of HMA Models -- 4.1 Generating Monitor Conditions for Runtime Verification -- 4.2 Simulation -- 5 Evaluation -- 5.1 Case Studies and Setup -- 5.2 Results and Insights -- 6 Related Work -- 7 Conclusion -- References -- Leveraging System Dynamics in Runtime Verification of Cyber-Physical Systems -- 1 Introduction -- 2 Preliminary Concepts -- 2.1 Signal Model -- 2.2 Signal Temporal Logic (STL) ch16mn04 -- 3 Exploiting Knowledge of System Dynamics -- 3.1 Motivating Example -- 3.2 System Model -- 3.3 Knowledge of Signal Dynamics -- 3.4 Using Partial Knowledge -- 4 Monitoring Distributed CPS -- 4.1 Distributed CPS Architecture -- 4.2 Additional Challenges in the Distributed Setup -- 5 Using Verified Dynamics -- 6 Conclusion -- References -- Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept -- 1 Introduction -- 2 Background and Related Work -- 2.1 Essentials of Statistical Model Checking -- 2.2 Trace Execution Properties -- 2.3 Probabilistic Verification -- 2.4 SMC Tools -- 3 Illustrative Example -- 3.1 SMC-Based Validation -- 3.2 Using Traces for Automated Program Repair. 4 Designing a Repair Agent -- 4.1 A SMC-Based Program Repair Algorithm -- 5 Implementation and Experimental Results -- 5.1 Experimental Results -- 6 Conclusions and Future Work -- References -- Towards Safe and Resilient Hybrid Systems in the Presence of Learning and Uncertainty -- 1 Introduction -- 2 Background -- 2.1 Reinforcement Learning (RL) -- 2.2 Simulink and the RL Toolbox -- 2.3 Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 2.5 Stochastic Hybrid Model -- 2.6 Signal Temporal Logic -- 2.7 Learning Optimal Decisions for Stochastic Hybrid Systems -- 3 Related Work -- 4 Combining Deductive and Quantitative Analyses -- 4.1 An Intelligent Water Distribution System -- 4.2 Formal Verification of Safety and Resilience -- 4.3 Resilient Scheduling Under Uncertainty -- 5 Evaluation -- 5.1 Deductive Verification -- 5.2 Quantitative Analysis -- 6 Conclusion -- References -- Non-functional Testing of Runtime Enforcers in Android -- 1 Introduction -- 2 Background -- 2.1 Runtime Policy -- 2.2 Policy Enforcement Models -- 3 Test4Enforcers -- 3.1 Test Case Generation -- 3.2 Test Execution -- 4 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Automata Learning Meets Shielding -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Markov Decision Processes and Reinforcement Learning -- 3.2 Learning of MDPs -- 3.3 Shielding in MDPs -- 4 Learned Shields for Safe RL -- 4.1 Setting and Problem Statement -- 4.2 Overview of Iterative Safe RL via Learned Shields -- 4.3 Details for Training Using Learned Shields -- 5 Experiments -- 5.1 Case Study Subjects -- 5.2 Experimental Results -- 5.3 Zigzag Gridworlds -- 5.4 Slippery Shortcuts Gridworlds -- 5.5 Wall Gridworlds -- 5.6 Discussion -- 6 Conclusion -- References -- Safe Policy Improvement in Constrained Markov Decision Processes -- 1 Introduction. 2 Motivating Example. |
| Record Nr. | UNISA-996495569403316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen
| Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (505 pages) |
| Disciplina | 006.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer programming Compilers (Computer programs) Application software Software Engineering Artificial Intelligence Programming Techniques Compilers and Interpreters Computer and Information Systems Applications |
| ISBN | 3-030-89159-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | STRESS - Introduction -- An Introduction to Graphical Modeling of CI/CD Workflows with Rig -- Pyrus: an Online Modeling Environment for No-Code Data-Analytics Service Composition -- Integrating External Services in DIME -- Asking Why -- Formal Methods for a Digital Industry: Industrial Day at ISoLA 2021 -- Agile Business Engineering: From Transformation Towards Continuous Innovation -- Towards Living Canvases -- Use Cases for Simulation in the Development of Automated Driving Systems -- Simulation-based Elicitation of Accuracy Requirements for the Environmental Perception of Autonomous Vehicles -- DSLs and Middleware Platforms in a Model-Driven Development Approach for Secure Predictive Maintenance Systems in Smart Factories -- From Requirements to Executable Rules: An Ensemble of Domain-Specific Languages for Programming Cyber-Physical Systems in Warehouse Logistics -- Mining Data Quality Rules for Data Migrations: A Case Study on Material Master Data -- Programming - What is Next? -- Low-Code is Often High-Code, So We Must Design Low-Code Platforms to Enable Proper Software Engineering -- Time for All Programs, Not Just Real-Time Programs -- Integrated Modeling and Development of Component-Based Embedded Software in Scala -- Slang: The Sireum Programming Language -- HAMR: An AADL Multi-Platform Code Generation Toolset -- Fundamental Constructs in Programming Languages -- Introducing Dynamical Systems and Chaos Early in Computer Science and Software Engineering Education can Help Advance Theory and Practice of Software Development and Computing -- GATE: Gradual Effect Types -- Fixing Classification: A Viewpoint-based Approach -- The Future of Programming and Modelling: a Vision -- Towards Model-based Intent-Driven Adaptive Software -- The Interoperability Challenge: Building a model driven Digital Thread platform for CPS -- Programming vs. That Thing Subject Matter Experts Do -- Aligned, Purpose-Driven Cooperation: The Future Way of System Development -- RAILS: Roadmaps for AI integration in the raiL Sector -- A Journey through Software Model Checking of Interlocking Programs -- Supporting the Development of Hybrid ERTMS/ETCS Level 3 with Formal Modelling, Analysis and Simulation -- Formal Methods in Railway Signalling Infrastructure Standardisation Processes -- sVerify: Verifying Smart Contracts through Lazy Annotation and Learning -- Verifying temporal properties of stigmergic collective systems using CADP. |
| Record Nr. | UNISA-996464522603316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
