Functional code clone detection is important for software maintenance. In recent years, deep learning techniques are introduced to improve the performance of functional code clone detectors. By representing each code snippet as a vector containing its program semantics, syntactically dissimilar functional clones are detected. However, existing deep learning-based approaches attach too much importance to code feature learning, hoping to project all recognizable knowledge of a code snippet into a single vector. We argue that these deep learning-based approaches can be enhanced by considering the characteristics of syntactic code clone detection, where we need to compare the contents of the source code (e.g., intersection of tokens, similar flow graphs, and similar subtrees) to obtain code clones. In this paper, we propose a novel deep learning-based approach named DSFM, which incorporates comparisons between code snippets for detecting functional code clones. Specifically, we improve the typical deep clone detectors with deep subtree interactions that compare every two subtrees extracted abstract syntax trees (ASTs) of two code snippets, thereby introducing more fine-grained semantic similarity. By conducting extensive experiments on three widely-used datasets, GCJ, OJClone, and BigCloneBench, we demonstrate the great potential of deep subtree interactions in code clone detection task. The proposed DSFM outperforms the state-of-the-art approaches, including two traditional approaches, two unsupervised and four supervised deep learning-based baselines.

SQL injection attacks have posed a significant threat to web applications for decades. They obfuscate malicious codes into natural SQL statements so as to steal sensitive data, making them difficult to detect. Generally, malicious signals can be identified by using the contextual information of SQL statements. Such contextual information, however, is not always easily captured. Due to the fact that SQL as a formal language is highly structured, two tokens that are spatially far away may be semantically very close. An effective approach thus should take the structural feature of SQL statements into account when modeling their contextual information.

The application of deep learning techniques in software engineering becomes increasingly popular. One key problem is developing high-quality and easy-to-use source code representations for code-related tasks. The research community has acquired impressive results in recent years. However, due to the deployment difficulties and performance bottlenecks, seldom these approaches are applied to the industry. In this paper, we present xASTNN, an eXtreme Abstract Syntax Tree (AST)-based Neural Network for source code representation, aiming to push this technique to industrial practice. The proposed xASTNN has three advantages. First, xASTNN is completely based on widely-used ASTs and does not require complicated data pre-processing, making it applicable to various programming languages and practical scenarios. Second, three closely-related designs are proposed to guarantee the effectiveness of xASTNN, including statement subtree sequence for code naturalness, gated recursive unit for syntactical information, and gated recurrent unit for sequential information. Third, a dynamic batching algorithm is introduced to significantly reduce the time complexity of xASTNN. Two code comprehension downstream tasks, code classification and code clone detection, are adopted for evaluation. The results demonstrate that our xASTNN can improve the state-of-the-art while being faster than the baselines.

As the 5th generation (5G) network develops and rolls out rapidly, user requests can be offloaded to nearby edge servers for processing. This alleviates the pressure on the network backhaul and the remote cloud. Nevertheless, the edge user allocation (EUA) problem, as one of the main research challenges in the 5G era, has become a major obstacle to ensuring users’ Quality of Experience (QoE) in the edge computing environment. Conventional EUA approaches, ranging from static global allocation model to online decision-making model, have ignored the long-term impact of the changes in users’ expectations on user-perceived Quality of Service (QoS). Additionally, most existing approaches have not taken into account the distance between an edge user and an edge server, which impacts the user’s data rate profoundly. In this paper, we tackle these challenges by formulating EUA problem as a spatial-temporal one (ST-EUA), which models distance-aware QoS based on the wireless transmission attenuation and models users’ QoE based on the Expectation Confirmation Theory (ECT). To find an appropriate solution for ST-EUA problem, we develop two fuzzy control-based approaches, namely FC and BFC, for on demand scenarios and batch processing scenarios, respectively. They can balance effectively the user consolidation and server load. We conduct extensive experiments based on two widely-used real-world datasets. The results demonstrate the superiority of our FC and BFC in effectiveness and efficiency over the baselines and state-of-the-art.

