We propose and develop a framework for validating smart contracts derived from e-contracts. The goal is to ensure the generated smart contracts fulfil all the conditions outlined in their corresponding e-contracts. By confirming alignment between the smart contracts and their original agreements, this approach enhances trust and reliability in automated contract execution. The proposed framework will systematically compare and validate the terms and clauses of the e-contracts with the logic of the smart contracts. This validation confirms that the agreement is accurately translated into executable code. Automated verification identifies issues between the e-contracts and their smart contract counterparts. This proposed work will solve the problems of gap between legal language and code execution, this framework ensures seamless integration of smart contracts into the existing legal framework.

Abstract ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the category of Test-Comp 2025.

Exploring all the feasible paths in order to generate test cases is costly when dynamic symbolic execution is considered. Hence, there comes the interpolation concept that minimizes the cost to some extent. The earlier work on custom interpolation introduced a resource annotator that instruments the program and generates multiple meta programs (LLVM IRs) in order to generate optimal MCD/DC-based test cases. The proposed approach leverages a Meta Program Generator (MPG) to create a single meta program that encapsulates SC-MCC sequences within “assert” statements, aligned with their corresponding predicates. The effectiveness of this approach is demonstrated through experiments on benchmark programs, comparing it with traditional methods. The results indicate improved efficiency and the generation of a higher number of feasible SC-MCC sequences, making our approach a promising advancement in software testing and symbolic execution. We experimented with 75 Rigorous Examination of Reactive Systems (RERS) benchmark programs for experimentation. It is observed that our implementation has obtained more feasible SC-MCC sequences in 41 out of 75 programs.

Unique-Cause MC/DC (UCM) is the most desired form of MC/DC in many safety-critical applications. For a given predicate, the UCM considers the independent pair of each condition by flipping the corresponding condition and fixing the other conditions. For the given N conditions in a predicate, the existing static symbolic execution tool, CBMC, generates MC/DC (Modified Condition/Decision) goal constraints of size, N + 1 that constitutes its minimal independent pairs. However, we propose a novel UCM Sequence Generator (UCM-Gen) that generates all possible inequality comparisons of the sequences/combinations of the N conditions which helps in computing the independent pairs further. The UCM-Gen outputs UCM Annotated Program which when given to the program verifiers, produces the UCM Score (%). In our work, we have considered CBMC to get the SAT/UNSAT results for each sequence of the UCM Annotated Program. Upon analysing these results, we calculate the total number of independently affected conditions (i.e., I value) for all the predicates in the given program. Furthermore, this work is compared with the CBMC's mode of MC/DC implementation. Interestingly, our proposed approach based UCM score (%) is always greater than the CBMC's MC/DC score (%) and hence claiming that their corresponding test cases contribute in effective bug finding.

Bug reproduction is becoming an important task in the security analysis of Solidity smart contracts. By simulating attacks, developers and auditors can better understand how a vulnerability is triggered in practice. To reproduce a bug, one often needs to define an attacker contract and a specific sequence of interactions that exploit the vulnerability. However, in smart contracts, there are rarely automated tools that can generate such contracts and sequences and validate their correctness. Existing security tools, such as formal verifiers, are effective at detecting bugs, but they are not designed for bug reproduction. They often omit execution traces or produce incomplete ones. Moreover, their reports rarely reflect the behaviour patterns of attacker contracts. This gap motivates our work. We propose VeriExploit, a framework that combines formal methods and large language models to automatically generate, validate, and refine reproduction contracts and execution steps. Given a vulnerable contract and its counterexample, VeriExploit produces a contract that re-triggers the same bug and outputs a concrete trace showing how the exploit works. Experiments show that VeriExploit is effective at automating bug reproduction, achieving a success rate of 85.60% on our benchmark dataset.

Fuzz testing is one of the popular techniques for evaluating software reliability. Its effectiveness largely depends on the quality and diversity of the initial seed inputs. Traditionally, these seeds are generated randomly, which may limit the effectiveness of the fuzzing process. However, generating seeds based on an analysis of the target code can significantly improve the performance of these tools. To address this, we proposed a Large Language Model (LLM)-based seed generation approach for effective fuzzing and named it gptPromptFuzz. In our approach, initially, one meta-prompt is designed in accordance with the objective of diverse seed generation. To further enhance diversity, we construct ten additional prompts that are semantically equivalent to the meta-prompt. Each of these prompts is independently processed by LLM to produce unique seeds. The experimental results demonstrated that the proposed gptPromptFuzz outperformed random AFL in generating seeds effectively, with reduced execution time, in all 45 benchmark C programs. Further, a larger number of paths are obtained in 41 out of 45 programs.

