Academic literature on the topic 'Abstract Interpretation, Abstract Domain, Program Analysis, Partial Completeness'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Abstract Interpretation, Abstract Domain, Program Analysis, Partial Completeness.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Abstract Interpretation, Abstract Domain, Program Analysis, Partial Completeness"

1

Campion, Marco, Mila Dalla Preda, and Roberto Giacobazzi. "Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis." Proceedings of the ACM on Programming Languages 6, POPL (2022): 1–31. http://dx.doi.org/10.1145/3498721.

Full text
Abstract:
Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we
APA, Harvard, Vancouver, ISO, and other styles
2

Lesbre, Dorian, and Matthieu Lemerre. "Compiling with Abstract Interpretation." Proceedings of the ACM on Programming Languages 8, PLDI (2024): 368–93. http://dx.doi.org/10.1145/3656392.

Full text
Abstract:
Rewriting and static analyses are mutually beneficial techniques: program transformations change the intensional aspects of the program, and can thus improve analysis precision, while some efficient transformations are enabled by specific knowledge of some program invariants. Despite the strong interaction between these techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract interpreters into compilers, using a simple free algebra over the standard signature of abstract domains. Functor domains correspond to compiler passes, for which soundness
APA, Harvard, Vancouver, ISO, and other styles
3

MARIÑO, JULIO, ÁNGEL HERRANZ, and JUAN JOSÉ MORENO-NAVARRO. "Demand analysis with partial predicates." Theory and Practice of Logic Programming 7, no. 1-2 (2007): 153–82. http://dx.doi.org/10.1017/s1471068406002882.

Full text
Abstract:
AbstractTo alleviate the inefficiencies caused by the interaction of the logic and functional sides, integrated languages may take advantage of demand information, i.e. knowing in advance which computations are needed and, to which extent, in a particular context. This work studies demand analysis – which is closely related to backwards strictness analysis – in a semantic framework of partial predicates, which in turn are constructive realizations of ideals in a domain. This will allow us to give a concise, unified presentation of demand analysis, to relate it to other analyses based on abstra
APA, Harvard, Vancouver, ISO, and other styles
4

GARCÍA-CONTRERAS, ISABEL, JOSÉ F. MORALES, and MANUEL V. HERMENEGILDO. "Semantic code browsing." Theory and Practice of Logic Programming 16, no. 5-6 (2016): 721–37. http://dx.doi.org/10.1017/s1471068416000417.

Full text
Abstract:
AbstractProgrammers currently enjoy access to a very high number of code repositories and libraries of ever increasing size. The ensuing potential for reuse is however hampered by the fact that searching within all this code becomes an increasingly difficult task. Most code search engines are based on syntactic techniques such as signature matching or keyword extraction. However, these techniques are inaccurate (because they basically rely on documentation) and at the same time do not offer very expressive code query languages. We propose a novel approach that focuses on querying for semantic
APA, Harvard, Vancouver, ISO, and other styles
5

Bruni, Roberto, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. "A Correctness and Incorrectness Program Logic." Journal of the ACM, February 6, 2023. http://dx.doi.org/10.1145/3582267.

Full text
Abstract:
Abstract interpretation is a well known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness , which requires that no false alarms are produced only relatively to some fixed program inputs. Based on
APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic "Abstract Interpretation, Abstract Domain, Program Analysis, Partial Completeness"

1

Campion, Marco. "Partial (In)Completeness in Abstract Interpretation." Doctoral thesis, 2021. http://hdl.handle.net/11562/1049799.

Full text
Abstract:
In the abstract interpretation framework, completeness represents an optimal simulation by the abstract operators over the behavior of the concrete operators. This corresponds to an ideal (often rare) feature where there is no loss of information accumulated in abstract computations with respect to the properties encoded by the underlying abstract domains. In this thesis, we deal with the opposite notion of completeness in abstract interpretation, that is, incompleteness, applied to two different contexts: static program analysis and formal languages over the Chomsky's hierarchy. In static
APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Abstract Interpretation, Abstract Domain, Program Analysis, Partial Completeness"

1

Ascari, Flavio, Roberto Bruni, and Roberta Gori. "Logics for Extensional, Locally Complete Analysis via Domain Refinements." In Programming Languages and Systems. Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30044-8_1.

Full text
Abstract:
AbstractAbstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple $$\vdash _{A}[P]~\textsf{c}~[Q]$$ ⊢ A [ P ] c [ Q ] in the logic implies completen
APA, Harvard, Vancouver, ISO, and other styles
2

Jones, Neil D., and Flemming Nielson. "Abstract interpretation: a semantics-based tool for program analysis." In Handbook of Logic in Computer Science. Oxford University PressOxford, 1995. http://dx.doi.org/10.1093/oso/9780198537809.003.0005.

Full text
Abstract:
Abstract Desirable mathematical background for this chapter includes basic concepts such as lattices, complete partial orders, homomorphisms, etc.the elements of domain theory, e.g. as in the chapter by Abramsky in volume 3 of this Handbook, or the books [Schmidt, 1986] or [Nielson and Nielson, 1992a]. the elements of denotational semantics, e.g. as in the chapter by Tennent in volume 3 of this Handbook, or the books [Schmidt, 1986] or [Nielson and Nielson, 1992a]. Interpretations as used in logic. There will be some use of structural operational semantics [Kahn, 1987], [Plotkin, 1981], [Niels
APA, Harvard, Vancouver, ISO, and other styles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!