Precise static analysis is necessary for an industrial environment to ensure reliability and security, which is usually field-sensitive and inter-procedural. However, it faces the problem of insufficient scale capability when being applied to various industrial environments: (1) Field-sensitive analysis can not assure termination if field accesses are modeled by unbounded access paths; (2) Inter-procedural analysis may lead to path explosion problems because of the unbounded length of call chains. While using longer access paths or call chains can improve precision, the analysis may have poor performance in terms of efficiency. Specifically, an industry-strength method should be scalable enough to face different applications. This paper presents a scalable fault detection method based on the precise access path. Precise access path models a memory location with accurate operations and offsets from a source. Points-to relations of variables are used to refine it. It can differentiate elements of aggregate structures and is more precise than the ordinary access path. Based on the precise access path, we perform an inter-procedural analysis with the help of an intra-procedural analysis and combined function summary. Furthermore, our method is designed backward to detect error handling bugs. Compared with the state-of-the-art tools, our method is more scalable, with higher precision and efficiency on both benchmarks and 11 widely-used applications.

SSL library plays an important role in ensuring secure connections against remote attacks, and thus the correct usages of SSL library should be guaranteed to avoid security and reliability flaws. However, improper error handling of API function failures frequently happens in SSL library usages, which could introduce security vulnerabilities. To detect such bugs in SSL usages, existing tools need correct error handling specifications. Manually write specifications is tedious and time-consuming. Therefore, a few works towards automatic inferring specifications are presented. However, the principles used in such works are insufficient for SSL library. Thus, in this paper, we first conduct an empirical study of error handling bugs in SSL applications to understand the true nature of such bugs, and the properties of these bugs are summarized, including the frequently used code structure for handling errors, the commonly occurred error-indicating features of the handling actions, and the general bug categories. Based on these properties, we design and implement a tool that can automatically infer error handling specifications and detect error handling bugs by exploiting the specifications in SSL applications. We evaluated our tool on 9 real-world open-source SSL applications. The tool infers 424 specifications in total, out of which 383 are confirmed correct, with a precision of 90%. Moreover, 27 real-world bugs have been detected, and all of them are confirmed by developers.

C language plays a key role in system programming and applications. Integer error is a common yet important C program defect because arithmetic operations may produce unrepresentable values in certain integer types. Integer error is one of the major sources of software failures and vulnerabilities. Due to the complex semantics of C integers, manually repairing integer errors is prone to introducing additional errors even for experienced programmers. This paper presents an approach to automatically generate fixes for integer errors. Our approach infers, for each expression, a type that is capable of representing its possible values, and utilizes inferred types as program fixes based on common fix patterns codified from real world. We have developed our system IntPTI which is evaluated on the largest public benchmark of integer errors and 7 widely-used open-source projects. The evaluation results demonstrate the superior performance of IntPTI in terms of accuracy, scalability, runtime overhead and robustness of fixes. In addition, IntPTI is applied on the embedded software of a realistic train control system. It succeeds in both detecting 67 new integer errors and generating 101 fixes confirmed by developers. The study substantiates the feasibility and effectiveness of the proposed methodology.

Using open-source libraries can provide rich functions and reduce development cost. However, some critical issues have also been caused such as license conflicts and vulnerability risks. In this paper, we design and implement an open-source libraries detection tool OSLDetector which uses methods of matching features to detect third-party libraries for multi-platform software in binaries. We took a series of methods such as filtering features and novelty building an internal clone forest to cope with the challenge of feature duplication. The tool can also provide the conflict of licenses and identify possible corresponding vulnerabilities, so these potential risks can be resolved and avoided. To evaluate the efficiency of OSLDetector, we collect 5K libraries containing 9K versions and manage their respective license type and existing vulnerabilities. The experimental results with a precision of 96% and recall of 92.3% show that OSLDetector is effective and outperforms similar tools.

Precise pointer analysis is desired since many program analyses benefit from it both in precision and performance. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. The more dimensions a pointer analysis considers, the more accurate its results will be. However, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced. This paper presents a flow, context, field and quasi path sensitive pointer analysis algorithm for C programs. Our algorithm runs on a control flow automaton, a key structure for our analysis to be flow sensitive. During the analysis process, we use function summaries to get context information. Elements of aggregate structures are handled to improve precision. We collect path conditions to filter unreachable paths and make all points-to relations gated. For efficiency, we propose a multi-entry mechanism. The algorithm is implemented in TsmartGP, which is an extension of CPAchecker. Our algorithm is compared with some state-of-the-art algorithms and TsmartGP is compared with cppcheck and Clang Static Analyzer by detecting uninitialized pointer errors in 13 real-world applications. The experimental results show that our algorithm is more accurate and TsmartGP can find more errors than other tools.

Today, large and complex software is developed with integrated components using application programming interfaces (APIs). Correct usage of APIs in practice presents a challenge due to implicit constraints, such as call conditions or call orders. API misuse, i.e., violation of these constraints, is a well-known source of bugs, some of which can cause serious security vulnerabilities. Although researchers have developed many API-misuse detectors over the last two decades, recent studies show that API misuses are still prevalent. In this paper, we provide a comprehensive empirical study on API-misuse bugs in open-source C programs. To understand the nature of API misuses in practice, we analyze 830 API-misuse bugs from six popular programs across different domains. For all the studied bugs, we summarize their root causes, fix patterns and usage statistics. Furthermore, to understand the capabilities and limitations of state-of-the-art static analysis detectors for API-misuse detection, we develop APIMU4C, a dataset of API-misuse bugs in C code based on our empirical study results, and evaluate three widely-used detectors on it qualitatively and quantitatively. We share all the findings and present possible directions towards more powerful API-misuse detectors.

Value flow are widely used in static analysis to detect bugs. Existing techniques usually employ a pointer analysis and generate source sink summaries defined by problem domain, then a solver is invoked to determine whether the path is feasible. However, most of the tools does not provide an easy way for users to find user defined bugs within the same architecture of finding pre-defined bugs. This paper presents VFQL, an expressive query language on value flow graph and the framework to execute the query to find user defined defects. Moreover, VFQL provides a nice GUI to demonstrate the value flow graph and a modeling language to define system libraries or user libraries without code, which further enhances its usability. The experimental results on open benchmarks show that VFQL achieve a competitive performance against other state of art tools. The result of case study conducted on open source program shows that the flexible query and modeling language provide a great support in finding user specified defects.

Static analysis has long prevailed as a promising approach to detect program bugs at an early development process to increase software quality. However, such tools face great challenges to balance the false-positive rate and the false-negative rate in practical use. In this paper, we present VBSAC, a value-based static analyzer for C aiming to improve the precision and recall. In our tool, we employ a pluggable value-based analysis strategy. A memory skeleton recorder is designed to maintain the memory objects as a baseline. While traversing the control flow graph, diverse value-based plug-ins analyze the specific abstract domains and share program information to strengthen the computation. Simultaneously, checkers consume the corresponding analysis results to detect bugs. We also provide a user-friendly web interface to help users audit the bug detection results. Evaluation on two widely-used benchmarks shows that we perform better to state-of-the-art bug detection tools by finding 221-339 more bugs and improving F-Score 9.88%-40.32%.

Misuse of APIs happens frequently due to misunderstanding of API semantics and lack of documentation. An important category of API-related defects is the error handling defects, which may result in security and reliability flaws. These defects can be detected with the help of static program analysis, provided that error specifications are known. The error specification of an API function indicates how the function can fail. Writing error specifications manually is time-consuming and tedious. Therefore, automatic inferring the error specification from API usage code is preferred. In this paper, we present Ares, a tool for automatic inferring error specifications for C code through static analysis. We employ multiple heuristics to identify error handling blocks and infer error specifications by analyzing the corresponding condition logic. Ares is evaluated on 19 real world projects, and the results reveal that Ares outperforms the state-of-the-art tool APEx by 37% in precision. Ares can also identify more error specifications than APEx. Moreover, the specifications inferred from Ares help find dozens of API-related bugs in well-known projects such as OpenSSL, among them 10 bugs are confirmed by developers. Video: https://youtu.be/nf1QnFAmu8Q. Repository: https://github.com/lc3412/Ares.

Precise pointer analysis is desired since it is a core technique to find memory defects. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. For static analysis tools utilizing pointer analysis, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced. This paper presents TsmartGP, a static analysis tool for finding memory defects in C programs with a precise and efficient pointer analysis. The pointer analysis algorithm is flow, context, field, and quasi path sensitive. Control flow automatons are the key structures for our analysis to be flow sensitive. Function summaries are applied to get context information and elements of aggregate structures are handled to improve precision. Path conditions are used to filter unreachable paths. For efficiency, a multi-entry mechanism is proposed. Utilizing the pointer analysis algorithm, we implement a checker in TsmartGP to find uninitialized pointer errors in 13 real-world applications. Cppcheck and Clang Static Analyzer are chosen for comparison. The experimental results show that TsmartGP can find more errors while its accuracy is also higher than Cppcheck and Clang Static Analyzer. The demo video is available at https://youtu.be/IQlshemk6OA.

Secure Sockets Layer (SSL) and Transport Layer Security (TLS) protocols provide a reliable communication channel between applications over the Internet.Implementations of these protocols (e.g., OpenSSL and GnuTLS) publish wellformat documentation and examples online to guide the usage of SSL/TLS APIs.However, incorrect usages have caused many severe vulnerabilities (e.g., privilege escalation, denial of service, man-in-the-middle attack, etc.) in recent years.In this paper, we introduce SSLDoc to diagnose incorrect SSL API usages in real-world C programs automatically.The key insight behind SSLDoc is a constraint-directed static analysis technique powered by domain-specific usage patterns that we learn from real-world vulnerabilities and bug-fix-related patches.We have instantiated SSLDoc for OpenSSL APIs and applied it to large-scale opensource programs.SSLDoc found 45 previously unknown securitysensitive bugs in OpenSSL implementation and applications in Ubuntu.We created and submitted issues for all of them.Up to now, 35 have been confirmed by the corresponding development communities and 27 have been fixed in master branch.

Application Programming Interfaces (APIs) usually have usage constraints, such as call conditions or call orders. Incorrect usage of these constraints, called API misuse, will result in system crashes, bugs, and even security problems. It is crucial to detect such misuses early in the development process. Though many approaches have been proposed over the last years, recent studies show that API misuses are still prevalent, especially the ones specific to individual projects. In this paper, we strive to improve current API-misuse detection capability for large-scale C programs. First, We propose IMSpec, a lightweight domain-specific language enabling developers to specify API usage constraints in three different aspects (i.e., parameter validation, error handling, and causal calling), which are the majority of API-misuse bugs. Then, we have tailored a constraint guided static analysis engine to automatically parse IMSpec rules and detect API-misuse bugs with rich semantics. We evaluate our approach on widely used benchmarks and real-world projects. The results show that our easily extensible approach performs better than state-of-the-art tools. We also discover 19 previously unknown bugs in real-world open-source projects, all of which have been confirmed by the corresponding developers.

Libraries offer reusable functionality through Application Programming Interfaces (APIs) with usage constraints such as call conditions or orders. Constraint violations, i.e. API misuses, commonly lead to bugs and security issues. Although researchers have developed various API misuse detectors in the past few decades, recent studies show that API misuse is prevalent in real-world projects, especially for secure socket layer (SSL) certificate validation, which is completely broken in many security-critical applications and libraries. In this paper, we introduce SSLDoc to effectively detect API misuse bugs, specifically for SSL API libraries. The key insight behind SSLDoc is a constraint-directed static analysis technique powered by a domain-specific language (DSL) for specifying API usage constraints. Through studying real-world API misuse bugs, we propose ISpec DSL, which covers majority types of API usage constraints and enables simple but precise specification. Furthermore, we design and implement SSLDoc to automatically parse ISpec into checking targets and employ a static analysis engine to identify potential API misuses and prune false positives with rich semantics. We have instantiated SSLDoc for OpenSSL APIs and applied it to large-scale open-source programs. SSLDoc found 45 previously unknown security-sensitive bugs in OpenSSL implementation and applications in Ubuntu. Up to now, 35 have been confirmed by the corresponding development communities and 27 have been fixed in master branch.

In C programs, integer error is a common yet important kind of defect due to arithmetic operations that produce unrepresentable values in certain types. Integer errors are harbored in a wide range of applications and possibly lead to serious software failures and exploitable vulnerabilities. Due to the complicated semantics of C, manually preventing integer errors is challenging even for experienced developers. In this paper we propose a novel approach to automate C integer error repair by elevating the precision of arithmetic operations according to a set of code transformation rules. A large portion of integer errors can be repaired by recovering expected results (i.e., tolerance) instead of removing program functionality. Our approach is fully automatic without requiring code specifications. Furthermore, the transformed code is ensured to be well-typed and has conservativeness property with respect to the original code. Our approach is implemented as a prototype CIntFix which succeeds in repairing all the integer errors from 7 categories in NIST's Juliet Test Suite. Furthermore, CIntFix is evaluated on large code bases in SPEC CINT2000, scaling to 366 KLOC within 126 seconds while the transformed code has 10.5 percent slowdown on average. The evaluation results substantiate the potential of our approach in real-world scenarios.

Static analysis is an effective way of checking memory safety issues in program. Usually, multiple analysis algorithms usually run together to achieve a precise analysis result. In this paper, a novel analysis frame work over access path is presented for incorporating analysis algorithms. A pointer analysis based on access path works as a base layer, alias and pointer information are automatically handled. An summary based checking algorithm is designed for checking real world project. Moreover, the framework is fully extensible and various analysis can be added as plugins. Experimental results show that our method has good precision on Juliet Test Suite and scales to large software.

Combinatorial testing can test software that has various configurations for multiple parameters efficiently. This method is based on a set of test cases that guarantee a certain level of interaction among parameters. Mixed covering array (MCA) can be used to represent a test-suite. Each row of the array corresponds to a test case. In general, a smaller size of MCA does not necessarily imply less testing time. There are certain combinations of parameter values which would take much longer time than other cases. Based on this observation, it is more valuable to construct MCAs that are better in terms of testing effort characterization other than size. We present a method to find cost-aware MCAs. The method contains two steps. First, simulated annealing algorithm is used to get an MCA with a small size. Then we propose a novel nested differential evolution algorithm to improve the solution with its testing effort. The experimental results indicate that our method succeeds in constructing cost-aware MCAs for real-world applications. The testing effort is significantly reduced compared with representative state-of-the-art algorithms.

When analyzing programs using static program analysis, we need to determine the reachability of each possible execution path of the programs. Many static analysis tools collect constraints of each path and use SMT solvers to determine the satisfiability of these constraints. The accumulated computing time can be long if we use SMT solvers too many times. In this paper, we propose a constraint-pattern based method for reachability determination to address the limitation of current approaches. We define some constraint-patterns. For each pattern, a carefully designed constraints solving algorithm is presented. Our method contains two steps. Firstly, we collect some information about the constraints in the program to be analyzed. Then we choose the most suitable algorithm for reachability determination based on the information. Secondly, we apply the algorithm in analysis process to speed up satisfiability checking of path constraints. We implement our method based on CPAchecker, a famous software verification tool. The experimental results on some well-known benchmarks show that, with a moderate accuracy, our method is more efficient in comparison with some state-of-the-art SMT solvers.

