Preface
Organization
Risks Management Around Machine Learning Software (Keynote Speech)
Contents
Model Checking and Markov Decision Process
Formal Derivation and Verification of Critical Path Algorithm for Directed Acyclic Graph
1 Introduction
2 PAR Method and PAR Platform
3 Formal Derivation of Critical Path Algorithm
3.1 Describing Formal Specification
3.2 Dividing the Problem
3.3 Constructing Recursive Relation
3.4 Writing Radl Algorithm
3.5 Developing Apla Program
4 Formal Verification of Critical Path Algorithm
4.1 Developing Loop Invariants
4.2 Verifying Correctness of the Loop Statements in the Apla Program
5 Conclusion and Future Work
References
An Approach of Transforming Non-Markovian Reward to Markovian Reward
1 Introduction
2 Background
2.1 Linear Temporal Logic Over Finite Traces
2.2 Markov Decision Process
2.3 Deterministic Finite Automata
3 Transforming NMRDP to MDP
3.1 Non-Markovian Reward
3.2 Transforming each i of TERF into a DFA
3.3 Constructing an MDP from TERF and DFA
3.4 Optimizing the Reward Function of MDP
4 Empirical Evaluation
4.1 Academic Advising
4.2 Triangle Tireworld
5 Summary and Discussion
References
A JPSL Based Model Checking Approach for Java Programs
1 Introduction
2 Preliminaries
2.1 Java Property Specific Language
2.2 Labeled Normal Form Graph
2.3 JPSL to PPTL
2.4 Java Source Code to OOAST
2.5 Multi-property Verification Problems
2.6 Model-Checking with On-The-Fly Strategy
2.7 Counter Example Path
3 Case Study
4 Conclusion
References
Model Analysis and Tool Implementation
Implementation of Matlab matfun Toolkit Based on MSVL
1 Introduction
2 The Design and Implementation of Matfun Toolkit
2.1 MSVL
2.2 Function Implementation Method
3 Application of PCA Implementation
4 Conclusion
References
Extending Visibly Pushdown Automata over Multi-matching Nested Relations
1 Introduction
2 Preliminaries
2.1 Multi-matching Nested Relation
2.2 Word Encoding
3 Multi-matching Visibly Pushdown Automata
3.1 Model
3.2 Determinization
4 Symbolic Multi-matching Visibly Pushdown Automata
4.1 Notations
4.2 Model
5 Conclusion
References
Schedulability Analysis of Rate-Monotonic Algorithm on Concurrent Execution of Digraph Real-Time Tasks
1 Introduction
2 The Digraph Task Model
3 Schedulability Analysis for Digraph Task Models
4 Conclusion and Future Work
References
Formal Specification and Testing
Formalization of Natural Language into PPTL Specification via Neural Machine Translation
1 Introduction
2 Theoretical Basis
2.1 PPTL
2.2 PPTLGenerator
3 Neural Machine Translation
3.1 Encoder Network
3.2 Decoder Network
4 Experiments
5 Related Work
6 Conclusion
References
Testing Program Segments to Detect Runtime Exceptions in Java
1 Introduction
2 Preliminary
2.1 Arithmetic Exceptions in Java
2.2 System Dependency Graph
2.3 Program Slicing
3 Methodology
4 Case Study
5 Related Work
6 Conclusion and Future Work
References
Inferring Exact Domains to Efficiently Generate Valid Test Cases via Testing
1 Introduction
2 Preliminaries
2.1 X.509 Certificate
2.2 Certificate Generation
3 Inferring Exact Domains via Testing
3.1 Obtaining Data Types of Parameters
3.2 Inferring Tight Domains
3.3 Checking the Extensibility of Tight Bounds
4 Experiments
4.1 Experimental Settings
4.2 Parameters and Their Data Types
4.3 Exact Domains Inferred by IED
4.4 Evaluation
5 Related Work
6 Conclusion
References
Algorithms and Verification
Testing and Verifying the Security of COVID-19 CT Images Deep Learning System with Adversarial Attack
1 Introduction
2 Adversarial Attack
2.1 The Concept of Generating Adversarial Sample
2.2 The Classification of Adversarial Sample Generation Methods
3 Experiment
3.1 Datasets
3.2 Deep Learning Model
3.3 Adversarial Attack
4 Discussion
4.1 Results of Experiment
4.2 Formal Methods and Formal Verification
5 Conclusion
References
Verifying and Improving Neural Networks Using Testing-Based Formal Verification
1 Introduction
2 Preliminary
2.1 Principle of TBFV
2.2 Interval Arithmetic and Symbolic Execution
2.3 Verification of Neural Networks
3 Background and Motivation
3.1 Background
3.2 Motivation
4 Methodology
4.1 Overview
4.2 Testing-based Neural Networks Pruning
4.3 Formal Verification and Retraining of Neural Networks
5 Case Study
6 Related Work
7 Conclusion and Future Work
References
Alternating Projection Temporal Epistemic Logic
1 Introduction
2 Preparation
2.1 Concurrent Game Structure and AETS
2.2 Epistemic Logic
3 Alternating Projection Temporal Epistemic Logic
3.1 APTEL Syntax
3.2 APTEL Semantics
3.3 Applications of APTEL
4 Conclusion
References
Author Index