Robustness and correctness are certainly desirable properties of a piece of software. So is performance. Certain mainstream approaches to robustness, such as dynamic checks, have negative performance effects, which may create the impression that robustness or correstness is fundamentally at odds with performance. But is it really the case?
Read more...TL;DR: Debugging (using a debugger) is painful, unnecessary, and a sign of a poor design.
Read more...In February 1991, a Patriot missile defence system failed to track and neutralise a missile heading towards US Army barracks, resulting in death of 28 people. The report issued by the US General Accounting Office a year later blamed a software error. The growing dependence of our society on software that directly acts on the physical environment (including software in vehicles used for both civilian and military purposes) leads to the question: How do we make safety-critical software more reliable? In this post I discuss an approach to incremental construction of such software, based on a technique known as “refinement”.
Read more...In Minuska, one can describe the semantics of a programming language using term rewriting. As term rewriting is quite low-level and expressing common patterns is repetitive, Minuska, inspired by the K-framework, implements some shortcuts (“syntactic sugar”) whose meaning is defined only by their translation to term rewriting rules. This post motivates the need for and presents a design of a higher-level language-description language that I plan to implement into Minuska.
Read more...I am weighting my options on future research directions.
Read more...Here a present an idea for a simple tool for information flow control. As usually, the idea is language-parametric.
Read more...There is one aspect of the Minuska framework which provides a language designer a great flexibility. Namely, a programming language configuration is a tree whose leaves hold values from an arbitrary domain (typically integers, lists, etc); it is up to the language designer to choose a suitable domain. This makes writing language-parametric tools in Minuska even harder. In this post I explore some arguments for supporting domain-parametricity anyway, discuss the associated problems, and sketch out a possible solution.
Read more...In order to be useful, data stored in computer need to represent real-world phenomena. However, making the representation go through an extra level of indirection – through the realm of mathematics – can be benefitial.
Read more...Debugging is costly. Theorem proving is costly. Debugging by attempting to prove a property that does not hold and then wondering about why it can’t be proven - you do not want to do that. How do I know? I have tried that too many times.
Read more...As my PhD defence is approaching, I am reflecting on why I got into that research area - the area of formal methods for software engineering. Unlike for many of my research peers, it was not an innate interest in theory or mathematics that got me there; rather, my motivation was practical. The journey began when I got my first software engineering job (back in 2013), and was started by a question: “How can I write software better?”. The tentative answer was, and still is: “By having better tools”.
Read more...