[PRL] An Exercise in Invariant-based Programming with Interactive and Automatic Th...

[Mitch]

fwiw...

Sent to you by Mitch via Google Reader: An Exercise in Invariant-based
Programming with Interactive and Automatic Theorem Prover Support.
(arXiv:1202.4829v1 [cs.LO]) via cs.PL updates on arXiv.org by
Ralph-Johan Back (Åbo Akademi University), Johannes Eriksson (Åbo
Akademi University) on 2/22/12

Invariant-Based Programming (IBP) is a diagram-based
correct-by-construction programming methodology in which the program is
structured around the invariants, which are additionally formulated
before the actual code. Socos is a program construction and
verification environment built specifically to support IBP. The
front-end to Socos is a graphical diagram editor, allowing the
programmer to construct invariant-based programs and check their
correctness. The back-end component of Socos, the program checker,
computes the verification conditions of the program and tries to prove
them automatically. It uses the theorem prover PVS and the SMT solver
Yices to discharge as many of the verification conditions as possible
without user interaction. In this paper, we first describe the Socos
environment from a user and systems level perspective; we then
exemplify the IBP workflow by building a verified implementation of
heapsort in Socos. The case study highlights the role of both automatic
and interactive theorem proving in three sequential stages of the IBP
workflow: developing the background theory, formulating the program
specification and invariants, and proving the correctness of the final
implementation.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed