PhD defense of Josef Kufner

The dissertation thesis defense of Ing. Josef Kufner takes place semi-distantly on November 30 from 14:00 in the room KN:E 205 and also via MS Teams. Josef will be defending his dissertation thesis "Specifications for Intelligent Software Synthesis" supervised by Ing. Radek Mařík, CSc. In case you want to watch the exam online, do so on the FEE CTU YouTube channel.


To relieve programmers of repetitive and tiring work on simple, yet too diverse, entities in web applications, this thesis searches for an assistive framework, where machines aid the programmers with implementing such entities. The first question to answer is how to tell the computer what we want without specifying all the details; otherwise, we could just implement the application instead. The second question is how to effectively reason about the software so that we can analyze what we have and infer what we miss. The proposed solution introduces Smalldb state machines as a formal model that describes the behavior of the entities in a web application. Such a model is not designed to cover every aspect of the application; instead, it leaves well-defined gaps for the details that are impractical to specify formally. The formal model then becomes part of the application architecture and run-time, where it provides a secure API between business logic and presentation layer; moreover, it verifies that the implementation corresponds to the model. To answer the first question, we return to the very beginning of the software development process, where we identify software specifications that programmers already use and discuss whether such specifications are sufficiently machine-friendly for automated processing. The identified BPMN business process diagrams become an input for a novel STS algorithm — a software architect draws how users will use a web application, and the STS algorithm infers the implementation in the form of a Smalldb state machine. The thesis concludes with presenting a Cascade, a machine-friendly approach to software composition based on the utilization of the formal models.