Titlebook: Dependable Software Engineering. Theories, Tools, and Applications; 6th International Sy Jun Pang,Lijun Zhang Conference proceedings 2020 S

的是兄弟

Modelling and Implementation of Unmanned Aircraft Collision Avoidance,mportant and valuable. An ideal collision avoidance system gives the aircraft an optimal strategy for choosing flight actions to avoid collision risks when it detects other aircraft nearby. Currently the general approach to generating collision avoidance logics is to model the problem as a partially

outset

控诉

Computing Linear Arithmetic Representation of Reachability Relation of One-Counter Automata,shown to be NP-complete when the integers in the OCA are encoded in binary. In this paper, we study the problem of computing the reachability relation of OCA. We show that, for each OCA, an existential Presburger arithmetic (EPA) formula of polynomial size can be computed in polynomial time to repre

Cytokines

Compiling FL, on Finite Words,mulas (FL for short) is the core part of PSL, which has once been an industrial standard of specification language accepted by IEEE, and has now been adopted in SystemVerilog. We in this paper present a variant of FL, called FL., whose semantics is defined w.r.t. finite words. In comparison to the o

的’

Symbolic Model Checking with Sentential Decision Diagrams,BDD). The SDD data structure can be up to exponentially more succinct than BDDs, using a generalized notion of variable order called a variable tree (“vtree”). We also contribute to the practice of SDDs, giving a novel heuristic for constructing a vtree that minimizes SDD size in the context of mode

卧虎藏龙

Probably Approximately Correct Interpolants Generation,y correct (PAC) learning. The computed interpolant is termed as a PAC interpolant with respect to a violation level . and confidence level .: with at least . confidence, the probability that the PAC interpolant is a true interpolant is larger than .. Unlike classical interpolants which are used to j

恃强凌弱

Canvas

Learning Safe Neural Network Controllers with Barrier Certificates,rs are based on neural networks (NNs). To certify the safety property we utilize barrier functions, which are also represented by NNs. We train controller-NN and barrier-NN simultaneously, achieving verification-in-the-loop synthesis. We provide a prototype tool . with a number of case studies. Prel

一小块

Software Defect-Proneness Prediction with Package Cohesion and Coupling Metrics Based on Complex Neifficult for programmers to be thoughtful when modifying code, increasing the risk of defects. In an object-oriented software system, packages take the role of a middle tier that aggregates classes and limits class access. However, as the software system evolves, the logic and correctness of package

残忍