CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Interleaving Symbolic Execution and Partial Evaluation

Richard Bubel (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Reiner Hähnle (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Ran Ji (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. 8th International Symposium on Formal Methods for Components and Objects, FMCO 2009, Eindhoven, 4-6 November 2009 (0302-9743). Vol. 6286 (2010), p. 125-146.
[Konferensbidrag, refereegranskat]

Partial evaluation is a program specialization technique that allows to optimize programs for which partial input is known. We show that partial evaluation can be used with advantage to speed up as well symbolic execution of programs. Interestingly, the input required for partial evaluation comes from symbolic execution itself which makes it natural to interleave partial evaluation and symbolic execution steps in a software verification setup.



Denna post skapades 2010-10-27. Senast ändrad 2016-07-26.
CPL Pubid: 128191

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Datalogi
Programvaruteknik

Chalmers infrastruktur