Methods
and Models for Concurrent Processing of Messages. M.Sc. Thesis,
Technical University - Sofia, Sofia, Bulgaria, 1995 (in Bulgarian). Regression
Test Selection Using Rough Sets. In Proceedings of the
International Conference “Applications of Computer Systems’97”,
Szczecin, Poland, 1997. (PS) Software
Test Generation Using Refinement Types. Technical Report P13/99,
Department of Informatics, Wroclaw Polytechnic, Wroclaw, Poland,
1999. (PS) -
Software
Test Generation Using Refinement Types. In
Automated Software Engineering’99 Proc., Cocoa Beach,
FL, USA, 1999. (IEEEXplore link) Software
Test Generation Using Program Skeletons. PhD Thesis. Technical
Report PRE 23/01, Department of Informatics, Wroclaw Polytechnic,
Wroclaw, Poland, 2001. (ZIP with PS of corrected version, slides, LaTeX sources, Haskell prototype) (bibl. info.) - A Simple Supercompiler Formally Verified in Coq. Draft, accepted to META-2010, 2010. (ZIP with PDF, TeX; slides; Coq archive)
- A Metacomputation Toolkit for a Subset of F# and Its Application To Software Testing. Draft, submitted to META-2012, 2012. (PDF; accompanying F# source archive)
- Towards a Framework for Building Formally Verified Supercompilers in Coq. Draft, submitted to TFP 2012, 2012 (PDF; corresponding Coq sources; they require a Coq library for almost-full relations, which can be found on the home page of Dimitrios Vytiniotis )
|
|