Carlo A. Furia

I'm an associate professor in the Formal Methods Division (part of Software Technology) of the Department of Computer Science and Engineering of Chalmers University of Technology. My research interests center around developing rigorous techniques and tools to analyze and improve the quality, correctness, and reliability of software and systems.

The paper Triggerless Happy — Intermediate Verification with a First-Order Prover won the best paper award at iFM 2017!
Contract-Based Program Repair Without the Contracts accepted for ASE 2017!
A Fully Verified Container Library to appear in the FAOC journal!
Triggerless Happy — Intermediate Verification with a First-Order Prover accepted for iFM 2017!
I've been invited to present a poster on my work on Bayesian data analysis in the ICSE 2017 poster session!
Bounded Variability of Metric Temporal Logic to appear in the AMAI journal!

About me

I have a PhD in Computer Science from the Politecnico di Milano, a Master of Science in Computer Science from the University of Illinois at Chicago, and a Laurea degree in Computer Science and Engineering also from the Politecnico di Milano. Before coming to Chalmers, I spent about seven years as senior researcher at ETH Zurich in the remarkable Chair of Software Engineering (don't look for it; it's not there anymore).


Most of my research is in the area of formal methods for software engineering. These include a wide array of models, techniques, methods, and tools to support the analysis, rigorous development, and verification of software and software-intensive systems. Much of my work aims at making formal methods practical and more widely applicable—for example by increasing the level of automation. It often features combinations of diverse techniques to improve versatility and reduce limitations; and thorough empirical evaluations to assess relevance and impact of research outcomes.

The domains where I made major contributions include: practical techniques and tools to analyze, reason about, and improve software equipped with simple elements of functional specification such as assertions; and models and techniques to rigorously describe and reason about the behavior of systems, such as real-time, hybrid, and cyber-physical systems.

Try out some of our verification tools online on Comcom!

I wrote a book on modeling and analyzing real-time and hybrid systems; it's available online from Springer. Modeling time in computing: book cover


The latest courses I've been teaching:

The teaching page has a longer list including older courses.

If you're a student looking for a project or thesis topic, check out these student projects, as well as my research page; feel free to drop me a line if you find something that interests you or simply want to discuss possible topics.


Scientific events, such as conferences, I'm currently involved in organizing:

The events page has a longer list including past events.

The talks page lists events I've attended, often participating by giving a talk.