Designing interactive UI templates is a challenging task. Designers often struggle to determine the best design choices, and even experienced professionals spend significant time evaluating layouts. Moreover, assessing whether a design is good or bad for users remains difficult. This study aims to develop a framework for predicting and scoring the placement of interactive UI elements. By providing usability scores for element placement, our goal is to help trace the users in-teraction and make it more efficient and assist designers in optimizing their layouts. The You Only Look Once (YOLO) model is employed to detect interactive elements in UI screen-shots and evaluate their placement on a usability scale. The model predicts element positions and usability scores, enabling designers to refine their layouts based on data-driven insights. The model evaluates UI designs by identifying interactive elements and assigning usability scores. Designers can use these scores to assess the effectiveness of their layouts and make informed improvements without direct position suggestions. Our approach enhances UI usability, helping designers create more effective interfaces aligned with current design trends.

Abstract Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. The major advantage of DSE is its path-by-path exploration of the program execution space. However, this often leads to the path explosion problem. To address this issue, a method of abstraction learning has been used. The key step here is the computation of an interpolant to represent the learned abstraction. In Test-Comp 2024, we use two different approaches of interpolant generation viz., Deletion Interpolation and Weakest Precondition Interpolation. The former is our more stable and mature system and briefly discussed in [8]. In this paper, we present the latter approach which is the heart of TracerX. In general, the Weakest Precondition (WP) is the ideal (most general) interpolant. However, WP is intractable to compute and is exponentially disjunctive. A major challenge is to obtain a conjunctive approximation of the WP. Therefore, we generate an approximation of the WP.

Advancements in blockchain technologies empower society with trust-based applications. Smart contracts, which are programs designed to facilitate activities on the blockchain, serve as important instruments for executing agreements. Smart contracts are established among involved parties to codify their respective requirements and commitments. In various situations, where a smart contract manages substantial and valuable transactions, the likelihood of encountering issues and asset losses increases significantly. Therefore, it becomes essential to verify and test smart contracts thoroughly. In this paper, we present a new tool to measure condition coverage criterion for smart contracts using Solidity-based model checkers. We demonstrate the process of annotating the original smart contract by the condition coverage properties and employ the model checker to validate the feasibility of the specified properties. Further, we assess the properties instrumented to compute the condition coverage score. We conducted experiments on 70 smart contracts, employing both the Bounded Model Checker (BMC) and Constrained Horn Clauses (CHC). Our findings demonstrate BMC's superior performance compared to CHC. The tool we propose assists smart contract developers in verifying their code through condition coverage analysis. Utilizing both model checkers in tandem contributes to enhancing the quality of smart contracts, as the outcome may vary, and either of the checkers might yield superior condition coverage. Video-cast: https://youtu.beI13kuIjpPGPI?si=YQIWYPJhp7vzORI4

The important contribution that large language models (LLMs) have made to the development of a new software testing era is the main objective of this proposed approach. It emphasizes the role that LLMs play in producing complex and diverse input seeds, which opens the way for efficient bug discovery. In the study we also introduce a systematic approach for combining various input values, employing the principles of Combinatorial testing using the PICT (Pairwise independent Combinatorial testing). By promoting a more varied set of inputs for thorough testing, PICT enhances the seed production process. Then we show how these different seeds may be easily included in the American Fuzzy Lop (AFL) tool, demonstrating how AFL can effectively use them to find and detect software flaws. This integrated technique offers a powerful yet straightforward approach to software Quality.

Modified Condition/Decision Coverage (MC/DC) is an important criterion to test the safety-critical applications because it generates test cases in a linear manner from N + 1 to 2 N , where N is the number of Atomic Conditions in a given predicate. It is desirable in comparison to the exponential test cases produced for Multiple Condition Coverage (MCC), i.e., 2 N . However, MCC with Short-Circuit (SC-MCC) is recommended since most of the safety-critical applications are built on the high-level languages that use Short-Circuit evaluation property. Our goal is to demonstrate that, despite the added overhead, the SC-MCC coverage-based test cases have a high error-detection probability compared to that of MC/DC. In this work, we have considered the CBMC tool to generate both the SC-MCC and MC/DC test cases for 80 RERS benchmark programs . Then, by optimizing the traditional Mutation Testing (using the GCOV tool), we computed the Mutation Score (%) to assess the quality of the generated test cases . As per the Mutation analysis, the proposed SC-MCC outperformed MC/DC for over 75% of the 80 RERS programs considered. Additionally, as per the Execution time analysis, the average total time taken to evaluate the MC/DC part of the proposed framework is 3065.98 s, whereas SC-MCC framework evaluation took 2167.70 s. This proves the efficiency of the proposed (SC-MCC) work over the traditional criterion (MC/DC) based work.

