scholarly journals Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints

2021 ◽  
pp. 438-442
Author(s):  
Simmo Saan ◽  
Michael Schwarz ◽  
Kalmer Apinis ◽  
Julian Erhard ◽  
Helmut Seidl ◽  
...  
Keyword(s):  
Static Analysis ◽  
Abstract Interpretation ◽  
Analysis Framework ◽  
Data Race ◽  
C Programs ◽  
Global Invariants ◽  
Race Analysis

AbstractGoblintis a static analysis framework for C programs specializing in data race analysis. It relies on thread-modular abstract interpretation where thread interferences are accounted for by means of flow-insensitive global invariants.

scholarly journals Loopfrog — loop summarization for static analysis

10.29007/g3fd ◽  
2018 ◽  
Author(s):  
Daniel Kroening ◽  
Natasha Sharygina ◽  
Stefano Tonetta ◽  
Aliaksei Tsitovich ◽  
Christoph M. Wintersteiger
Keyword(s):  
Model Checking ◽  
Static Analysis ◽  
Abstract Interpretation ◽  
C Programs ◽  
Run Time ◽  
Fix Point

Loopfrog is a scalable static analyzer for ANSI-C programs, that combines the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it does not calculate the abstract fix-point of a program by iterative application of an abstract transformer. Instead, it calculates symbolic abstract transformers for program fragments (e.g., loops) using a loop summarization algorithm. Loopfrog computes abstract transformers starting from the inner-most loops, which results in linear (in the number of the looping constructs) run-time of the sum- marization procedure and which is often considerably smaller than the traditional saturation procedure of abstract interpetation. It also provides “leaping” counterexamples to aid in the diagnosis of errors.

A Survey of Parametric Static Analysis

2021 ◽  
Vol 54 (7) ◽  
pp. 1-37
Author(s):  
Jihyeok Park ◽  
Hongki Lee ◽  
Sukyoung Ryu
Keyword(s):  
Recent Work ◽  
Static Analysis ◽  
Abstract Interpretation ◽  
Black Box ◽  
Parameter Selection ◽  
Survey Analysis ◽  
Future Directions ◽  
Analysis Techniques ◽  
Analysis Quality

Understanding program behaviors is important to verify program properties or to optimize programs. Static analysis is a widely used technique to approximate program behaviors via abstract interpretation. To evaluate the quality of static analysis, researchers have used three metrics: performance, precision, and soundness. The static analysis quality depends on the analysis techniques used, but the best combination of such techniques may be different for different programs. To find the best combination of analysis techniques for specific programs, recent work has proposed parametric static analysis . It considers static analysis as black-box parameterized by analysis parameters , which are techniques that may be configured without analysis details. We formally define the parametric static analysis, and we survey analysis parameters and their parameter selection in the literature. We also discuss open challenges and future directions of the parametric static analysis.

scholarly journals Enhancing the Security of C/C++ Programs using Static Analysis

2016 ◽  
Vol 9 (44) ◽  
Author(s):  
Subburaj Ramasamy ◽  
Anuj Singh ◽  
Deepak Singal
Keyword(s):  
Static Analysis ◽  
C Programs

scholarly journals Building a modular static analysis framework in Scala (tool paper)

2016 ◽  
Author(s):  
Quentin Stiévenart ◽  
Jens Nicolay ◽  
Wolfgang De Meuter ◽  
Coen De Roover
Keyword(s):  
Static Analysis ◽  
Analysis Framework

SharpChecker: Static analysis tool for C# programs

2017 ◽  
Vol 43 (4) ◽  
pp. 268-276 ◽  
Author(s):  
V. K. Koshelev ◽  
V. N. Ignatiev ◽  
A. I. Borzilov ◽  
A. A. Belevantsev
Keyword(s):  
Static Analysis ◽  
Analysis Tool ◽  
C Programs ◽  
Static Analysis Tool

Verification of Non-Functional Requirements by Abstract Interpretation

2012 ◽  
pp. 22-35
Author(s):  
Agostino Cortesi ◽  
Francesco Logozzo
Keyword(s):  
Static Analysis ◽  
Abstract Interpretation ◽  
Software Requirements ◽  
Functional Requirements ◽  
Formal Approach ◽  
Space Efficiency ◽  
Source Program ◽  
Service Oriented ◽  
Abstract Domains ◽  
Functional Software

This chapter investigates a formal approach to the verification of non-functional software requirements that are crucial in Service-oriented Systems, like portability, time and space efficiency, and dependability/robustness. The key-idea is the notion of observable, i.e., an abstraction of the concrete semantics when focusing on a behavioral property of interest. By applying an abstract interpretation-based static analysis of the source program, and by a suitable choice of abstract domains, it is possible to design formal and effective tools for non-functional requirements validation.

Sign in / Sign up

Export Citation Format

Share Document