TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures

Marc Brockschmidt and Andrey Rybalchenko

Abstract

A program with procedures can be formally modelled by a set of transition relations that form a pushdown system. These transition relations keep track how valuations of variables in scope of individual procedures evolve during program execution. We present such a model together with its representation using the SMTLIB2 language.

Details

Publication typeOther
> Publications > TermComp Proposal: Pushdown Systems as a Model for Programs with Procedures