Re: symbolic interpretation

Basile STARYNKEVITCH <basile.starynkevitch@cea.fr>
19 Jan 2001 23:16:02 -0500

          From comp.compilers

Related articles
symbolic interpretation bettini@dsi.unifi.it (Lorenzo Bettini) (2001-01-11)
Re: symbolic interpretation fjh@cs.mu.OZ.AU (2001-01-18)
Re: symbolic interpretation idbaxter@semdesigns.com (Ira D. Baxter) (2001-01-18)
Re: symbolic interpretation scarroll@csrd.uiuc.edu (Steven Carroll) (2001-01-18)
Re: symbolic interpretation basile.starynkevitch@cea.fr (Basile STARYNKEVITCH) (2001-01-19)
Re: symbolic interpretation fjh@cs.mu.OZ.AU (2001-01-26)
| List of all articles for this month |

From: Basile STARYNKEVITCH <basile.starynkevitch@cea.fr>
Newsgroups: comp.compilers
Date: 19 Jan 2001 23:16:02 -0500
Organization: Commissariat a l'Energie Atomique - France
References: 01-01-072 01-01-079
Keywords: optimize
Posted-Date: 19 Jan 2001 23:16:02 EST

>>>>> "Fergus" == Fergus Henderson <fjh@cs.mu.OZ.AU> writes:


        Fergus> Lorenzo Bettini <bettini@dsi.unifi.it> writes:
        >> Do you have any pointer and/or reference to symbolic
        >> interpretation in compiler writing, please? I would need a
        >> specific one, not just a generic one.


        Fergus> I think "symbolic interpretation" is more commonly called
        Fergus> "abstract interpretation". (Or is there some difference
        Fergus> in these terms that I'm unaware of?)


Abstract interpretation is a kind of static code analysis. In very
primitive terms, it means executing the program with abstract values
(for instance instead of executing a program on concrete numbers, you
execute it on intervals, or other kind of lattices, etc...). The
result is some crude approximation of the execution. Abstract
interpretation is some kind of interpretation of the program with
approximate set of values. (with some more technical tricks, widening,
narrowing, etc...)


Symbolic interpretation (or symbolic execution) is another kind of
static code analysis. In naive terms, you execute the program with
some properties (eg 1st order logic predicates) attached at most
control points. Symbolic interpretation is more like automatic theorem
proving related to programs.


Regards.


---------------------------------------------------------------------
Basile STARYNKEVITCH ---- Commissariat l Energie Atomique
DTA/LETI/DEIN/SLA * CEA/Saclay b.528 (p111f) * 91191 GIF/YVETTE CEDEX * France
phone: 1,69.08.60.55; fax: 1.69.08.83.95 home: 1,46.65.45.53
email: Basile point Starynkevitch at cea point fr
web perso: http://perso.wanadoo.fr/starynkevitch/basile/


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.