arXiv subjects

Dimitur Nikolaev Krustev

Publications and source records attributed to Dimitur Nikolaev Krustev.

2 recordsLinked to original sources

arXiv2020

Optimizing Program Size Using Multi-result Supercompilation

Supercompilation is a powerful program transformation technique with numerous interesting applications. Existing methods of supercompilation, however, are often very unpredictable with respect to the size of the resulting programs. We consider an approach for controlling result size, based on a combination of multi-result supercompilation and a specific generalization strategy, which avoids code duplication. The current early experiments with this method show promising results - we can keep the size of the result small, while still performing powerful optimizations.

cs.PL↗

arXiv2020

Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract)

While the use of formal verification techniques is well established in the development of mission-critical software, it is still rare in the production of most other kinds of software. We share our experience that a formal verification tool such as Coq can be very useful and practical in the context of off-the-shelf software development -- CAD in particular -- at least in some occasions. The emphasis is on 3 main areas: factors that can enable the use of Coq in an industrial context; some typical examples of tasks, where Coq can offer an advantage; examples of issues to overcome - and some non-issues - when integrating Coq in a standard development process.

cs.PL↗