7 citations · 20 across the 7 of their papers we have counts for
7 papers
Probabilistic modelling and safety assurance of an agriculture robot providing light-treatment
Mustafa Adam, Kangfeng Ye, David A. Anisi +3
Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology. This motivates our work on safety assurance…
RoboCertProb: Property Specification for Probabilistic RoboChart Models
Kangfeng Ye, Jim Woodcock
RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and…
Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
Kangfeng Ye, Fang Yan, Simos Gerasimou
Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties for probabilistic models. However, captu…
Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
Kangfeng Ye, Jim Woodcock, Simon Foster
Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic p…
Formally Verified Animation for RoboChart using Interaction Trees
Kangfeng Ye, Simon Foster, Jim Woodcock
RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared var…
Automated Verification of Reactive and Concurrent Programs by Calculation
Simon Foster, Kangfeng Ye, Ana Cavalcanti +1
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applicati…
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Simon Foster, Kangfeng Ye, Ana Cavalcanti +1
Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite…