Abstract Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. Although prior efforts have aimed to address this limitation, we show that state-of-the-art methods remain inaccurate. In this paper, we propose a novel modeling approach that captures mutex semantics using ordering constraints, enabling accurate deadlock verification within partial-order-based concurrent verification frameworks. We formally prove the correctness of our method and implement it in a prototype tool, Deagle-DL . We evaluate Deagle-DL against a state-of-the-art bounded model checker ESBMC that employs the conventional modeling approach, and a state-of-the-art static analysis tool for deadlock detection. Our experiments show that Deagle-DL significantly outperforms both tools in terms of precision, while maintaining substantial efficiency.

Abstract SMT solving with ordering consistency theory achieves state-of-the-art efficiency in bounded model checking of concurrent programs. At its core is a dedicated theory solver that derives the write-serialization (WS) and from-read (FR) orders on the fly, thereby allowing their explicit encodings to be omitted. Additionally, the solver is equipped with preventive propagation , which proactively eliminates theory-level conflicts. This work presents a refined ordering consistency theory that overcomes two existing limitations. First, we address the weak SC problem , where the solver may fail to reconstruct a total WS order and thus admit executions weaker than Sequential Consistency. We identify the core reason as insufficient constraints on WS totality. As a solution, we restore the WS encodings to ensure its totality, while preserving WS derivation to curb the resulting growth in the search space. Second, the existing framework for preventive propagation does not support WS variables or atomicity constraints. We extend it to incorporate these elements, yielding a more general and principled propagation mechanism. Experiments show that our approach soundly prevents weak-SC behaviors, enables effective propagation, and maintains competitive overall performance.

Merge conflicts often arise when developers integrate changes from different software branches. The conflicts can result from overlapping edits in programs (i.e., textual conflicts), or cause build and test errors (i.e., build and test conflicts). They degrade software quality and hinder programmer productivity. While several tools detect build conflicts, few offer meaningful support for resolving them. To overcome limitations of existing tools, we introduce BuCoR (BUild COnflict Resolver), a new conflict resolver. BuCoR first detects conflicts by comparing three versions related to a merging scenario: base b, left l, and right r. To resolve conflicts, it employs two complementary strategies: example-based transformation (BuCoR-E) and rule-based transformation (BuCoR-R). BuCoR-R applies predefined rules to resolve conflicts in frequently suggested or conventional ways. BuCoR-E mines branch versions (l and r) for exemplar edits applied to fix related build errors. From these examples, it infers and generalizes program transformation patterns to resolve conflicts in project-specific or unconventional ways.

Invariant synthesis is a fundamental problem in program verification, yet existing learning-based approaches rarely exploit the inherent symmetry present in many programs, particularly parameterized and concurrent systems. Such symmetry induces a symmetric reachable state space, naturally yielding symmetric samples and admitting symmetric invariants, motivating the task of learning symmetric invariants from symmetric samples. To this end, we introduce symmetric decision trees (SDTs), a novel hypothesis class that enforces symmetry structurally, guaranteeing symmetric invariants by construction. Furthermore, we develop a learning algorithm to construct SDTs and integrate it as the learner within the Horn-ICE framework, yielding our approach, Horn-SDT. Empirical evaluation on parameterized programs demonstrates that Horn-SDT achieves faster convergence and constructs more compact trees compared to non-symmetric baselines.

The emerging non-volatile memory (NVM) technologies provide competitive performance with DRAM and ensure data persistence in the event of system failure. However, it exhibits weak behaviour in terms of the order in which stores are committed to NVMs, and therefore requires extra efforts from developers to flush pending writes. To ensure correctness of this error-prone task, it is crucial to develop a rigid method to check crash consistency of programs running on NVM devices. Most existing solutions are testing-based and rely on user guidance to dynamically detect such deficiencies. In this paper, we present a fully automated method to verify robustness, a newly established property for ensuring crash consistency of such programs. The method is based on the observation that, reachability of a post-crash non-volatile state under a given pre-crash execution can be reduced to validity of the pre-crash execution with additional ordering constraints. Our robustness verification algorithm employs a search-based framework to explore all partial executions and states, and checks if any non-volatile state is reachable under certain pre-crash execution. Once a reachable non-volatile state is obtained, we further check its reachability under memory consistency model. The algorithm is implemented in a prototype tool PMVerify that leverages symbolic encoding of the program and utilizes an SMT solver to efficiently explore all executions and states. The method is integrated into the DPLL(T) framework to optimize the robustness checking algorithm. Experiments on the PMDK example benchmark show that PMVerify is competitive with the state-of-the-art dynamic tool, PSan, in terms of robustness violation detection.

