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
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.
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.
2024
- HELFRICH, M.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; KŘETÍNSKÝ, J.; MARTIČEK, Š.; ŠAFRÁNEK, D. Abstraction-based segmental simulation of reaction networks using adaptive memoization. BMC BIOINFORMATICS, 2024, vol. 25, no. 1,
p. 1-24. ISSN: 1471-2105. Detail
2022
- 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. Proceedings of Machine Learning Research. Eindhoven: Proceedings of Machine Learning Research, 2022. no. 180,
p. 85-95. ISSN: 2640-3498. 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: Springer Nature Switzerland AG, 2022.
p. 256-266. ISBN: 978-3-031-25312-6. 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 - Č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 - 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 - 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
2021
- 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 - 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.; 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 - Č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
2020
- Č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 - 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