Transfer Function Synthesis without Quantifier Elimination

Traditionally, transfer functions have been designed manually for each operation in a program, instruction by instruction. In such a setting, a transfer function describes the semantics of a single instruction, detailing how a given abstract input state is mapped to an abstract output state. The net...

Full description

Bibliographic Details
Main Authors: Jörg Brauer, Andy King
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2012-09-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/814/pdf