Bridging the Gap Between AI and Reality: First International Conference, AISoLA 2023, Crete, Greece, October 23–28, 2023, Proceedings (Lecture Notes in Computer Science)

Preface
Organization
Contents
Panels and Keynotes
	DigHum Panel. Beyond Chat-GPT: The Impact of AI on Academic Research
	Technology and Democracy
		Summary
	Education and AI – Current Status, Opportunities and Challenges
	The Human-or-Machine Matter: Turing-Inspired Reflections on an Everyday Issue (Brief Summary of Paper)
	Graph Neural Networks: Everything Is Connected
Deep Neural Networks, Explanations, and Rationality
	1 Imperfect Intelligence
	2 Explainable AI
	3 Fear
	4 Conclusions
	References
Verification Meets Learning and Statistics
Welcome Remarks from AISoLA 2023/Track C2 Chairs
	References
Shielded Reinforcement Learning for Hybrid Systems *-6pt
	1 Introduction
	2 Euclidian and Hybrid Markov Decision Processes
	3 Safety, Partitioning, Synthesis and Shielding
	4 Experiments
	5 Conclusion
	References
What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety-Critical Systems
	1 Introduction
	2 Challenges in Engineering Safety-Critical Systems Integrating Learning-Enabled Components
	3 Research Challenges
		3.1 Uncertainty
		3.2 Size and Complexity of the AI Models
		3.3 Lack of Novel Analysis Methods that Are both Rigorous and Efficient
	4 Methodology
		4.1 State-of-the-Art 1: A Design and Co-Simulation Framework
		4.2 Properties and Specifications at Different Levels
		4.3 Guarantees Achieved at Component Levels
		4.4 State-of-the-Art 2: Offline V and V Methods and Guarantee
	5 Conclusion
	References
DeepAbstraction++: Enhancing Test Prioritization Performance via Combined Parameterized Boxes
	1 Introduction
	2 Background
		2.1 Runtime Monitors
		2.2 Gini Index
		2.3 DeepAbstraction
	3 Problem Analysis
		3.1 Clustering
		3.2 Tau Selection Issue
	4 Approach
		4.1 Combined Parameterized Boxes
		4.2 Combination Strategy
		4.3 Illustrative Example
	5 Experimental Setup
	6 Experimental Evaluation
		6.1 Weights Effectiveness
		6.2 Algorithms Effectiveness
		6.3 Performance Stability
		6.4 Combination Strategy Selection
	7 Conclusion and Future Work
	References
Shielded Learning for Resilience and Performance Based on Statistical Model Checking in Simulink
	1 Introduction
	2 Background
		2.1 Reinforcement Learning (RL)
		2.2 Simulink and the RL Toolbox
		2.3 Differential Dynamic Logic and Simulink2dL
		2.4 Statistical Model Checking and Encoding of Properties
	3 Related Work
	4 Shielded SMC-Based Learning in Simulink
		4.1 Approach
		4.2 Intelligent Water Distribution System in Simulink
		4.3 Stochastic Extensions for Modeling Pump Failures and Repairs
		4.4 Formal Verification of Safety and Resilience Contracts
		4.5 Performability Subsystem and SMC-Based Learning
	5 Evaluation of Results and Validation
		5.1 Model Parameters
		5.2 Settings for Simulink and SMC-Based Learning
		5.3 Optimizing Resilience
		5.4 Optimizing Performance
	6 Conclusion
	References
Formal XAI via Syntax-Guided Synthesis
	1 Introduction
	2 Illustrative Example
	3 Preliminaries
	4 Synthesizing Mimic Programs
		4.1 Semantic Constraints for Mimic Programs
		4.2 Syntactic Constraints for Mimic Programs
	5 Experimental Evaluation
		5.1 MNIST Dataset
		5.2 Pima Indians Diabetes Dataset
	6 Related Work
	7 Conclusion
	References
Differential Safety Testing of Deep RL Agents Enabled by Automata Learning
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Markov Decision Processes
	4 Learning-Based Differential Testing of RL Agents
		4.1 Setting
		4.2 Overview
		4.3 Automata Learning
		4.4 Test-Case Generation
		4.5 Test-Case Execution
	5 Experiments
		5.1 Setup
		5.2 Results
	6 Conclusion
	References
