Category Archives: Uncategorized

CCA 2024 Conference

This week, during my vacation, I attended the Twenty-First International Conference on Computability and Complexity in Analysis. It was held at Swansea in Wales, UK. There I presented joint work with Zvonko Iljazović and Lucija Validžić. The title of the presentation was Computability of One-point Metric Bases. The slides can be found here.

Some photos from Swansea, including the Bay Campus can be found below.

Slides

CCA_2024_Burnik_Iljazovic_Validzic

Computable Analysis Applied to Formal Verification of Cyber-Physical Systems

The following video I found online is about combining the theory of computable analysis with formal verification methods. I find this video very interesting because my diploma/master's thesis was about formal verification while my PhD study is from the area of computable analysis, so the work presented in this video nicely combines the two areas.

Title: "Computable Real Numbers and Why They Are Still Important Today"

Author: Edmund Clarke

Description: "Talk by ACM A.M. Turing Laureate Edmund Clarke during the ACM A.M. Turing Centenary Celebration, June, 2012. Abstract: Although every undergraduate in computer science learns about Turing Machines, it is not well known that they were originally proposed as a means of characterizing computable real numbers. For a long time, formal verification paid little attention to computational applications that involve the manipulation of continuous quantities, even though such applications are ubiquitous. In recent years, however, there has been great interest in safety-critical hybrid systems involving both discrete and continuous behaviors, including autonomous automotive and aerospace applications, medical devices of various sorts, control programs for electric power plants, and so on. As a result, the formal analysis of numerical computation can no longer be ignored. This talk focuses on one of the most successful verification techniques, temporal logic model checking. Current industrial model checkers do not scale to handle realistic hybrid systems. The key to handling more complex systems is to make better use of the theory of the computable reals, and computable analysis more generally. New formal methods for hybrid systems should combine existing discrete methods in model checking with new algorithms based on computable analysis. In particular, this talk discusses a model checker currently being developed along these lines."

Links