As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the ...As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.展开更多
Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to...Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.展开更多
Data race is one of the most important concurrent anomalies in multi-threaded programs.Emerging con-straint-based techniques are leveraged into race detection,which is able to find all the races that can be found by a...Data race is one of the most important concurrent anomalies in multi-threaded programs.Emerging con-straint-based techniques are leveraged into race detection,which is able to find all the races that can be found by any oth-er sound race detector.However,this constraint-based approach has serious limitations on helping programmers analyze and understand data races.First,it may report a large number of false positives due to the unrecognized dataflow propa-gation of the program.Second,it recommends a wide range of thread context switches to schedule the reported race(in-cluding the false one)whenever this race is exposed during the constraint-solving process.This ad hoc recommendation imposes too many context switches,which complicates the data race analysis.To address these two limitations in the state-of-the-art constraint-based race detection,this paper proposes DFTracker,an improved constraint-based race detec-tor to recommend each data race with minimal thread context switches.Specifically,we reduce the false positives by ana-lyzing and tracking the dataflow in the program.By this means,DFTracker thus reduces the unnecessary analysis of false race schedules.We further propose a novel algorithm to recommend an effective race schedule with minimal thread con-text switches for each data race.Our experimental results on the real applications demonstrate that 1)without removing any true data race,DFTracker effectively prunes false positives by 68%in comparison with the state-of-the-art constraint-based race detector;2)DFTracker recommends as low as 2.6-8.3(4.7 on average)thread context switches per data race in the real world,which is 81.6%fewer context switches per data race than the state-of-the-art constraint based race detec-tor.Therefore,DFTracker can be used as an effective tool to understand the data race for programmers.展开更多
Satisfiability Modulo Theories （SMT） have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our know...Satisfiability Modulo Theories （SMT） have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, SYMBA and OPT-MATHSAT are two most efficient solvers available for this problem. The key algorithms used by SVMBA and OPT-MATHSAT consist of the loop of two procedures： 1） critical finding for detecting a critical point, which is very likely to be globally optimal, and 2） global checking for confirming the critical point is reMly globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the Mgorithms of critical finding in SYMBA and OPT-MATHSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against SYMBA and OPT-MATHSAT on a critical class of problems in real-time systems. Our approach outperforms SYMBA on 99.6% of benchmarks and is superior to OPT-MATHSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem.展开更多
基金Supported by the National Natural Science Foundation of China(Nos.61063002,61100186,61262008)Guangxi Natural Science Foundation of China(2011GXNSFA018164,2011GXNSFA018166,2012GXNSFAA053220)the Key Project of Education Department of Guangxi
文摘As a complementary technology to Binary Decision Diagram-based(BDD-based) symbolic model checking, the verification techniques on Boolean satisfiability problem have gained an increasing wide of applications over the last few decades, which brings a dramatic improvement for automatic verification. In this paper, we firstly introduce the theory about the Boolean satisfiability verification, including the description on the problem of Boolean satisfiability verification, Davis-Putnam-Logemann-Loveland(DPLL) based complete verification algorithm, and all kinds of solvers generated and the logic languages used by those solvers. Moreover, we formulate a large number optimizations of technique revolutions based on Boolean SATisfiability(SAT) and Satisfiability Modulo Theories(SMT) solving in detail, including incomplete methods such as bounded model checking, and other methods for concurrent programs model checking. Finally, we point out the major challenge pervasively in industrial practice and prospect directions for future research in the field of formal verification.
基金Project supported by the National Natural Science Foundation of China (Nos 60635020 and 90718039)the National Basic Research Program (973) of China (No 2004CB719406)
文摘Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.
基金This work is supported by the National Key Research and Development Program of China under Grant No.2023YFB4503400the National Natural Science Foundation of China under Grant Nos.62322205,62072195,and 61825202.
文摘Data race is one of the most important concurrent anomalies in multi-threaded programs.Emerging con-straint-based techniques are leveraged into race detection,which is able to find all the races that can be found by any oth-er sound race detector.However,this constraint-based approach has serious limitations on helping programmers analyze and understand data races.First,it may report a large number of false positives due to the unrecognized dataflow propa-gation of the program.Second,it recommends a wide range of thread context switches to schedule the reported race(in-cluding the false one)whenever this race is exposed during the constraint-solving process.This ad hoc recommendation imposes too many context switches,which complicates the data race analysis.To address these two limitations in the state-of-the-art constraint-based race detection,this paper proposes DFTracker,an improved constraint-based race detec-tor to recommend each data race with minimal thread context switches.Specifically,we reduce the false positives by ana-lyzing and tracking the dataflow in the program.By this means,DFTracker thus reduces the unnecessary analysis of false race schedules.We further propose a novel algorithm to recommend an effective race schedule with minimal thread con-text switches for each data race.Our experimental results on the real applications demonstrate that 1)without removing any true data race,DFTracker effectively prunes false positives by 68%in comparison with the state-of-the-art constraint-based race detector;2)DFTracker recommends as low as 2.6-8.3(4.7 on average)thread context switches per data race in the real world,which is 81.6%fewer context switches per data race than the state-of-the-art constraint based race detec-tor.Therefore,DFTracker can be used as an effective tool to understand the data race for programmers.
基金This work is supported by the National Natural Science Foundation of China under Grant No. 61170072, and the Chinese Academy of Sciences/State Administration of Foreign Experts Affairs （CAS/SAFEA） International Partnership Program for Creative Research Teams.
文摘Satisfiability Modulo Theories （SMT） have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, SYMBA and OPT-MATHSAT are two most efficient solvers available for this problem. The key algorithms used by SVMBA and OPT-MATHSAT consist of the loop of two procedures： 1） critical finding for detecting a critical point, which is very likely to be globally optimal, and 2） global checking for confirming the critical point is reMly globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the Mgorithms of critical finding in SYMBA and OPT-MATHSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against SYMBA and OPT-MATHSAT on a critical class of problems in real-time systems. Our approach outperforms SYMBA on 99.6% of benchmarks and is superior to OPT-MATHSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem.