gRoMA: A Tool for Measuring the Global Robustness of Deep Neural Networks
	1 Introduction
	2 Related Work
	3 DNNs and Adversarial Robustness
	4 Introducing the gRoMA Tool
	5 Evaluation
	6 Conclusion and Future Work
	References
Optimized Smart Sampling
	1 Introduction
	2 Background
	3 The Lightweight Scheduler Approach
		3.1 The Original Smart Sampling Algorithm from ch8DLST15
		3.2 Beyond the First Implementation of the Smart Sampling Algorithm
	4 New Lightweight Algorithms for Statistical Model Checking
		4.1 Modification of the Chernoff Bound Test
		4.2 Other Optimizations
	5 Conclusion
	References
Towards a Formal Account on Negative Latency
	1 Introduction
	2 Preliminaries
	3 Predictions in Markov Decision Processes
		3.1 Prediction Quality Criteria
		3.2 k-Predictions
		3.3 Cost-Aware Predictions
		3.4 Negative Latency
	4 Machine Learning for Negative Latency
		4.1 Strategy Estimation
		4.2 Supervised Learning
	5 Concluding Remarks
	References
Safety Verification of DNNs
Track C1: Safety Verification of Deep Neural Networks (DNNs)
	1 Description of the Track
	2 Verification of Neural Networks and Autonomous Systems
	3 Verification Benchmarks
	4 Summary and Outlook
	References
Formal Verification of a Neural Network Based Prognostics System for Aircraft Equipment
	1 Introduction
	2 Remaining Useful Life Estimator
	3 Property Formalization
		3.1 Stability Properties
		3.2 Monotonicity Properties
	4 Verification Methods
	5 Verification Results
		5.1 Reduction of Global Properties to Local Properties
		5.2 Stability Verification
		5.3 Monotonicity Verification
	6 Conclusion and Future Work
	References
The Inverse Problem for Neural Networks
	1 Introduction
		1.1 Related Work
	2 The Preimage of a Piecewise-Affine Neural Network
		2.1 Preliminaries
		2.2 Inverse Affine Map
		2.3 Inverse Piecewise-Affine Activation Function
		2.4 Inverse Piecewise-Affine DNN
	3 Applications and Extensions
		3.1 Interpretability
		3.2 Approximation Schemes
		3.3 Forward-Backward Computation
	4 Conclusion
	References
Continuous Engineering for Trustworthy Learning-Enabled Autonomous Systems
	1 Introduction
	2 Design Flow for Trustable Learning Components
		2.1 Trustworthy Perception and Sensing
		2.2 Safe Data-Driven Control
		2.3 Trustworthy Updates of LECs
	3 Design Flow for LEAS
		3.1 Requirements and Formal Specifications
		3.2 Simulation-Based Modeling, Testing and Monitoring at Design Time
		3.3 Deployment, Operation and Analysis of LEAS at Runtime
		3.4 Assurance Cases for LEAS
	4 Case Studies Demonstrating the FOCETA Methodology
		4.1 Traffic Speed Detection and Path Lane Following
		4.2 Safe and Secure Intelligent Automated Valet Parking
		4.3 Anaesthetic Drug Target Control Infusion
	5 Conclusion
	References
Benchmarks: Semantic Segmentation Neural Network Verification and Objection Detection Neural Network Verification in Perceptions Tasks of Autonomous Driving
	1 Introduction
	2 Related Work
	3 Semantic Segmentation Benchmark–Carvana Unet
	4 Patch-Level Object Detection Benchmark–CCTSDB YOLO
	5 Experiments
	6 Conclusion
	A  Network Details
	B  Implementation Details
	References
Benchmark: Neural Network Malware Classification
	1 Introduction
	2 Preliminaries
		2.1 Feature Datasets
		2.2 Image Datasets
		2.3 Robustness
	3 Benchmarks
		3.1 Malware Feature Benchmark
		3.2 Malware Image Benchmark
	4 Benchmark Demonstration
	5 Conclusion
	References
Benchmark: Remaining Useful Life Predictor for Aircraft Equipment
	1 Introduction
	2 Model Description
	3 Properties Description
		3.1 Stability Properties
		3.2 Monotonicity Properties
		3.3 If-Then Properties
	4 Concluding Remarks
	References
Benchmark: Object Detection for Maritime Search and Rescue
	1 Introduction
	2 Model Description
	3 Property Description
		3.1 Robustness Properties Overview
		3.2 Robustness Properties for the YOLO Model
	4 Property Generation
	5 Concluding Remarks
	References
