Sciweavers

ECEASST
2006

ENFORCe: A System for Ensuring Formal Correctness of High-level Programs

13 years 3 months ago
ENFORCe: A System for Ensuring Formal Correctness of High-level Programs
Graph programs allow a visual description of programs on graphs and graph-like structures. The correctness of a graph program with respect to a pre- and a postcondition can be shown in a classical way by constructing a weakest precondition of the program relative to the postcondition and checking whether the precondition implies the weakest precondition. ENFORCe is a currently developed system for ensuring formal correctness of graph programs and, more general, high-level programs by computing weakest preconditions of these programs. In this paper, we outline the features of the system and present its software framework.
Karl Azab, Annegret Habel, Karl-Heinz Pennemann, C
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ECEASST
Authors Karl Azab, Annegret Habel, Karl-Heinz Pennemann, Christian Zuckschwerdt
Comments (0)