In this paper, we present structural abstraction refinement, a novel framework for verifying the threshold problem of probabilistic programs. Our approach represents the structure of a Probabilistic Control-Flow Automaton (PCFA) as a Markov Decision Process (MDP) by abstracting away statement semantics. The maximum reachability of the MDP naturally provides a proper upper bound of the violation probability, termed the structural upper bound . This introduces a fresh “structural” characterization of the relationship between PCFA and MDP, contrasting with the traditional “semantical” view, where the MDP reflects semantics. The method uniquely features a clean separation of concerns between probability and computational semantics that the abstraction focuses solely on probabilistic computation and the refinement handles only the semantics aspect, where the latter allows non-random program verification techniques to be employed without modification. Building upon this feature, we propose a general counterexample-guided abstraction refinement (CEGAR) framework, capable of leveraging established non-probabilistic techniques for probabilistic verification. We explore its instantiations using trace abstraction. Our method was evaluated on a diverse set of examples against state-of-the-art tools, and the experimental results highlight its versatility and ability to handle more flexible structures swiftly.

P4 is widely adopted for programming data planes in software-defined networking. Formal verification of P4 programs is essential to ensure network reliability and security. However, existing P4 verifiers overlook the stateful nature of packet processing, rendering them inadequate for verifying complex stateful P4 programs.In this paper, we introduce a novel concept called packet invariants to address the stateful aspects of P4 programs. We present an automated verification tool specifically designed for stateful P4 programs. This algorithm efficiently discovers and validates packet invariants in a data-driven manner, offering a novel and effective verification approach for stateful P4 programs. To the best of our knowledge, this approach represents the first attempt to generate and leverage domain-specific invariants for P4 program verification. We implement our approach in a prototype tool called P4Inv. Experimental results demonstrate its effectiveness in verifying stateful P4 programs.

IC3 is a famous bit-level framework for safety verification. By incorporating datapath abstraction, a notable enhancement in the efficiency of hardware verification can be achieved. However, datapath abstraction entails a coarse level of abstraction where all datapath operations are approximated as uninterpreted functions. This level of abstraction, albeit useful, can lead to an increased computational burden during the verification process as it necessitates extensive exploration of redundant abstract state space. In this paper, we introduce a novel approach called datapath propagation. Our method involves leveraging concrete constant values to iteratively compute the outcomes of relevant datapath operations and their associated uninterpreted functions. Meanwhile, we generate potentially useful datapath propagation lemmas in abstract state space and tighten the datapath abstraction. With this technique, the abstract state space can be reduced, and the verification efficiency is significantly improved. We implemented the proposed approach and conducted extensive experiments. The results show promising improvements of our approach compared to the state-of-the-art verifiers.

Termination is a fundamental liveness property for program verification. In this paper, we revisit the problem of non-termination analysis and propose the first data-driven learning algorithm for synthesizing recurrent sets, where the non-terminating samples are effectively speculated by a novel method. To ensure convergence of learning, we develop a learning algorithm which is guaranteed to converge to a valid recurrent set if one exists, and thus establish its relative completeness. The methods are implemented in a prototype tool, and experimental results on public benchmarks show its efficacy in proving non-termination as it outperforms state-of-the-art tools, both in terms of cases solved and performance. Evaluation on non-linear programs also demonstrates its ability to handle complex programs.

P4 is a mainstream language for Software Defined Network (SDN) data planes. P4 is designed to achieve target-independent, protocol-independent, and configurable SDN data planes. However, logic errors may occur in P4 programs, resulting in improper packet processing, which may cause serious network errors and information disclosure. In addition, P4 programs contain many branches and thus are more challenging to ensure correctness. Formal verification is a powerful technique to verify the correctness of P4 programs. Unfortunately, current P4 verification studies lack basic toolchains, and their intermediate languages are not expressive enough. We present P4b, an efficient translator from P4 programs to Boogie, a verification-oriented intermediate representation. We provide formal translation rules to ensure the correctness of the translation process. The translated results can be verified by the toolchain of Boogie. We conducted experiments on 170 P4 programs collected from GitHub, and the experimental results demonstrate that our translator is useful and practical. The screencast is available at https://youtu.be/8_rEj3QFQeM. The tool is available at https://github.com/Invincibleyc/P4B-Translator.

Layout-sensitive grammars have been adopted in many modern programming languages. In a serious language design phase, the specified syntax—typically a grammar—must be unambiguous. Although checking ambiguity is undecidable for context-free grammars and (trivially also) layout-sensitive grammars, ambiguity detection , on the other hand, is possible and can benefit language designers from exposing potential design flaws . In this paper, we tackle the ambiguity detection problem in layout-sensitive grammars. Inspired by a previous work on checking the bounded ambiguity of context-free grammars via SAT solving , we intensively extend their approach to support layout-sensitive grammars but via SMT solving to express the ordering and quantitative relations over line/column numbers. Our key novelty lies in a reachability condition, which takes the impact of layout constraints on ambiguity into careful account. With this condition in hand, we propose an equivalent ambiguity notion called local ambiguity for the convenience of SMT encoding. We translate local ambiguity into an SMT formula and developed a bounded ambiguity checker that automatically finds a shortest nonempty ambiguous sentence (if exists) for a user-input grammar. The soundness and completeness of our SMT encoding are mechanized in the Coq proof assistant. We conducted an evaluation on both grammar fragments and full grammars extracted from the language manuals of domain-specific languages like YAML as well as general-purpose languages like Python, which reveals the effectiveness of our approach.

Recently, learning embeddings of nodes in graphs has attracted increasing research attention. There are two main kinds of graph embedding methods, i.e., transductive embedding methods and inductive embedding methods. The former focuses on directly optimizing the embedding vectors, and the latter tries to learn a mapping function for the given nodes and features. However, little work has focused on applying the learned model from one graph to another, which is a pervasive idea in Computer Vision or Natural Language Processing. Although some of the graph neural networks (GNNs) present a similar motivation, none of them considers graph biases between graphs. In this paper, we present a novel graph embedding problem called Adaptive Task (AT), and propose a unified framework for the adaptive task, which introduces two types of alignment to learn adaptive node embeddings across graphs. Then, based on the proposed framework, a novel Graph Adaptive Embedding network (GraphAE) is designed to address the adaptive task. Furthermore, we extend GraphAE to a multi-graph version to consider a more complex adaptive situation. The extensive experimental results demonstrate that our model significantly outperforms the state-of-the-art methods, and also show that our framework can make a great improvement over a number of existing GNNs.

Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints. In this article, we propose a novel ordering consistency theory for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called Zord , and have conducted extensive experiments on the SV-COMP 2020 ConcurrencySafety benchmarks. Our experimental results show a significant improvement over the state-of-the-art.

In collaborative software development, programmers create software branches to add features and fix bugs tentatively, and then merge branches to integrate edits. When edits from different branches textually overlap (i.e., textual conflicts ) or lead to compilation and runtime errors (i.e., build and test conflicts ), it is challenging for developers to remove such conflicts. Prior work proposed tools to detect and solve conflicts. They investigate how conflicts relate to code smells and the software development process. However, many questions are still not fully investigated, such as what types of conflicts exist in real-world applications and how developers or tools handle them. For this article, we used automated textual merge, compilation, and testing to reveal three types of conflicts in 208 open-source repositories: textual conflicts, build conflicts (i.e., conflicts causing build errors), and test conflicts (i.e., conflicts triggering test failures). We manually inspected 538 conflicts and their resolutions to characterize merge conflicts from different angles. Our analysis revealed three interesting phenomena. First, higher-order conflicts (i.e., build and test conflicts) are harder to detect and resolve, while existing tools mainly focus on textual conflicts. Second, developers manually resolved most higher-order conflicts by applying similar edits to multiple program locations; their conflict resolutions share common editing patterns implying great opportunities for future tool design. Third, developers resolved 64% of true textual conflicts by keeping complete edits from either a left or right branch. Unlike prior studies, our research for the first time thoroughly characterizes three types of conflicts, with a special focus on higher-order conflicts and limitations of existing tool design. Our work will shed light on future research of software merge.

