- 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. accepted to META-2012, 2012. (PDF; accompanying F# source archive; slides)
- Towards a Framework for Building Formally Verified Supercompilers in Coq. In Post-proceedings of TFP 2012, LNCS 7829, 2013, pp 133-148 (PDF; corresponding Coq sources; they require a Coq library for almost-full relations, which can be found on the home page of Dimitrios Vytiniotis). The original publication is available at link.springer.com.
- An Approach for Modular Verification of Multi-result Supercompilers. Draft, accepted to META-2014, 2014. (PDF; Coq source; slides)