FuSeBMC IA: Interval Analysis and Methods for Test Case Generation (Competition Contribution)

Mohannad Aldughaim, Kaled M. Alshmrany, Mikhail R. Gadelha, Rosiane de Freitas, Lucas C. Cordeiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

The cooperative verification of Bounded Model Checking and Fuzzing has proved to be one of the most effective techniques when testing C programs. FuSeBMC is a test-generation tool that employs BMC and Fuzzing to produce test cases. In Test-Comp 2023, we present an interval approach to FuSeBMC IA, improving the test generator to use interval methods and abstract interpretation (via Frama-C) to strengthen our instrumentation and fuzzing. Here, an abstract interpretation engine instruments the program as follows. It analyzes different program branches, combines the conditions of each branch, and produces a Constraint Satisfaction Problem (CSP), which is solved using Constraint Programming (CP) by interval manipulation techniques called Contractor Programming. This process has a set of invariants for each branch, which are introduced back into the program as constraints. Experimental results show improvements in reducing CPU time (37%) and memory (13%), while retaining a high score.
Original languageEnglish
Title of host publicationFASE2023: 26th International Conference on Fundamental Approaches to Software Engineering
Publication statusAccepted/In press - 4 Mar 2023
EventFASE2023: 26th International Conference on Fundamental Approaches to Software Engineering - Paris, France
Duration: 22 Apr 202327 Apr 2023

Conference

ConferenceFASE2023: 26th International Conference on Fundamental Approaches to Software Engineering
Country/TerritoryFrance
CityParis
Period22/04/2327/04/23

Keywords

  • Automated Test-Case Generation
  • Bounded Model Checking
  • Fuzzing
  • Abstract Interpretation
  • Constraint Programming
  • Contractors

Fingerprint

Dive into the research topics of 'FuSeBMC IA: Interval Analysis and Methods for Test Case Generation (Competition Contribution)'. Together they form a unique fingerprint.

Cite this