Termination is a fundamental liveness property for program verification. A loop bound is an upper bound of the number of loop iterations for a given program. The existence of a loop bound evidences the termination of the program. This paper employs a reinforced black-box learning approach for termination proving, consisting of a loop bound learner and a validation checker. We present efficient data-driven algorithms for inferring various kinds of loop bounds, including simple loop bounds, conjunctive loop bounds, and lexicographic loop bounds. We also devise an efficient validation checker by integrating a quick bound checking algorithm and a two-way data sharing mechanism. We implemented a prototype tool called ddlTerm. Experiments on publicly accessible benchmarks show that ddlTerm outperforms state-of-the-art termination analysis tools by solving 13-48% more benchmarks and saving 40--77% solving time.

Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing works, an SMT solver is simply treated as the backend. There is little research on improving SMT solving for concurrent program verification.

Abstract is an SMT-based multi-threaded program verification tool. It is built on top of (front-end) and (back-end). The basic idea of is to integrate into the SMT solver an ordering consistency theory that handles ordering relations over the shared variable accesses in the program. The front-end encodes the input program into an extended propositional formula that contains ordering constraints. The back-end is reinforced with a solver for the ordering consistency theory. This paper presents the basic idea, architecture, installation, and usage of .

The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.

Software systems evolve throughout their life cycles. Many revisions are produced over time. Verifying each revision of the software is impractical. Regression verification suggests reusing intermediate results from the previous verification runs. This paper studies regression verification via summary reuse. Not only procedure summaries, but also loop summaries are proposed to be reused. This paper proposes a fully automatic regression verification technique in the context of CEGAR. A lazy counterexample analysis technique is developed to improve the efficiency of summary reuse. We performed extensive experiments on two large sets of industrial programs (3,675 revisions of 488 Linux kernel device drivers). Results show that our summary reuse technique saves 84 to 93 percent analysis time of the regression verification.

Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial-order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks; the results show significant promotion of our approach.

Business organizations regularly collect customer data to improve their services. Organizations may want to share data within themselves or even with third-parties to maximize data utility. Since business data contain lots of customer data, organizations must respect customers' privacy expounded by privacy laws. In this paper, we present PSpec-SQL, a distributed data analytics system that automatically enforces privacy compliance for SQL queries. Our system provides a high-level language PSpec for the data owner to specify her data usage policy. As usual, the data analyst queries data to perform data analysis, but our system checks each query to ensure only policy-compliant queries are executed. We have implemented a prototype of PSpec-SQL on top of Spark-SQL, and carried out a case study on the TPC benchmarks. The results show the practicability of our system with negligible overhead over query processing.

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.

We propose a novel approach to proving the termination of imperative programs by k-induction. By our approach, the termination proving problem can be formalized as a k-inductive invariant synthesis task. On the one hand, k-induction uses weaker invariants than that required by the standard inductive approach. On the other hand, the base case of k-induction, which unrolls the program, can provide stronger pre-condition for invariant synthesis. As a result, the termination arguments of our approach can be synthesized more efficiently than the standard method. We implement a prototype of our k-inductive approach. The experimental results show the significant effectiveness and efficiency of our approach.

