[图书][B] Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino
Long gone are the days when program veri? cation was a task carried out merely by hand
with paper and pen. For one, we are increasingly interested in proving actual program …
with paper and pen. For one, we are increasingly interested in proving actual program …
A program logic for resources
We introduce a reasoning infrastructure for proving statements about resource consumption
in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a …
in a fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a …
A compositional natural semantics and Hoare logic for low-level languages
The advent of proof-carrying code has generated significant interest in reasoning about low-
level languages. It is widely believed that low-level languages with jumps must be difficult to …
level languages. It is widely believed that low-level languages with jumps must be difficult to …
Automated compositional proofs for real-time systems
CA Furia, M Rossi, D Mandrioli, A Morzenti - Theoretical computer science, 2007 - Elsevier
We present a framework for formally proving that the composition of the behaviors of the
different parts of a complex, real-time system ensures a desired global specification of the …
different parts of a complex, real-time system ensures a desired global specification of the …
Verification conditions are code
AM Gravell - Acta informatica, 2007 - Springer
This paper presents a new theoretical result concerning Hoare Logic. It is shown here that
the verification conditions that support a Hoare Logic program derivation are themselves …
the verification conditions that support a Hoare Logic program derivation are themselves …