Project Details

CAQTUS - Computer-Aided Quantitative Synthesis

Project Period: 1. 1. 2020 - 31. 12. 2022

Project Type: grant

Code: GJ20-02328Y

Agency: Czech Science Foundation

Program: Juniorské granty

English title
CAQtuS: Computer-Aided Quantitative Synthesis

Quantitative formal methods; syntax-guided synthesis; program sketching; counter-examples; evolutionary optimisation; approximation techniques; decision procedures; system design automation; computational biochemical models; probabilistic programs


Computer-aided synthesis represents an emerging paradigm in design automation with many practical applications. The two main approaches to synthesis can be characterised as search-based and inductive techniques. The former use a procedure for generating candidate solutions followed by a verification procedure, and typically cannot guarantee the non-existence or optimality of a solution. The latter leverage an expensive decision procedure that directly constructs the desired solution or proves its non-existence.

This project will develop a new methodology that uniquely combines the two approaches within the framework of syntax-guided synthesis. It will focus on systems embracing uncertainty, stochasticity, or approximate computation, which all require quantitative reasoning. The proposed synthesis methods will be tailored to design automation in practically relevant engineering and biological applications. We believe that the combined approach will significantly improve the capabilities of synthesis methods and pave the way towards an automated correct-by-construction design process.

Team members
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT) , research leader
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT) , team leader
Mrázek Vojtěch, Ing., Ph.D. (UPSY FIT VUT) , team leader
Ambrožová Gabriela, Mgr., Ph.D. (UITS FIT VUT)
Andriushchenko Roman, Ing. (FIT VUT)
Andriushchenko Roman, Ing. (UITS FIT VUT)
Bíl Jan, Bc. (FIT VUT)
Frejlach Jakub, Bc. (FIT VUT)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Malásková Věra (UITS FIT VUT)
Martiček Štefan, Ing. (UITS FIT VUT)
Matyáš Jiří, Ing. (UITS FIT VUT)
Stupinský Šimon, Ing. (FIT VUT)




Back to top