Fuzzing is a popular and highly effective technique for software testing especially vulnerability detection. Fuzzing includes the random mutation of well-formed program inputs using dynamic program analysis. Though fuzzing is an active area of research, less systematic efforts have been investigated to understand as well as to generate powerful input seeds for a fuzzer. Reactive systems are used in different applications such as web services, decision support systems, and logical controllers. These systems are quite complex and bigger, hence the validation process becomes tedious. In this work, we propose a static seed generator that helps to accelerate the performance of existing fuzzers. In this paper, we validate the reactive systems using our approach by detecting vulnerability. To evaluate the performance of our developed seeder, we experimented with 100 Rigorous Ex-amination of Reactive Systems (RERS) C-programs. Experimental results show that our approach SSG-AFL is superior as compared to the AFL with random seeds. SSG-AFL shows 59.75% winning programs after running all four phases as compared to Random-AFL.

In this paper, we propose and develop a real-time profiler to validate the strong coverage criteria such as Modified Condition/Decision Coverage (MC/DC) and Multiple Condition Coverage with Short Circuit (SC-MCC). We named our new tool as gMCov, which is a gCov based profiler. Currently, the existing gCov profiler gives line coverage and branch coverage. As we know, line and branch coverages are weak coverage criteria. Since there exists no profiler to produce the information of feasible sequence properties of either MC/DC or SC-MCC, it is important to have a tool that validates these coverage criteria based on their final scores. Hence, we proposed a new profiler i.e. gMCov which is a generalized tool that can be plugged with any test case generator. It requires a set of test cases and a program to produce the score (%) with a detailed report. The overhead of the gMCov execution time is considerable i.e., 0.68 (s) for MC/DC and 1.26 (s) for SC-MCC, thus proving its efficiency.

MC/DC coverage prescribes a set of MC/DC sequences. Such a sequence is defined by a specification of the truth values of certain atomic boolean expressions which appear in predicates (i.e. boolean combinations of atomic boolean expressions) in the program. An execution trace satisfies the sequence if it realizes the atomic boolean conditions in accordance with the truth value specification of the sequence. An MC/DC sequence is feasible if there is one such execution trace. The overall goal for an MC/DC test generator is, for each sequence: if feasible, to generate a test input realizing the sequence; otherwise, to prove that the sequence is infeasible.

Dynamic Symbolic Execution (DSE) is an important method for testing of programs. An important system on DSE is KLEE [ 1 ] which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion . The method of abstraction learning [ 7 ] has been used to address this. The key step here is the computation of an interpolant to represent the learned abstraction. TracerX, our tool, is built on top of KLEE and it implements and utilizes abstraction learning . The core feature in abstraction learning is subsumption of paths whose traversals are deemed to no longer be necessary due to similarity with already-traversed paths. Despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often brings significant overall benefits. In particular, TracerX can fully explore many programs that would be impossible for any non-pruning system like KLEE to do so.

Distributed concolic testing (DCT) for complex programs takes a remarkable computational time. Also, the achieved modified condition/decision coverage (MC/DC) for such programs is often inadequate. We propose an improved DCT approach that reduces the computational time and simultaneously enhanced the MC/DC. We have named our approach SMCDCT (scalable MC/DC percentage calculator using DCT). Our experimental study on forty-five C programs indicates 6.62% of average increase in MC/DC coverage. Copyright © 2016 John Wiley & Sons, Ltd.

Modified Condition / Decision Coverage (MC/DC) is the second strongest coverage criterion in white-box testing.According to DO178C/RTCA criterion it is mandatory to achieve Level A certification for MC/DC.Concolic testing is the combination of Concrete and Symbolic execution.It is a systematic technique that performs symbolic execution but uses randomlygenerated test inputs to initialize the search and to allow the tool to execute programs when symbolic execution fails.In this paper, we extend concolic testing by computing MC/DC using the automatically generated test cases.On the other hand Feedback-Directed Random Test Generation builds inputs incrementally by randomly selecting a method call to apply and find arguments from among previously-constructed inputs.As soon as the input is built, it is executed and checked against a set of contracts and filters.In our proposed work, we combine feedback-directed test cases generation with concolic testing to form Java-Hybrid Concolic Testing (Java-HCT).Java-HCT generates more number of test cases since it combines the features of both Feedback-Directed Random Test and Concolic Testing.Hence, through Java-HCT, we achieve high MC/DC.Combinations of approaches represent different tradeoffs of completeness and scalability.We develop Java-HCT using RANDOOP, jCUTE, and COPECA.Combination of RANDOOP and jCUTE creates more test cases.COPECA is used to measure MC/DC% using the generated test cases.Experimental study shows that Java-HCT produces better MC/DC% than individual testing techniques(feedback-directed random testing and concolic testing).We have improved MC/DC by ×1.62 and by ×1.26 for feedback-directed random testing and concolic testing respectively.