Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
113
3. A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, “Combinatorial
Sketching for Finite Programs,” ACM Sigplan Notices, vol. 41, no. 11, pp. 404–415,
2006.
4. C. David and D. Kroening, “Program Synthesis: Challenges and Opportunities,”
Phil. Trans. R. Soc. A, vol. 375, no. 2104, p. 20150403, 2017.
5. A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, E. Polgreen,
and D. Kroening, “Automated formal synthesis of digital controllers for state-space
physical plants,” in Proceedings of CAV, LNCS 10426, 2017, pp. 462–482.
6. A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening,
and E. Polgreen, “Automated formal synthesis of provably safe digital controllers
for continuous plants,” Acta Informatica, 2020.
7. H. Ravanbakhsh and S. Sankaranarayanan, “Counter-example guided synthesis of
control lyapunov functions for switched systems,” in IEEE Control and Decision
Conference (CDC), 2015, pp. 4232–4239.
8. ——, “Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework,” in ACM/IEEE Conference on Embedded Software (EMSOFT), 2016, pp. 8:1–8:10.
9. D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of
View, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer
Berlin Heidelberg, 2016.
10. Gurobi Optimization, LLC, “Gurobi Optimizer Reference Manual,” 2018. [Online].
Available: http://www.gurobi.com
11. L. De Moura and N. Bjørner, “Z3: An Efficient SMT solver,” in International
conference on Tools and Algorithms for the Construction and Analysis of Systems.
Springer, 2008, pp. 337–340.
12. R. Kalman and J. Bertram, “Control System Analysis and Design via the “Second
Method” of Lyapunov: Part I Continuous-time Systems,” Trans. AMSE Series D
J. Basic Eng., vol. 82, no. 2, pp. 371–393, 1960.
13. N. N. Krasovskii, Stability of Motion: Applications of Lyapunov’s Second Method
to Differential Systems and Equations With Delay. Stanford Univ. Press, 1963.
14. J. LaSalle and S. Lefschetz, Stability by Liapunov’s Direct Method With Applications. Academic Press, 1961.
15. V. I. Zubov, Methods of A. M. Lyapunov and Their Application. Noordhoff, 1964.
16. R. Brayton and C. Tong, “Stability of Dynamical Systems: A Constructive Approach,” IEEE Transactions on Circuits and Systems, vol. 26, no. 4, pp. 224–234,
1979.
17. P. A. Parrilo, “Structured Semidefinite Programs and Semialgebraic Geometry
Methods in Robustness and Optimization,” Ph.D. dissertation, California Institute
of Technology, 2000.
18. A. Papachristodoulou and S. Prajna, “On the Construction of Lyapunov Functions using the Sum of Squares Decomposition,” in Proceedings of the 41st IEEE
Conference on Decision and Control, 2002., vol. 3. IEEE, 2002, pp. 3482–3487.
19. S. Prajna, A. Papachristodoulou, and P. A. Parrilo, “SOSTOOLS: Sum of squares
Optimization Toolbox for MATLAB–User’s Guide,” Control and Dynamical Systems, California Institute of Technology, Pasadena, CA, vol. 91125, 2004.
20. A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo, “SOSTOOLS Version 3.03. Sum of Squares Optimization Toolbox for MATLAB,” 2018.
21. R. Geiselhart, R. H. Gielen, M. Lazar, and F. R. Wirth, “An Alternative Converse
Lyapunov Theorem for Discrete-time Systems,” Syst. Control Lett., vol. 70, pp.
49–59, 2014.
113
3. A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, “Combinatorial
Sketching for Finite Programs,” ACM Sigplan Notices, vol. 41, no. 11, pp. 404–415,
2006.
4. C. David and D. Kroening, “Program Synthesis: Challenges and Opportunities,”
Phil. Trans. R. Soc. A, vol. 375, no. 2104, p. 20150403, 2017.
5. A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, E. Polgreen,
and D. Kroening, “Automated formal synthesis of digital controllers for state-space
physical plants,” in Proceedings of CAV, LNCS 10426, 2017, pp. 462–482.
6. A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening,
and E. Polgreen, “Automated formal synthesis of provably safe digital controllers
for continuous plants,” Acta Informatica, 2020.
7. H. Ravanbakhsh and S. Sankaranarayanan, “Counter-example guided synthesis of
control lyapunov functions for switched systems,” in IEEE Control and Decision
Conference (CDC), 2015, pp. 4232–4239.
8. ——, “Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework,” in ACM/IEEE Conference on Embedded Software (EMSOFT), 2016, pp. 8:1–8:10.
9. D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of
View, ser. Texts in Theoretical Computer Science. An EATCS Series. Springer
Berlin Heidelberg, 2016.
10. Gurobi Optimization, LLC, “Gurobi Optimizer Reference Manual,” 2018. [Online].
Available: http://www.gurobi.com
11. L. De Moura and N. Bjørner, “Z3: An Efficient SMT solver,” in International
conference on Tools and Algorithms for the Construction and Analysis of Systems.
Springer, 2008, pp. 337–340.
12. R. Kalman and J. Bertram, “Control System Analysis and Design via the “Second
Method” of Lyapunov: Part I Continuous-time Systems,” Trans. AMSE Series D
J. Basic Eng., vol. 82, no. 2, pp. 371–393, 1960.
13. N. N. Krasovskii, Stability of Motion: Applications of Lyapunov’s Second Method
to Differential Systems and Equations With Delay. Stanford Univ. Press, 1963.
14. J. LaSalle and S. Lefschetz, Stability by Liapunov’s Direct Method With Applications. Academic Press, 1961.
15. V. I. Zubov, Methods of A. M. Lyapunov and Their Application. Noordhoff, 1964.
16. R. Brayton and C. Tong, “Stability of Dynamical Systems: A Constructive Approach,” IEEE Transactions on Circuits and Systems, vol. 26, no. 4, pp. 224–234,
1979.
17. P. A. Parrilo, “Structured Semidefinite Programs and Semialgebraic Geometry
Methods in Robustness and Optimization,” Ph.D. dissertation, California Institute
of Technology, 2000.
18. A. Papachristodoulou and S. Prajna, “On the Construction of Lyapunov Functions using the Sum of Squares Decomposition,” in Proceedings of the 41st IEEE
Conference on Decision and Control, 2002., vol. 3. IEEE, 2002, pp. 3482–3487.
19. S. Prajna, A. Papachristodoulou, and P. A. Parrilo, “SOSTOOLS: Sum of squares
Optimization Toolbox for MATLAB–User’s Guide,” Control and Dynamical Systems, California Institute of Technology, Pasadena, CA, vol. 91125, 2004.
20. A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo, “SOSTOOLS Version 3.03. Sum of Squares Optimization Toolbox for MATLAB,” 2018.
21. R. Geiselhart, R. H. Gielen, M. Lazar, and F. R. Wirth, “An Alternative Converse
Lyapunov Theorem for Discrete-time Systems,” Syst. Control Lett., vol. 70, pp.
49–59, 2014.