Automated Software Verification Supporting ABS TCS Safety Design

1994 ◽  
Author(s):  
Torsten Sauer
Keyword(s):  
Software Verification ◽  
Safety Design ◽  
Automated Software ◽  
Automated Software Verification

Synthesizing Conjunctive & Disjunctive Linear Invariants by K-means++ and SVM

2020 ◽  
Vol 17 (6) ◽  
pp. 847-856
Author(s):  
Shengbing Ren ◽  
Xiang Zhang
Keyword(s):  
Software Verification ◽  
State Of The Art ◽  
Positive Sample ◽  
Machine Learning Algorithms ◽  
Support Vector ◽  
Hoare Logic ◽  
Excellent Performance ◽  
Automated Software ◽  
Inductive Invariants ◽  
Linear Invariants

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

scholarly journals TCAS software verification using constraint programming

2012 ◽  
Vol 27 (3) ◽  
pp. 343-360 ◽  
Author(s):  
Arnaud Gotlieb
Keyword(s):  
Constraint Programming ◽  
Software Verification ◽  
Constraint Propagation ◽  
Critical Properties ◽  
Safety Properties ◽  
Safety Critical ◽  
Constraint Systems ◽  
Collision Avoidance System ◽  
Commercial Applications ◽  
Automated Software

AbstractSafety-critical software must be thoroughly verified before being exploited in commercial applications. In particular, any TCAS (Traffic Alert and Collision Avoidance System) implementation must be verified against safety properties extracted from the anti-collision theory that regulates the controlled airspace. This verification step is currently realized with manual code reviews and testing. In our work, we explore the capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint solving procedure that combines constraint propagation with Linear Programming to solve conditional disjunctive constraint systems over bounded integers extracted from computer programs and safety properties. An experience we made on verifying a publicly available TCAS component implementation against a set of safety-critical properties showed that this approach is viable and efficient.

Sign in / Sign up

Export Citation Format

Share Document