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
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. (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, Ing. (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)
Publications

2024

  • HELFRICH Martin, ANDRIUSHCHENKO Roman, ČEŠKA Milan, KŘETÍNSKÝ Jan, MARTIČEK Štefan and ŠAFRÁNEK David. Abstraction-based segmental simulation of reaction networks using adaptive memoization. BMC Bioinformatics, vol. 25, no. 1, 2024, pp. 1-24. ISSN 1471-2105. Detail

2022

  • HELFRICH Martin, ČEŠKA Milan, KŘETÍNSKÝ Jan and 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, pp. 41-60. ISBN 978-3-031-15033-3. Detail
  • ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch and 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, pp. 785-792. ISBN 978-1-6654-7404-7. Detail
  • ANDRIUSHCHENKO Roman, ČEŠKA Milan, MARCIN Vladimír and 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, pp. 256-266. ISBN 978-3-031-25312-6. Detail
  • ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian and KATOEN Joost-Pieter. Inductive Synthesis of Finite-State Controllers for POMDPs. In: Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research, vol. 180. Eindhoven: Proceedings of Machine Learning Research, 2022, pp. 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, pp. 86-91. ISBN 978-1-6654-6605-9. Detail
  • ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch, SEKANINA Lukáš, VAŠÍČEK Zdeněk and VOJNAR Tomáš. SagTree: Towards Efficient Mutation in Evolutionary Circuit Approximation. Swarm and Evolutionary Computation, vol. 69, no. 100986, 2022, pp. 1-10. ISSN 2210-6502. Detail

2021

  • ABATE Alessandro, ANDRIUSHCHENKO Roman, ČEŠKA Milan and KWIATKOWSKA Marta. Adaptive formal approximations of Markov chains. Performance Evaluation, vol. 148, no. 102207, 2021, pp. 1-23. ISSN 0166-5316. Detail
  • ČEŠKA Milan, HENSE Christian, JUNGES Sebastian and KATOEN Joost-Pieter. Counterexample-guided inductive synthesis for probabilistic systems. Formal Aspects of Computing, vol. 33, no. 4, 2021, pp. 637-667. ISSN 0934-5043. Detail
  • ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian and 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, pp. 191-209. ISBN 978-3-030-72015-5. Detail
  • ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter and STUPINSKÝ Šimon. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In: International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 12759. Cham: Springer Verlag, 2021, pp. 856-869. ISBN 978-3-030-81684-1. Detail

2020

  • MARCHISIO Alberto, MASSA Andrea, MRÁZEK Vojtěch, BUSSOLINO Beatrice, MARTINA Mauricio and 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, pp. 1-9. ISBN 978-1-4503-8026-3. Detail
  • ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch and 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, vol. 12178. Alghero: Springer International Publishing, 2020, pp. 481-491. ISBN 978-3-030-51824-0. Detail
  • ČEŠKA Milan, CHAU Calvin and 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, vol. 12224. Cham: Springer Verlag, 2020, pp. 653-666. ISBN 978-3-030-53287-1. Detail
Back to top