This paper presents a verification framework that is parametric in a (trusted)
operational semantics of some programming language. The underlying proof system
is language-independent and consists of eight proof rules. The proof system is
proved partially correct and relatively complete (with respect to the
programming language configuration model). To show its practicality, the generic
framework is instantiated with a fragment of C and evaluated with encouraging
results.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
