Project Details

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
Type
grant
Keywords

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

Abstract

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. (DITS) – research leader
Ambrožová Gabriela, Mgr., Ph.D.
Andriushchenko Roman, Ing. (DITS)
Bíl Jan, Ing.
Frejlach Jakub, Ing.
Havlena Vojtěch, Ing., Ph.D. (DITS)
Malásková Věra (DITS)
Martiček Štefan, Ing.
Matyáš Jiří, Ing., Ph.D. (RG VERIFIT)
Stupinský Šimon, Ing.
Publication Results

2024

2022

2021

2020

Back to top