Almost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. Our approach automatically decomposes the runs of the probabilistic program into a finite union of ω-regular subsets and then proves almost-sure termination of each subset based on the notion of localized ranking supermartingales. Compared to the lexicographic methods and the compositional methods, our approach does not require a lexicographic order over the ranking supermartingales as well as the so-called unaffecting condition. Thus it has high generality. We present the algorithm of our approach and prove its soundness, as well as its relative completeness. We show that our approach can be applied to some hard cases and the evaluation on the benchmarks of previous works shows the significant efficiency of our approach.

Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.

Research on program termination has a long tradition. However, most of the existing techniques target a single program only. We propose in this paper an incremental termination analysis approach by reusing certified modules across different program versions. A transformation-based procedure is further developed to increase the reusability of certified modules. The proposed approach has wide applicability, applicable to various program changes. The proposed technique, to the best of our knowledge, represents a novel attempt to the termination analysis of evolving programs. We implemented the approach on top of Ultimate Automizer. Experimental results show dramatic improvement of our approach over the state-of-the-art tool.

Software products are evolving during their life cycles. Ideally, every revision need be formally verified to ensure software quality. Yet repeated formal verification requires significant computing resources. Verifying each and every revision can be very challenging. It is desirable to ameliorate regression verification for practical purposes. In this paper, we regard predicate analysis as a process of assertion annotation. Assertion annotations can be used as a certificate for the verification results. It is thus a waste of resources to throw them away after each verification. We propose to reuse the previously-yielded assertion annotation in regression verification. A light-weight impact-analysis technique is proposed to analyze the reusability of assertions. A novel assertion strengthening technique is furthermore developed to improve reusability of annotation. With these techniques, we present an incremental predicate analysis technique for regression verification. Correctness of our incremental technique is formally proved. We performed comprehensive experiments on revisions of Linux kernel device drivers. Our technique outperforms the state-of-the-art program verification tool CPAchecker by getting 2.8x speedup in total time and solving additional 393 tasks.

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, the current SMT solvers are designed for the general purpose of constraint solving. Many useful knowledge of programs cannot be utilized during the SMT solving. As a result, the SMT solver may spend a lot of effort to explore redundant search space. In this paper, we propose a novel approach for utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks, the results show orders of magnitude improvements of our approach.

Resolving conflicts is the main challenge for software merging. The existing merge tools usually rely on the developer to manually resolve conflicts. This is of course inefficient. We propose an interactive approach for resolving merge conflicts. To the best of our knowledge, this is the first attempt for conflict resolution of structured merge. To represent the possibly very large set of candidate programs, we propose an expressive and efficient representation by version space algebra. We also design a simple mechanism for ranking resolutions in the program space, such that the top-ranked resolution is very likely to meet the developer's expectation. We prototype our approach as a merge tool AutoMerge, and evaluate it on 244 real-world conflicts arising from 10 open-source projects. Results show great practicality of our approach.

Formal program verification is a powerful technique to ensure the correctness of programs. To perform this technique, one oftentimes needs to manually specify assertions, which is a time-consuming and error-prone task. Generating assertions automatically can significantly improve the usability of formal program verification. To decide where an assertion is needed heavily and which value range of the variable should be checked are the most challenging parts of assertion recommendation. This paper proposes the first assertion recommendation approach for program verification. With the help of machine learning techniques, the approach automatically decides whether a program function needs to add assertions. If an assertion is needed, the approach automatically recommends a variable that is most likely to occur in this assertion. Meanwhile, a value range of the variable is suggested. Our method of assertion recommendation has been integrated into Ceagle Online (a program verifier) and evaluated on the benchmarks of SV-COMP and CProver. Our best performance in assertion necessity classification can reach 92.1192% accuracy rate, 84.2281% precision rate and 86.8512% recall rate.

Probabilistic models are widely deployed in various systems. To ensure their correctness, verification techniques have been developed to analyze probabilistic systems. We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an Markov decision process. Different from previous works, weighted assumptions are introduced to attain completeness of our framework. Since weighted assumptions can be implicitly represented by multiterminal binary decision diagrams (MTBDDs), we give an >i /i<*-based learning algorithm for MTBDDs to infer weighted assumptions. Experimental results suggest promising outlooks for our compositional technique.

