Detail projektu

CAQtuS:Počítačem podporovaná kvantitativní syntéza

Období řešení: 01.01.2020 — 31.12.2022

Zdroje financování

Grantová agentura České republiky - Juniorské granty

- částečně financující (2020-01-01 - 2022-12-31)

O projektu

Počítačem podporovaná syntéza je nové paradigma v oblasti automatizace návrhu systémů s mnoha praktickými aplikacemi. V současnosti existují dva hlavní přístupy k syntéze: techniky založené na prohledávání stavového prostoru a induktivní techniky. Prvně zmíněný přístup postupně generuje kandidátní řešení, jejichž korektnost je následně verifikována. Tento přístup zpravidla není schopen dokázat neexistenci nebo optimálnost řešení. Induktivní techniky používají náročnou rozhodovací proceduru, která přímo zkonstruuje požadované řešení, nebo dokáže jeho neexistenci. Cílem tohoto projektu je vývoj nové metodiky, která unikátním způsobem kombinuje oba přístupy v rámci syntézy řízené syntaxí. Projekt je zaměřen na systémy mající pravděpodobnostní chování či zahrnující přibližné výpočty, a které tak vyžadují kvantitativní analýzu. Navržené metody budou přizpůsobeny problémům v oblasti vývoje relevantních inženýrských a biologických systémů. Věříme, že navržený kombinovaný přístup znatelně rozšíří možnosti současných metod pro automatizovaný vývoj komplexních systémů.

Popis anglicky
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.

Klíčová slova
Kvantitativní formální metody; syntakticky řízená syntéza; protipříklady; evoluční optimalizace; aproximační techniky; rozhodovací procedury; automatizace návrhů systémů; výpočetní biochemické modely; pravděpodobnostní programy

Klíčová slova anglicky
Quantitative formal methods; syntax-guided synthesis; program sketching; counter-examples; evolutionary optimisation; approximation techniques; decision procedures; system design automation; computational biochemical models; probabilistic programs

Označení

GJ20-02328Y

Originální jazyk

čeština

Řešitelé

Češka Milan, doc. RNDr., Ph.D. - hlavní řešitel

Útvary

Ústav inteligentních systémů
- příjemce (04.04.2019 - 31.12.2022)
Ústav počítačových systémů
- interní (04.04.2019 - 31.12.2022)

Výsledky

MARCHISIO, A.; MASSA, A.; MRÁZEK, V.; BUSSOLINO, B.; MARTINA, M.; SHAFIQUE, M. NASCaps: A Framework for Neural Architecture Search to Optimize the Accuracy and Hardware Efficiency of Convolutional Capsule Networks. In IEEE/ACM International Conference on Computer-Aided Design (ICCAD '20). Virtual Event: Association for Computing Machinery, 2020. p. 1-9. ISBN: 978-1-4503-8026-3.
Detail

ČEŠKA, M.; CHAU, C.; KŘETÍNSKÝ, J. SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. In International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer Verlag, 2020. p. 653-666. ISBN: 978-3-030-53287-1.
Detail

ČEŠKA, M.; MATYÁŠ, J.; MRÁZEK, V.; VOJNAR, T. Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits. In Theory and Applications of Satisfiability Testing - SAT 2020. Lecture Notes in Computer Science. Alghero: Springer International Publishing, 2020. p. 481-491. ISBN: 978-3-030-51824-0.
Detail

ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; KATOEN, J. Inductive Synthesis for Probabilistic Programs Reaches New Horizons. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021. p. 191-209. ISBN: 978-3-030-72015-5.
Detail

ANDRIUSHCHENKO, R.; ČEŠKA, M.; ABATE, A.; KWIATKOWSKA, M. Adaptive formal approximations of Markov chains. PERFORMANCE EVALUATION, 2021, vol. 148, no. 102207, p. 1-23. ISSN: 0166-5316.
Detail

ČEŠKA, M.; JUNGES, S.; KATOEN, J.; HENSE, C. Counterexample-guided inductive synthesis for probabilistic systems. Formal Aspects of Computing, 2021, vol. 33, no. 4, p. 637-667. ISSN: 0934-5043.
Detail

HELFRICH, M.; ČEŠKA, M.; KŘETÍNSKÝ, J.; MARTIČEK, Š. Abstraction-Based Segmental Simulation of Chemical Reaction Networks. In International Conference on Computational Methods in Systems Biology. Lecture Notes in Bioinformatics. Bucharest: Springer Verlag, 2022. p. 41-60. ISBN: 978-3-031-15033-3.
Detail

ČEŠKA, M.; MATYÁŠ, J.; MRÁZEK, V.; SEKANINA, L.; VAŠÍČEK, Z.; VOJNAR, T. SagTree: Towards Efficient Mutation in Evolutionary Circuit Approximation. Swarm and Evolutionary Computation, 2022, vol. 69, no. 100986, p. 1-10. ISSN: 2210-6502.
Detail

MRÁZEK, V. Optimization of BDD-based Approximation Error Metrics Calculations. In IEEE Computer Society Annual Symposium on VLSI (ISVLSI '22). Paphos: Institute of Electrical and Electronics Engineers, 2022. p. 86-91. ISBN: 978-1-6654-6605-9.
Detail

ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; KATOEN, J. Inductive Synthesis of Finite-State Controllers for POMDPs. In Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research. Eindhoven: Proceedings of Machine Learning Research, 2022. p. 85-95. ISSN: 2640-3498.
Detail

ČEŠKA, M.; MATYÁŠ, J.; MRÁZEK, V.; VOJNAR, T. Designing Approximate Arithmetic Circuits with Combined Error Constraints. In Proceeding of 25th Euromicro Conference on Digital System Design 2022 (DSD'22). Gran Canaria: Institute of Electrical and Electronics Engineers, 2022. p. 785-792. ISBN: 978-1-6654-7404-7.
Detail

ANDRIUSHCHENKO, R.; ČEŠKA, M.; MARCIN, V.; VOJNAR, T. GPU-Accelerated Synthesis of Probabilistic Programs. In International Conference on Computer Aided Systems Theory (EUROCAST'22). Lecture Notes in Computer Science. Cham: 2022. p. 256-266. ISBN: 978-3-031-25312-6.
Detail

ANDRIUSHCHENKO, R.; ČEŠKA, M.; STUPINSKÝ, Š.; JUNGES, S.; KATOEN, J. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science. Cham: Springer Verlag, 2021. p. 856-869. ISBN: 978-3-030-81684-1.
Detail

Odpovědnost: Češka Milan, doc. RNDr., Ph.D.