English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Lifted (family-based) static analysis by abstract interpretation is capableof analyzing all variants of a program family simultaneously, in a single runwithout generating any of the variants explicitly. The elements of theunderlying lifted analysis domain are tuples, which maintain one property pervariant. Still, explicit property enumeration in tuples, one by one for allvariants, immediately yields combinatorial explosion. This is particularlyapparent in the case of program families that, apart from Boolean features,contain also numerical features with big domains, thus admitting astronomicconfiguration spaces.  The key for an efficient lifted analysis is proper handling ofvariability-specific constructs of the language (e.g., feature-based runtimetests and #if directives). In this work, we introduce a new symbolicrepresentation of the lifted abstract domain that can efficiently analyzeprogram families with numerical features. This makes sharing between propertyelements corresponding to different variants explicitly possible. The elementsof the new lifted domain are constraint-based decision trees, where decisionnodes are labeled with linear constraints defined over numerical features andthe leaf nodes belong to an existing single-program analysis domain. Toillustrate the potential of this representation, we have implemented anexperimental lifted static analyzer, called SPLNUM^2Analyzer, for inferringinvariants of C programs. It uses existing numerical domains (e.g., intervals,octagons, polyhedra) from the APRON library as parameters. An empiricalevaluation on benchmarks from SV-COMP and BusyBox yields promising preliminaryresults indicating that our decision trees-based approach is effective andoutperforms the tuple-based approach, which is used as a baseline liftedanalysis based on abstract interpretation.

A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features (Extended Version)