Benchmark: Formal Verification of Semantic Segmentation Neural Networks
	1 Introduction
	2 Benchmark Design
		2.1 Philosophy
		2.2 Datasets
		2.3 Neural Network Models
		2.4 Segmentation in the Context of Proposed Datasets
		2.5 Adversarial Attacks
		2.6 Evaluation Metrics
		2.7 Robustness Property Specification
		2.8 Verification Property Specifications in Vnnlib Files: Illustrated with an Example
	3 Evaluation
		3.1 Reachability Analysis
		3.2 Neural Network Verification (NNV) Tool
		3.3 Results
	4 Conclusion and Future Ideas
	References
Empirical Analysis of Benchmark Generation for the Verification of Neural Network Image Classifiers
	1 Introduction
	2 Related Work
	3 Evaluation
	4 Results
		4.1 Initialization
		4.2 Regularization
		4.3 Random Seed
	5 Discussion
	6 Conclusion
	A  Appendix
	References
AI Assisted Programming
AI Assisted Programming
	1 Introduction
	2 Contributions
		2.1 Talks with Papers in the Proceedings
		2.2 Talks Without Papers in the Proceedings
	3 Conclusion
	References
Large Language Model Assisted Software Engineering: Prospects, Challenges, and a Case Study
	1 Introduction
	2 LLMs in Software Engineering: Prospects and State-of-the-Art
		2.1 Requirements Engineering
		2.2 System Design
		2.3 Code Generation
		2.4 Quality Assurance, Testing and Verification
	3 Case Study
		3.1 Requirements
		3.2 Design
		3.3 Testing
		3.4 Discussion
	4 Challenges in Adopting LLMs for Software Engineering
		4.1 Integration with Large Context
		4.2 Evaluating and Testing Generative Outputs
		4.3 Challenges in Practical Use
	5 What Could Happen if the Challenges Are Resolved?
	6 Concluding Remarks
	References
ChatGPT in the Loop: A Natural Language Extension for Domain-Specific Modeling Languages
	1 Motivation and Introduction
	2 Preliminaries
		2.1 Language-Driven Engineering
		2.2 LLMs and Programming
		2.3 Learning-Based Testing
	3 Concept
		3.1 Goals
		3.2 Language Integration
		3.3 Contextualization
		3.4 Validation and Feedback
	4 Example Implementation
		4.1 Model Decomposition
		4.2 Graphical Modelling
		4.3 Prompt Frame and Generation Frame
		4.4 Resulting Web Application
		4.5 Model Learning and Verification
	5 Discussion and Related Work
	6 Conclusion
	References
What Can Large Language Models Do for Theorem Proving and Formal Methods?
	1 Introduction
	2 Automated Conjecturing
		2.1 Case Study: Theory Exploration in GPT-4
	3 Conclusions and Further Work
	References
Integrating Distributed Component-Based Systems Through Deep Reinforcement Learning
	1 Introduction
	2 Preliminaries
	3 The Proposed Approach
		3.1 Overview
		3.2 Suggested Deep Learning Architecture
		3.3 An Extension of the Proposed Approach to the Advanced Model
	4 Experiments
		4.1 Experiments with the Simplified Model
		4.2 Experiments with the Advanced Model
	5 Conclusion
	References
Automotive Driving
Safe AI in Autonomous Vehicles
	References
Responsible and Trustworthy AI
Normative Perspectives on and Societal Implications of AI Systems
	1 Motivation
	2 Program
Nature of AI-Based Systems
The Nature of AI-Based Systems Track Introduction
Digital Humanities
Digital Humanities and Cultural Heritage in AI and IT-Enabled Environments
RAISE
Research in Advanced Low-Code/No-Code Application Development: Aspects Around the R@ISE Approach
Extended Abstracts
Distribution-Aware Neuro-Symbolic Verification
	Abstract
	1 Introduction
	2 Applications
		2.1 Verification within the Data Distribution
		2.2 Verification of Correct Epistemic Uncertainty Quantification
	References
Towards Verification of Changes in Dynamic Machine Learning Models Using Deep Ensemble Anomaly Detection
	Abstract
Benchmark: Neural Networks for Anomaly Detection in Batch Distillation
	Reference
AI-Assisted Programming with Test-Based Refinement
	Abstract
Author Index