%0 Generic %1 paige_02_using %A Paige, Richard F. %A Brooke, Phillip J. %D 2002 %K \_to\_review pvs refinement 2002 calculus \_pdf %T Using PVS to Support a Real-Time Refinement Calculus %U http://citeseer.ist.psu.edu/507963.html %X Hehner's theory of predicative programming is a general-purpose refinement calculus for producing correct sequential, concurrent, real-time, and communicating programs from specifications. However, only limited tool support exists for this theory. We give an overview of an ongoing project on how we are providing support for predicative programming via PVS, particularly for discharging the proof obligations that arise during algorithm refinement, and specifically, in the domain of real-time...

@misc{paige_02_using, abstract = {Hehner's theory of predicative programming is a general-purpose refinement calculus for producing correct sequential, concurrent, real-time, and communicating programs from specifications. However, only limited tool support exists for this theory. We give an overview of an ongoing project on how we are providing support for predicative programming via PVS, particularly for discharging the proof obligations that arise during algorithm refinement, and specifically, in the domain of real-time...}, added-at = {2009-03-10T04:53:19.000+0100}, author = {Paige, Richard F. and Brooke, Phillip J.}, biburl = {https://www.bibsonomy.org/bibtex/24cbcdf6b93c8007a02dac72989f30fd0/leonardo}, citeulike-article-id = {771671}, interhash = {d7d12ec40e44e4791f1920f269d32fb5}, intrahash = {4cbcdf6b93c8007a02dac72989f30fd0}, keywords = {\_to\_review pvs refinement 2002 calculus \_pdf}, posted-at = {2006-07-24 18:38:16}, priority = {4}, timestamp = {2009-03-10T04:53:19.000+0100}, title = {Using PVS to Support a Real-Time Refinement Calculus}, url = {http://citeseer.ist.psu.edu/507963.html}, year = 2002 }