CAQTUS - Computer-Aided Quantitative Synthesis

Název anglicky

CAQtuS: Computer-Aided Quantitative Synthesis

Typ

grant

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

Abstrakt

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ů.

Řešitelé

Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Mrázek Vojtěch, Ing., Ph.D. (UPSY FIT VUT) , spoluřešitel
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, Ing. (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)

Publikace

2022

HELFRICH Martin, ČEŠKA Milan, KŘETÍNSKÝ Jan a MARTIČEK Štefan. 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, s. 41-60. ISBN 978-3-031-15033-3. Detail
ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch a VOJNAR Tomáš. 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, s. 785-792. ISBN 978-1-6654-7404-7. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, MARCIN Vladimír a VOJNAR Tomáš. GPU-Accelerated Synthesis of Probabilistic Programs. In: International Conference on Computer Aided Systems Theory (EUROCAST'22). Lecture Notes in Computer Science. Cham, 2022, s. 256-266. ISBN 978-3-031-25312-6. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian a KATOEN Joost-Pieter. Inductive Synthesis of Finite-State Controllers for POMDPs. In: Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research, roč. 180. Eindhoven: Proceedings of Machine Learning Research, 2022, s. 85-95. ISSN 2640-3498. Detail
MRÁZEK Vojtěch. 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, s. 86-91. ISBN 978-1-6654-6605-9. Detail
ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch, SEKANINA Lukáš, VAŠÍČEK Zdeněk a VOJNAR Tomáš. SagTree: Towards Efficient Mutation in Evolutionary Circuit Approximation. Swarm and Evolutionary Computation, roč. 69, č. 100986, 2022, s. 1-10. ISSN 2210-6502. Detail

2021

ABATE Alessandro, ANDRIUSHCHENKO Roman, ČEŠKA Milan a KWIATKOWSKA Marta. Adaptive formal approximations of Markov chains. Performance Evaluation, roč. 148, č. 102207, 2021, s. 1-23. ISSN 0166-5316. Detail
ČEŠKA Milan, HENSE Christian, JUNGES Sebastian a KATOEN Joost-Pieter. Counterexample-guided inductive synthesis for probabilistic systems. Formal Aspects of Computing, roč. 33, č. 4, 2021, s. 637-667. ISSN 0934-5043. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian a KATOEN Joost-Pieter. Inductive Synthesis for Probabilistic Programs Reaches New Horizons. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021, s. 191-209. ISBN 978-3-030-72015-5. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter a STUPINSKÝ Šimon. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In: International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, roč. 12759. Cham: Springer Verlag, 2021, s. 856-869. ISBN 978-3-030-81684-1. Detail

2020

MARCHISIO Alberto, MASSA Andrea, MRÁZEK Vojtěch, BUSSOLINO Beatrice, MARTINA Mauricio a SHAFIQUE Muhammad. 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, s. 1-9. ISBN 978-1-4503-8026-3. Detail
ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch a VOJNAR Tomáš. Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits. In: Theory and Applications of Satisfiability Testing - SAT 2020. Lecture Notes in Computer Science, roč. 12178. Alghero: Springer International Publishing, 2020, s. 481-491. ISBN 978-3-030-51824-0. Detail
ČEŠKA Milan, CHAU Calvin a KŘETÍNSKÝ Jan. SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. In: International Conference on Computer Aided Verification. Lecture Notes in Computer Science, roč. 12224. Cham: Springer Verlag, 2020, s. 653-666. ISBN 978-3-030-53287-1. Detail