Content area

Abstract

Translate

Conference Title: 2023 12th Mediterranean Conference on Embedded Computing (MECO)

Conference Start Date: 2023, June 6

Conference End Date: 2023, June 10

Conference Location: Budva, Montenegro

Configurable software systems today are becoming very popular. They can produce a set of related programs by choosing preferable features (configuration options) at compile-time. Many configurable programs are applied in safety-critical areas, so their formal verification is of primary importance. In this paper, we introduce a new, interesting approach for verifying temporal properties of configurable programs that contain numerical features. We extend an abstract interpretation-based static analysis framework for proving temporal properties of single programs that uses a decision tree abstract domain. In particular, we define a novel lifted decision tree domain for proving temporal properties of configurable programs. We have developed a lifted static analyzer for proving temporal properties of #if-enriched C configurable programs. The evaluation on a range of loop benchmarks from SV-COMP confirms the effectiveness of our approach.

Details

Key topics
Powered by Web of Science® Description for Powered by Web of Science
Static analysis;
Software;
Abstract interpretation
Subject
Benchmarks;
Decision trees;
Configurable programs;
Safety critical;
Software
Identifier / keyword
Static analysis; Software; Abstract interpretation
Title
On Verifying Temporal Properties of Configurable Software
Author
Dimovski, Aleksandar S 1 ; Fetaji, Bekim 1 

1  Mother Teresa University - Skopje,Skopje,Rep. of North Macedonia 
Publication title
The Institute of Electrical and Electronics Engineers, Inc. (IEEE) Conference Proceedings; Piscataway
Source details
2023 12th Mediterranean Conference on Embedded Computing (MECO)
Publication year
2023
Publication date
2023
Publisher
The Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Place of publication
Piscataway
Country of publication
United States
Publication subject
Engineering--Electrical Engineering
Source type
Conference Paper
Language of publication
English
Document type
Conference Proceedings
Publication history
 
 
Online publication date
2023-06-26
Publication history
 
 
   First posting date
26 Jun 2023
DOI
https://doi.org/10.1109/MECO58584.2023.10155049
ProQuest document ID
2830413013
Document URL
https://www.proquest.com/conference-papers-proceedings/on-verifying-temporal-properties-configurable/docview/2830413013/se-2?accountid=208611
Copyright
Copyright The Institute of Electrical and Electronics Engineers, Inc. (IEEE) 2023
Last updated
2024-10-03
Database
ProQuest One Academic