Search for Articles:
Title / Keyword
Author / Affiliation / Email
Journal
Article Type
 
 
Advanced Search
 
Section
Special Issue
Volume
Issue
Number
Page
 
4.5
2.7
Journals
Applied Sciences
Special Issues
Static Analysis Techniques: Recent Advances and New Horizons
share announcement

Static Analysis Techniques: Recent Advances and New Horizons

A special issue of Applied Sciences (ISSN 2076-3417). This special issue belongs to the section "Computing and Artificial Intelligence".

Deadline for manuscript submissions: closed (30 September 2021) | Viewed by 11842

Special Issue Editors

Prof. Dr. Agostino Cortesi

E-Mail Website
Guest Editor
Dipartimento di Scienze Ambientali, Informatica e Statistica, Università Ca’ Foscari, Via Torino 155, 30170 Venice, Italy
Interests: static program analysis; software engineering; abstract interpretation; information flow security
Special Issues, Collections and Topics in MDPI journals
Dr. Pietro Ferrara

E-Mail Website
Guest Editor
JuliaSoft Srl, Verona, Italy
Interests: static analysis; abstract interpretation; object-oriented programming languages

Special Issue Information

Dear Colleagues,

We cordially invite you to consider submitting a paper to the Special Issue of the journal Applied Sciences (ISSN 2076-3417; IF 2.217) on “Static Analysis Techniques: Recent Advances and New Horizons”.

Static analysis is currently recognized as a key mean for enhancing software security and reliability. It is widely recognized as a fundamental approach for program verification, bug detection, compiler optimization, program understanding, and software maintenance. In fact, a white-box semantics-based approach to the analysis of source code can automatically reveal errors that do not manifest until a disaster occurs weeks, months or years after release, which might be very difficult to reproduce and that might not be captured by testing, as tests can only cover a finite number of execution traces. Several techniques have been introduced in the scientific literature, and several tools implementing such techniques are currently in use on software written in different programming language targets and focusing on different program properties.

This Special Issue is aimed at collecting new contributions in this area, ranging from the introduction of new techniques to their practical implementation and applications with a particular emphasis on applied aspects, i.e., on the issues related to scalability, interoperability, and maintainability of static analysis tools in highly demanding real scenarios.

Contributions are welcome on all aspects of static analysis, including, but not limited to:

  • Abstract Interpretation;
  • Data-flow and control-flow analysis;
  • Model checking;
  • Program verification;
  • Program certification;
  • Security analysis;
  • Type checking.

Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, and object-oriented programming.

Extended versions of papers presented in international conferences are welcome if the extended version contains significant additions which were not in the conference version of the paper. In this case, the authors are invited to submit a cover letter explaining how the submitted paper differs from the conference one.

Prof. Dr. Agostino Cortesi
Dr. Pietro Ferrara
Guest Editors

Manuscript Submission Information

Manuscripts should be submitted online at www.mdpi.com by registering and logging in to this website. Once you are registered, click here to go to the submission form. Manuscripts can be submitted until the deadline. All submissions that pass pre-check are peer-reviewed. Accepted papers will be published continuously in the journal (as soon as accepted) and will be listed together on the special issue website. Research articles, review articles as well as short communications are invited. For planned papers, a title and short abstract (about 100 words) can be sent to the Editorial Office for announcement on this website.

Submitted manuscripts should not have been published previously, nor be under consideration for publication elsewhere (except conference proceedings papers). All manuscripts are thoroughly refereed through a single-blind peer-review process. A guide for authors and other relevant information for submission of manuscripts is available on the Instructions for Authors page. Applied Sciences is an international peer-reviewed open access semimonthly journal published by MDPI.

Please visit the Instructions for Authors page before submitting a manuscript. The Article Processing Charge (APC) for publication in this open access journal is 2400 CHF (Swiss Francs). Submitted papers should be well formatted and use good English. Authors may use MDPI's English editing service prior to publication or during author revisions.

Keywords

  • Abstract interpretation
  • Data-flow and control-flow analysis
  • Model checking
  • Program cerification
  • Program certification
  • Security analysis
  • Type checking

Published Papers (4 papers)

Download All Papers
Order results
Result details
Show export options expand_more Show export options expand_less
Select all
Export citation of selected articles as:

Research