As a part of the international standard IEC 61375, the multifunction vehicle bus (MVB) has been used in most of the modern train control systems. It is highly desirable to check the temporal properties of the data transmitted on the bus. However, we are not aware of any published work on this problem. We proposed VeRV, the first temporal and data-concerned verification framework for the vehicle bus systems. A domain-specific language, called VeSpec, is proposed to specify the packet formats and the desired properties. The language is expressive, modular and easy to use. Given a VeSpec script, the VeRV allows automatic generation of runtime analyzer. We have applied our technique to a real tube train system and succeeded in diagnosing a real failure in this system. The industry application illustrates the effectiveness and efficiency of our technique.

We propose the first sound and complete learning-based compositional verification technique for probabilistic safety properties on concurrent systems where each component is an Markov decision process. Different from previous works, weighted assumptions are introduced to attain completeness of our framework. Since weighted assumptions can be implicitly represented by multi-terminal binary decision diagrams (MTBDD's), we give an L*-based learning algorithm for MTBDD's to infer weighted assumptions. Experimental results suggest promising outlooks for our compositional technique.

Temporal induction is one of the most popular SAT-based model checking techniques. It consists of two parts, the base case and the induction step. With the search length increment, both parts generate a sequence of SAT problems. This paper focuses on learnt clause replication and reuse in incremental temporal induction. Firstly, with the aid of assumption literals, we present an alternative clause replication scheme, which is much easier to implement than existing works. Secondly, based on our clause replication scheme, we present several clause reuse schemes to maximally explore the learnt clauses and their replications in temporal induction. Based on above ideas, we propose two new incremental temporal induction algorithms. Experimental results on a large number of benchmarks show significant performance improvement of our technique.

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the other hand, infers contextual assumptions by inspecting spurious erroneous traces. One would expect that their integration could further improve the capacity of model checking. Yet examining numerous erroneous traces to deduce contextual assumptions can be very time-consuming. The integration of symbolic model checking and assume-guarantee reasoning is thus far from clear. In this paper, we present a progressive witness analysis algorithm for automated assume-guarantee reasoning to exploit a multitude of traces from BDD-based symbolic model checkers. Our technique successfully integrates symbolic model checking with automated assume-guarantee reasoning by directly inferring BDD's as implicit assumptions. It outperforms monolithic symbolic model checking in four benchmark problems and an industrial case study in experiments.

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.

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.

This paper considers bounded model checking for extended labeled transition systems. Bounded model checking relies on a SAT solver to prove (or disprove) the existence of a counterexample with a bounded length. During the translation of a BMC problem to a SAT problem, much useful information is lost. This paper proposes an algorithm to analyze the transition system model, and then utilize the structure information hidden in the model to refine the decision ordering of variables in SAT solving. The basic idea is to guide the search process of SAT solving by the structure of the transition system. Experiments with this heuristic on real industrial designs show 5-12 times speedup over standard bounded model checking.

This paper presents a novel efficient satisfiability (SAT) algorithm based on maxterm covering. The satisfiability of a clause set is determined in terms of the number of relative maxterms of the empty clause with respect to the clause set. If the number of relative maxterms is zero, it is unsatisfiable, otherwise satisfiable. A set of synergic heuristic strategies are presented and elaborated. We conduct a number of experiments on 3-SAT and k-SAT problems at the phase transition region, which have been cited as the hardest group of SAT problems. Our experimental results on public benchmarks attest to the fact that, by incorporating our proposed heuristic strategies, our enhanced algorithm runs several orders of magnitude faster than the extension rule algorithm, and it also runs faster than zChaff and MiniSAT for most of k-SAT (k≥3) instances.

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.

Model checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We present an automated approach which combines compositional abstraction and counter-example guided abstraction refinement (CEGAR). The proposed approach exploits the semantics of a timed automaton to procure its over-approximative abstraction. Any safety property which holds on the abstraction is guaranteed to hold on the concrete model. In the case of a spurious counter-example, our proposed approach refines and strengthens the abstraction in a component-wise method. We implemented our method with the model checking tool Uppaal. Experimental results show promising improvements.

Model checking for large-scale systems is extremely difficult due to the state explosion problem. Creating useful abstractions for model checking task is a challenging problem, often involving many iterations of refinement. In this paper we consider techniques for model checking in the counter example-guided abstraction refinement. The state separation problem is one popular approach in counterexample-guided abstraction refinement, and it poses the main hurdle during the refinement process. To achieve effective minimization of the separation set, we present a novel probabilistic learning approach based on the sample learning technique, evolutionary algorithm, and effective heuristics. We integrate it with the abstraction refinement framework in the VIS model checker. We include experimental results on model checking to compare our new approach to recently published techniques. The benchmark results show that our approach has overall speedup of more than 56 percent against previous techniques. Our work is the first successful integration of evolutionary algorithm and abstraction refinement for model checking.

Automated compositional reasoning using assume-guarantee rules plays a key role in large system verification. A vexing problem is to discover fine decomposition of system contributing to appropriate assumptions. We present an automatic decomposition approach in compositional reasoning verification. The method is based on data mining algorithms. An association rule algorithm is harnessed to discover the hidden rules among system variables. A hypergraph partitioning algorithm is proposed to incorporate these rules as weight constraints for system variable clustering. The experiments demonstrate that our strategy leads to order-of-magnitude speedup over previous.

Model checking has been considered as a promising approach to establish the correctness of systems. Counterexample-guided abstraction refinement is a key strategy for model checking in verification of large-scale systems. State separation problem poses the main hurdle during the refinement. We present two fast heuristics to solve this problem. We prove the effectiveness of our heuristics by both theoretical analysis and experimental results. Experimental results show the promising performance of our approach.

Verification of complex system-on-a-chip (SoC) designs becomes a critical problem in practice. We consider using model checking to verify the correctness of such systems. We study the state separation problem in the framework of counterexample-guided abstraction refinement. We present two fast heuristics to solve this problem. To the best of our knowledge, our work is the first study on the effectiveness of greedy heuristics for this problem. In comparison with the latest work using the decision tree learning (DTL) solver, the proposed method performs about three orders of magnitude faster and the size of the separation set is 70% smaller on average.

article Share on A note on “a mapping algorithm for computer-assisted exploration in the design of embedded systems” Authors: Gang Chen Portland State University, Portland, OR Portland State University, Portland, ORView Profile , Xiaoyu Song Portland State University, Portland, OR Portland State University, Portland, ORView Profile , Feng Liu National Lab of Parallel Distributed Processing, Hunan, China National Lab of Parallel Distributed Processing, Hunan, ChinaView Profile , Qingping Tan National Lab of Parallel Distributed Processing, Hunan, China National Lab of Parallel Distributed Processing, Hunan, ChinaView Profile , Fei He Tsinghua University, Beijing, P.R. China Tsinghua University, Beijing, P.R. ChinaView Profile Authors Info & Claims ACM Transactions on Design Automation of Electronic SystemsVolume 12Issue 401 September 2007pp 52–eshttps://doi.org/10.1145/1278349.1278365Published:01 September 2007Publication History 0citation220DownloadsMetricsTotal Citations0Total Downloads220Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

Program verification plays an important role in assuring the reliability of software systems. This paper presents a novel verification methodology for Java programs based on the higher-order logic theorem proving system HOL. The soundness of a Java program in accordance with its specification in annotation is established in HOL4. A Hoare-logic based verification methodology (WHY) guides the verification process. As a case study, a Java program with four methods is specified in JML annotation and proved in HOL. The flexible manipulation of pure method call in annotation is presented in the HOL proof mechanism. This work may constitute the first attempt on using the proving system HOL for Java programs. The experience demonstrates the effectiveness and the promising results of the approach

Interconnect congestion estimation plays an important role in design automation of VLSI designs. This paper presents a novel probabilistic approach to predict the wiring space in two-dimensional arrays. We propose a hierarchical estimation method to derive approximated upper bounds for the wiring space, and we use the net density distribution to predict the routing congestion. Experimental results demonstrate the promising performance of the approach.