Integer errors in C/C++ are caused by arithmetic operations yielding results which are unrepresentable in certain type. They can lead to serious safety and security issues. Due to the complicated semantics of C/C++ integers, integer errors are widely harbored in real-world programs and it is error-prone to repair them even for experts. An automatic tool is desired to 1) automatically generate fixes which assist developers to correct the buggy code, and 2) provide sufficient hints to help developers review the generated fixes and better understand integer types in C/C++. In this paper, we present a tool IntPTI that implements the desired functionalities for C programs. IntPTI infers appropriate types for variables and expressions to eliminate representation issues, and then utilizes the derived types with fix patterns codified from the successful human-written patches. IntPTI provides a user-friendly web interface which allows users to review and manage the fixes. We evaluate IntPTI on 7 real-world projects and the results show its competitive repair accuracy and its scalability on large code bases. The demo video for IntPTI is available at: https://youtu.be/9Tgd4A_FgZM.

To reduce the false positives of static analysis, many tools collect path constraints and integrate SMT solvers to filter unreachable execution paths. However, the accumulated calling and computing of SMT solvers are time and resource consuming. This paper presents TsmartLW, an alternate static analysis tool in which we implement a path constraint solving engine to speed up reachability determination. Within the engine, typical types of constraint-patterns are firstly defined based on an empirical study of a large number of code repositories. For each pattern, a constraint solving algorithm is designed and implemented. For each program, the engine predicts the most suitable strategy and then applies the strategy to solve path constraints. The experimental results on some well-known benchmarks and real-world applications show that TsmartLW is faster than some state-of-the-art static analysis tools. For example, it is 1.32× faster than CPAchecker and our engine is 369× faster than SMT solvers in solving path constraints. The demo video is available at https://www.youtube.com/watch?v=5c3ARhFclHA&t=2s.

Integer errors in C program may lead to serious failures and vulnerabilities. They are harbored in a wide range of programs including mature software such as Linux kernel. Code reviewing is laborious and cannot guarantee reliable fixes for errors. Addressing potential errors in the development phase is error-prone even for experts and essentially hinders developing efficiency. In this paper we propose a novel approach to automate fix for C integer errors. Our approach directly replaces original C integers with dynamic-precision integers to fix potential errors without detecting them in advance. Many errors can be fixed by precision improvement without changing the design of application. We implement a tool CIntFix to automatically fix C integer errors. CIntFix succeeds in fixing all 5414 programs in NIST's Juliet test suite from 7 weakness categories. Meanwhile, on Juliet test suite and SPEC CINT2000 benchmarks, CIntFix processes C source code at the rate of 0.157s/KLOC and the fixed programs have 18.0% slowdown on average. The results show that CIntFix is capable to fix integer errors in real-world C programs.

Boundary value analysis is a typical conventional testing technique. However, manually identifying input regions and writing test cases are labor-intensive and time-consuming. In this paper, we propose a search-based random testing approach, which automatically generates test data along the boundaries of semantic regions of the input domain. The experiments on mutated programs confirm the effectiveness and efficiency of the proposed approach. Furthermore, our approach significantly outperforms the conventional ART (Adaptive Random Testing) methods, which sample test cases evenly across the input regions. Our approach also outperforms EvoSuite, a state-of-the-art tool that generates test cases satisfying certain coverage criterion.

Opposing to the oracle assumption, a trustworthy test oracle is not always available in real practice. Since manually written oracles and human judgements are still widely used, testers and programmers are in fact facing a high risk of erroneous test oracles. However, test oracle errors can bring much confusion thus causing extra time consumption in the debugging process. As substantiated by our experiment on the Siemens Test Suite, automatic fault localization algorithms suffer severely from erroneous test oracles, which impede them from reducing debugging time to the full extent. This paper proposes a simple but effective approach to debug the test oracle. Based on the observation that test cases covering similar lines of code usually generate similar results, we are able to identify suspicious test cases that are differently judged by the test oracle from their neighbors. To validate the effectiveness of our approach, experiments are conducted on both the Siemens Test Suite and grep. The results show that averagely over 75 percent of the highlighted test cases are actually test oracle errors. Moreover, performance of fault localization algorithms recovered remarkably with the debugged oracles.