27 pages, 1482 KiB  
Article
An Approach for Detecting Feasible Paths Based on Minimal SSA Representation and Symbolic Execution
by Abdalla Wasef Marashdih, Zarul Fitri Zaaba and Khaled Suwais
Appl. Sci. 2021, 11(12), 5384; https://0-doi-org.brum.beds.ac.uk/10.3390/app11125384 - 10 Jun 2021
Cited by 3 | Viewed by 2908
Abstract
Static analysis is one of the techniques used today to analyze source codes and minimize the issue of software vulnerability. Static analysis has the ability to observe all possible software paths in an application through the scrutiny of a web application’s source code. [...] Read more.
Static analysis is one of the techniques used today to analyze source codes and minimize the issue of software vulnerability. Static analysis has the ability to observe all possible software paths in an application through the scrutiny of a web application’s source code. Among those paths, some may be considered feasible paths, which refer to any paths that the test cases can execute. The detection of feasible paths in the results of a static analysis helps to minimize the false positive rate. However, the detection of feasible paths can be challenging, especially for programs that have multiple conditions in the same branch. The aim is to ensure that each feasible path is detected only once (not duplicated). This paper proposes an approach based on minimal static single assignment (MSSA) form and symbolic execution to detect feasible paths. The proposed approach starts by converting the source code into an abstract syntax tree (AST), followed by converting the AST to minimal SSA representation, which helps to decrease the number of instructions in the SSA form. An algorithm was built to examine all of the instructions of the SSA form, identify whole paths in the source code, and extract constraints along each path. A path weight method (PWM) is proposed in this work to avoid detecting duplicated feasible paths. The satisfiability modulo theory (SMT) solver was used to check the satisfiability of each path condition. The proposed approach was tested on seven well-known test programs that have been used in related studies and 10 large scale programs. The experimental results indicate that the proposed method (PWM) can avoid detecting duplicated feasible paths, and the proposed approach reduced the time required for generating the paths compared to that in related studies. Full article
(This article belongs to the Special Issue Static Analysis Techniques: Recent Advances and New Horizons)
►▼ Show Figures

Figure 1

33 pages, 563 KiB  
Article
Abstracting Strings for Model Checking of C Programs
by Henrich Lauko, Martina Olliaro, Agostino Cortesi and Petr Roc̆kai
Appl. Sci. 2020, 10(21), 7853; https://0-doi-org.brum.beds.ac.uk/10.3390/app10217853 - 05 Nov 2020
Viewed by 2105
Abstract
Data type abstraction plays a crucial role in software verification. In this paper, we introduce a domain for abstracting strings in the C programming language, where strings are managed as null-terminated arrays of characters. The new domain M-String is parametrized on an index [...] Read more.
Data type abstraction plays a crucial role in software verification. In this paper, we introduce a domain for abstracting strings in the C programming language, where strings are managed as null-terminated arrays of characters. The new domain M-String is parametrized on an index (bound) domain and a character domain. By means of these different constituent domains, M-Strings captures shape information on the array structure as well as value information on the characters occurring in the string. By tuning these two parameters, M-String can be easily tailored for specific verification tasks, balancing precision against complexity. The concrete and the abstract semantics of basic operations on strings are carefully formalized, and soundness proofs are fully detailed. Moreover, for a selection of functions contained in the standard C library, we provide the semantics for character access and update, enabling an automatic lifting of arbitrary string-manipulating code into our new domain. An implementation of abstract operations is provided within a tool that automatically lifts existing programs into the M-String domain along with an explicit-state model checker. The accuracy of the proposed domain is experimentally evaluated on real-case test programs, showing that M-String can efficiently detect real-world bugs as well as to prove that program does not contain them after they are fixed. Full article
(This article belongs to the Special Issue Static Analysis Techniques: Recent Advances and New Horizons)
►▼ Show Figures

Figure 1

48 pages, 906 KiB  
Article
An Abstraction Technique for Verifying Shared-Memory Concurrency
by Wytse Oortwijn, Dilian Gurov and Marieke Huisman
Appl. Sci. 2020, 10(11), 3928; https://0-doi-org.brum.beds.ac.uk/10.3390/app10113928 - 05 Jun 2020
Cited by 5 | Viewed by 2659
Abstract
Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical [...] Read more.
Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus primarily on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that balances expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol. Full article
(This article belongs to the Special Issue Static Analysis Techniques: Recent Advances and New Horizons)
►▼ Show Figures

Figure 1

34 pages, 648 KiB  
Article
Static Analysis for ECMAScript String Manipulation Programs
by Vincenzo Arceri, Isabella Mastroeni and Sunyi Xu
Appl. Sci. 2020, 10(10), 3525; https://0-doi-org.brum.beds.ac.uk/10.3390/app10103525 - 20 May 2020
Cited by 10 | Viewed by 2982
Abstract
In recent years, dynamic languages, such as JavaScript or Python, have been increasingly used in a wide range of fields and applications. Their tricky and misunderstood behaviors pose a great challenge for static analysis of these languages. A key aspect of any dynamic [...] Read more.
In recent years, dynamic languages, such as JavaScript or Python, have been increasingly used in a wide range of fields and applications. Their tricky and misunderstood behaviors pose a great challenge for static analysis of these languages. A key aspect of any dynamic language program is the multiple usage of strings, since they can be implicitly converted to another type value, transformed by string-to-code primitives or used to access an object-property. Unfortunately, string analyses for dynamic languages still lack precision and do not take into account some important string features. In this scenario, more precise string analyses become a necessity. The goal of this paper is to place a first step for precisely handling dynamic language string features. In particular, we propose a new abstract domain approximating strings as finite state automata and an abstract interpretation-based static analysis for the most common string manipulating operations provided by the ECMAScript specification. The proposed analysis comes with a prototype static analyzer implementation for an imperative string manipulating language, allowing us to show and evaluate the improved precision of the proposed analysis. Full article
(This article belongs to the Special Issue Static Analysis Techniques: Recent Advances and New Horizons)
►▼ Show Figures

Figure 1

Show export options expand_more Show export options expand_less
Select all
Export citation of selected articles as:
 
Displaying articles 1-4
Back to TopTop