TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard ...
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
Traditional security protocols are mainly concerned with key establishment and principal authentication and rely on predistributed keys and properties of cryptographic operators. I...
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
ion and equality to base types but retains lambda abstractions and higher-order variables. We show that this fragment enjoys the characteristic properties of first-order logic: co...
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
VCC is an industrial-strength verification environment for low-level concurrent system code written in C. VCC takes a program (annotated with function contracts, state assertions,...
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
Optical systems are becoming increasingly important as they tend to resolve many bottlenecks in the present age communications and electronics. Some common examples include their u...
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
TPHOL
2009
IEEE
14 years 4 months ago
2009
IEEE
We present four coinductive operational semantics for the While language accounting for both terminating and non-terminating program runs: big-step and small-step relational semant...