In many reactive systems, programs run cyclically. In each cycle, they check the current status and handle the business for a single step. The business logic has to be blasted to pieces, which violates the way that people are used to. Cyclic programs are difficult to develop and their reliability is hard to guarantee. To tackle these problems, we propose a model-based formal design flow which is more rigorous and rapid than the V-model. Our method consists of three phases: modeling, verification and code synthesis. In the modeling phase, BIP (Behavior-Interaction-Priority) language, which is expressive and allows flexible modeling, is used as the modeling language. Real-time behavior, that is highly concerned in reactive systems, can be modeled as well. In the verification phase, the system model is translated to timed automata and checked by Uppaal. Verification helps to ensure the correctness of the model. In the code synthesis phase, the software part of the system model is synthesized to cyclic code. We propose an algorithm which can generate high-performance cyclic code from a model which describes the business work-flow. This feature significantly simplifies program development. A set of tools is implemented to support our design flow and they are successfully applied to an industrial case study for a PLC (Programmable Logic Controller) system which is used to control several physical devices in a huge palace.

Large-scale systems are often modeled and verified in a component-based way. BIP (Behavior, Interaction, Priority) is a flexible component-based framework which supports hierarchical design of heterogeneous systems. BIP components interact via connectors in which data can be passed among multiple components. It also support the modeling of time. Due to its expressiveness and flexibility, many real-time systems can be modeled easily in BIP. Verification, however, is not well supported in the current BIP framework. That is a major disadvantage when it is used in a model-driven design flow. To fill this gap, we propose a translation from slightly restricted BIP models to timed automata. Then model checking can be applied to the latter using Uppaal (which is a sophisticated model checker for timed automata). The correctness of translation is proven formally and the translation is implemented as a tool Bip2Uppaal. Three industrial case studies show that our approach is practical and effective.

Temporal induction is a SAT-based model checking technique. We prove that the SAT instances generated by its induction rule can be reduced to the so called Incremental CNFs. A new DPLL procedure is customized for Incremental CNFs, so that the intermediate results in solving previous instances, including the learnt clauses and the search tree, can be reused in solving the next instance. To the best of our knowledge, this is the first result on reusing the search tree in SAT solving of temporal induction. Experimental results on a large number of benchmarks show significant performance gain of our approach.

Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper shows the modeling and validation work of a typical PLC control system using the Behavior-Interaction-Priority(BIP) component framework. The gate control system based on PLC is a real industry application. We design general system architecture for this kind of device control system. The control software and hardware of environment are all modeled as BIP components. Their interactions are described by BIP connectors. System requirements are formalized as monitors. Simulation is applied on the system model. We found a couple of design errors in simulation, which help us to improve the dependability of the original systems.

Propositional satisfiability problem (SAT) is a fundamental problem both in theory and practice. In the area of software engineering, people employ various techniques, such as model checking, theorem proving, automated testing and so on, to ensure the quality of software. Those techniques are usually based on SAT solvers. The efficiency is an important criterion for a good SAT solver. Besides, the ability of producing proofs is also considered to be quite useful because it provides a mechanism that the correctness of checking result is guaranteed. Moreover, proofs can be used when calculating interpolation. In this paper, we investigate a new resolution based algorithm for solving SAT problem. The algorithm combines resolution and search. It resolves certain clauses when necessary and at the same time tries to find a valuation under which the formula evaluates to true. Information found in the process of searching for such a valuation is used to guide the resolution. The algorithm stops whenever a satisfying valuation is found or empty clause is generated. So, it terminates quickly for both satisfiable and unsatisfiable clauses. Compared with other resolution based algorithms, the experiment result shows that the number of resolutions and number of generated clauses are much less than directional resolution. Another major advantage of our algorithm is, once terminates, a proof can be easily generated with very low time complexity.