23

I am not aware of a paper concerned with the comparison between symbolic execution and abstract interpretation. Nor do I think one is needed. Reading the original descriptions of these two techniques should be enough. King, Symbolic Execution and Program Testing, 1976 Cousot, Cousot, Abstract Interpretation: a Unified Lattice Model for Static Analysis of ...


17

Abstract interpretation is a very general concept and depending on whom you ask, you will receive different explanations because versatile concepts admit multiple perspectives. The view in this answer is mine and I would not assume it is general. Computational hardness as a motivation Let's start with decision problems, whose solutions have a structure ...


9

There's a very recent survey paper available on Alias Analysis for Object-Oriented Programs. It will be published in April in the LNCS state-of-the-art volume (gratuitous advertising alert): Aliasing in Object-Oriented Programming: Types, Analysis and Verification. Lecture Notes in Computer Science, Vol. 7850. Dave Clarke, Tobias Wrigstad, James Noble (Eds....


8

Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more practical-minded offshoot of this research is RAML (Resource Aware ML), a functional programming language with a type system that will give you precise ...


7

The COSTA tool developed by the COSTA research group does exactly what you want. Given a program (in Java bytecode format), the tool produces a cost equation based on a cost model provided by the programmer. The cost model can involve entities such as runtime, memory usage, or billable events (such as sending text messages). The runtime equation is then ...


7

You need to identify the lattices involved in each case. Let $(\wp(S),\subseteq)$ be the lattice of all subsets of a set $S$ ordered by subset inclusion. A function $f:\wp(S) \to \wp(S)$ is monotone if for every pair of sets $x$ and $y$, if $x \subseteq y$ it also holds that $f(x) \subseteq f(y)$. The definition applies more generally to functions $f: L \...


7

I agree that it's often hard to extract the main point from all those details. (In fact, my big issue with every treatment of abstract interpretation I've seen is that they present so much machinery without motivating it.) Here's how I think of it: Abstract interpretation is running programs, approximately, on large sets of inputs all at once. This doesn'...


5

I think this is meant in a very shallow sense. The first step of abstract interpretation is to identify a concrete collecting semantics. Rather than describe the evolution of a single state, collecting semantics describes the evolution of sets of states. Since symbolic execution reasons about the representations of sets of states, one can argue that it ...


5

Forward SE is easier to implement, composes better with other testing methods, and thus is more scalable. Usually, on industrial-scale workloads, it's not possible to enumerate all paths in the program under test -- there are simply too many paths. So we need some way to deal with this and sample only a subset of paths, while still having a reasonable ...


4

Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/wiki/Microsoft_Terminator . The newest version of this system is at https://mmjb.github.io/T2/ .


2

As such, your problem seems to be NP-complete. To see the membership in NP, you can first guess a path, and then check that this path ends with $V_q$ and is valid. For the hardness part, we can directly reduce from the Boolean satisfiability problem (SAT), which itself is NP-hard. The problem SAT takes as input a formula in conjunctive normal form (CNF), and ...


2

I don't know about a method for analyzing an arbitrary given algorithm to come up with a cache policy in general (this sounds quite hard), but this is essentially what's been done (optimally, in an asymptotic sense) on a case-by-case basis for most known cache-oblivious algorithms, by analyzing their divide-and-conquer structure. Cache-oblivious algorithms ...


2

This new version of the answer tries to take into account the changes in the question, and the information exchanged in the comments. This answer assumes that $S$ should be the set of variables that have a content that is used in some defined fragment of the program, rather than, at some point in the program, the variables with a content that will be ...


2

I actually thought about the same question a while ago. Here is the train of thought I had: As you said the halting problem is an issue. To avoid this we need a language which only allows programs that always halt. On the other hand our language needs to be expressive enough to deal with most common problems(e.g. it should at least capture all of the ...


2

See Patrick Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes (Iterative methods for construction and approximation of fixpoints of monotone operators on lattices, program static analysis). Thèse ès Sciences Mathématiques, Université Joseph Fourier, ...


2

I cannot see the article and have to guess. The text makes clear that they are using the symbol $\supset$ as notation for implication. So you could read it as In order to prove that a program $P$ possesses a property $R$, one has only to prove the implication $W(P) \implies R$. See the Wikipedia page on material implication for other notation for ...


Only top voted, non community-wiki answers of a minimum length are eligible